X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=c23e5acffd9d7270cd344fb18064e87409d1c550;hb=8a660ee06d72cfee52c707bb1d8d8be3bab0d682;hp=af8c8620472846642b368f8293dff680ca65b82c;hpb=5553ac7623425bce6f34eed6e17d4f0f8163e9aa;p=helm.git

diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml
index af8c86204..c23e5acff 100644
--- a/matita/components/grafite_parser/grafiteDisambiguate.ml
+++ b/matita/components/grafite_parser/grafiteDisambiguate.ml
@@ -28,8 +28,8 @@
 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 = 
@@ -138,7 +138,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)) =
@@ -193,10 +193,10 @@ 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
      NUri.uri_of_string (baseuri ^ "/" ^ name)
   in