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

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 89a09fc50..e7e3234c9 100644
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -25,7 +25,7 @@
 
 (* $Id$ *)
 
-module N  = CicNotationPt
+module N  = NotationPt
 module G  = GrafiteAst
 module L  = LexiconAst
 module LE = LexiconEngine
@@ -222,7 +222,7 @@ EXTEND
            | N.Implicit _ -> false
            | N.UserInput -> true
            | _ -> raise (Invalid_argument "malformed target parameter list 1")) l
-      | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ CicNotationPp.pp_term params)) ]
+      | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ NotationPp.pp_term params)) ]
   ];
   direction: [
     [ SYMBOL ">" -> `LeftToRight
@@ -868,7 +868,7 @@ EXTEND
     | IDENT "universe"; IDENT "constraint"; u1 = tactic_term; 
         SYMBOL <:unicode<lt>> ; u2 = tactic_term ->
         let urify = function 
-          | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
+          | NotationPt.AttributedTerm (_, NotationPt.Sort (`NType i)) ->
               NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
           | _ -> raise (Failure "only a Type[…] sort can be constrained")
         in