X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Flexicon%2FlexiconAst.ml;h=b0b9399b5850162623b4dd487f791d093cd7cad3;hb=a5709dff43233c041f77a4ee4b7f2df1a3c51ab6;hp=0c588d189200d3eb55a0e124269683a361c6e84a;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/lexicon/lexiconAst.ml b/matita/components/lexicon/lexiconAst.ml
index 0c588d189..b0b9399b5 100644
--- a/matita/components/lexicon/lexiconAst.ml
+++ b/matita/components/lexicon/lexiconAst.ml
@@ -44,16 +44,16 @@ type command =
   | Include of loc * string * inclusion_mode * string (* _,buri,_,path *)
   | Alias of loc * alias_spec
       (** parameters, name, type, fields *) 
-  | Notation of loc * direction option * CicNotationPt.term * Gramext.g_assoc *
-      int * CicNotationPt.term
+  | Notation of loc * direction option * NotationPt.term * Gramext.g_assoc *
+      int * NotationPt.term
       (* direction, l1 pattern, associativity, precedence, l2 pattern *)
   | Interpretation of loc *
-      string * (string * CicNotationPt.argument_pattern list) *
-        CicNotationPt.cic_appl_pattern
+      string * (string * NotationPt.argument_pattern list) *
+        NotationPt.cic_appl_pattern
       (* description (i.e. id), symbol, arg pattern, appl pattern *)
 
 (* composed magic: term + command magics. No need to change this value *)
-let magic = magic + 10000 * CicNotationPt.magic
+let magic = magic + 10000 * NotationPt.magic
 
 let description_of_alias =
  function