X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=c465fe1d8cd48f16e2b00968a0c6df1f14b2bf02;hb=b108ab28153129d6578d7d9c2ffdf19e6779d86f;hp=330a93a0dbb1691272c657b003cd77bd19f6839f;hpb=0fde70bd19b8fdfa72b807b9713a02ad1bd91b5b;p=helm.git

diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml
index 330a93a0d..c465fe1d8 100644
--- a/matita/components/grafite_parser/grafiteDisambiguate.ml
+++ b/matita/components/grafite_parser/grafiteDisambiguate.ml
@@ -27,15 +27,6 @@
 
 exception BaseUriNotSetYet
 
-type tactic = 
- (CicNotationPt.term, CicNotationPt.term, 
-  CicNotationPt.term GrafiteAst.reduction, string) 
-   GrafiteAst.tactic
-   
-type lazy_tactic = 
-  (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) 
-    GrafiteAst.tactic
-
 let singleton msg = function
   | [x], _ -> x
   | l, _   ->
@@ -61,7 +52,6 @@ let ncic_mk_choice = function
            | false -> NCic.Implicit `Term)
         ~mk_appl:(function 
            (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
-        ~term_of_uri:(fun _ -> assert false)
         ~term_of_nref:(fun nref -> NCic.Const nref)
        name dsc
   | LexiconAst.Number_alias (_, dsc) -> 
@@ -71,13 +61,8 @@ let ncic_mk_choice = function
   | LexiconAst.Ident_alias (name, uri) -> 
      uri, `Sym_interp 
       (fun l->assert(l = []);
-        try
-         let nref = NReference.reference_of_string uri in
-          NCic.Const nref
-        with
-         NReference.IllFormedReference _ ->
-          let uri = UriManager.uri_of_string uri in
-           fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
+        let nref = NReference.reference_of_string uri in
+         NCic.Const nref)
 ;;
 
 
@@ -143,7 +128,7 @@ let disambiguate_nterm expty estatus context metasenv subst thing
 
 
 type pattern = 
-  CicNotationPt.term Disambiguate.disambiguator_input option * 
+  NotationPt.term Disambiguate.disambiguator_input option * 
   (string * NCic.term) list * NCic.term option
 
 let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) =
@@ -198,12 +183,12 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
    in
    let name = 
      match obj with
-     | CicNotationPt.Inductive (_,(name,_,_,_)::_)
-     | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind"
-     | CicNotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
-     | CicNotationPt.Inductive _ -> assert false
+     | NotationPt.Inductive (_,(name,_,_,_)::_)
+     | NotationPt.Record (_,name,_,_) -> name ^ ".ind"
+     | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
+     | NotationPt.Inductive _ -> assert false
    in
-     UriManager.uri_of_string (baseuri ^ "/" ^ name)
+     NUri.uri_of_string (baseuri ^ "/" ^ name)
   in
   let diff, _, _, cic =
    singleton "third"
@@ -212,7 +197,7 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
       ~description_of_alias:LexiconAst.description_of_alias
       ~mk_choice:ncic_mk_choice
       ~mk_implicit ~fix_instance
-      ~uri:(OCic2NCic.nuri_of_ouri uri)
+      ~uri
       ~rdb:estatus
       ~aliases:estatus#lstatus.LexiconEngine.aliases
       ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases) 
@@ -220,20 +205,10 @@ 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 (text,prefix_len,cmd)=
+
+let disambiguate_command estatus (text,prefix_len,cmd)=
   match cmd with
-   | GrafiteAst.Index(loc,key,uri) -> (* MATITA 1.0 *) assert false
-   | GrafiteAst.Select (loc,uri) -> 
-        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
-   | GrafiteAst.Default _
-   | GrafiteAst.Drop _
    | GrafiteAst.Include _
    | GrafiteAst.Print _
-   | GrafiteAst.Qed _
    | GrafiteAst.Set _ as 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