cicNotation* ==> notation*

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

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 89a09fc50cda8fe22f7379fb5c5cef08d0ae975a..e7e3234c93a4ff8b41b433daa8963328f27e5e1c 100644 (file)
--- 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