acic_procedural and tactics removed

[helm.git] / matita / components / grafite_parser / grafiteDisambiguate.ml

diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml
index eb9f33f516c8ff6c0a31e29087232b21daa19fce..330a93a0dbb1691272c657b003cd77bd19f6839f 100644 (file)
--- a/matita/components/grafite_parser/grafiteDisambiguate.ml
+++ b/matita/components/grafite_parser/grafiteDisambiguate.ml
@@ -220,13 +220,11 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
   let estatus = LexiconEngine.set_proof_aliases estatus diff in
    estatus, cic
 ;;
-let disambiguate_command estatus ?baseuri metasenv (text,prefix_len,cmd)=
+let disambiguate_command estatus ?baseuri (text,prefix_len,cmd)=
   match cmd with
    | GrafiteAst.Index(loc,key,uri) -> (* MATITA 1.0 *) assert false
    | GrafiteAst.Select (loc,uri) -> 
-        estatus, metasenv, GrafiteAst.Select(loc,uri)
-   | GrafiteAst.Pump(loc,i) -> 
-        estatus, metasenv, GrafiteAst.Pump(loc,i)
+        estatus, GrafiteAst.Select(loc,uri)
    | GrafiteAst.PreferCoercion (loc,t) -> (* MATITA 1.0 *) assert false
    | GrafiteAst.Coercion (loc,t,b,a,s) -> (* MATITA 1.0 *) assert false
    | GrafiteAst.Inverter (loc,n,indty,params) -> (* MATITA 1.0 *) assert false
@@ -236,6 +234,6 @@ let disambiguate_command estatus ?baseuri metasenv (text,prefix_len,cmd)=
    | GrafiteAst.Print _
    | GrafiteAst.Qed _
    | GrafiteAst.Set _ as cmd ->
-       estatus,metasenv,cmd
+       estatus,cmd
    | GrafiteAst.Obj (loc,obj) -> (* MATITA 1.0 *) assert false
    | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) -> (* MATITA 1.0 *) assert false