- cic almost not used

[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 330a93a0dbb1691272c657b003cd77bd19f6839f..bd633d5d2edb26057068c8ee0f8c3dc7146971a3 100644 (file)
--- a/matita/components/grafite_parser/grafiteDisambiguate.ml
+++ b/matita/components/grafite_parser/grafiteDisambiguate.ml
@@ -28,14 +28,10 @@
 exception BaseUriNotSetYet
 
 type tactic = 
- (CicNotationPt.term, CicNotationPt.term, 
-  CicNotationPt.term GrafiteAst.reduction, string) 
+ (NotationPt.term, NotationPt.term, 
+  NotationPt.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, _   ->
@@ -71,13 +67,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 +134,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 +189,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 +203,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)