X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fgrafite%2FgrafiteAst.ml;h=bc001d173c4b71575b686c78cf470d15be18fa1b;hb=46ee64f692a1e5e65864ebb82ec875e8d115843c;hp=9d4d3490a9ce7b3729b85e50484bf3790b174ad2;hpb=a2412e41cda18a25d780ae631ee02d6ae05c52b1;p=helm.git

diff --git a/matitaB/components/grafite/grafiteAst.ml b/matitaB/components/grafite/grafiteAst.ml
index 9d4d3490a..bc001d173 100644
--- a/matitaB/components/grafite/grafiteAst.ml
+++ b/matitaB/components/grafite/grafiteAst.ml
@@ -32,7 +32,7 @@ type loc = Stdpp.location
 type npattern = 
  NotationPt.term option * (string * NotationPt.term) list * NotationPt.term option
 
-type auto_params = NotationPt.term list option * (string*string) list
+type auto_params = (bool * NotationPt.term list) option * (string*string) list
 
 type ntactic =
    | NApply of loc * NotationPt.term
@@ -103,9 +103,9 @@ type command =
   | NUnivConstraint of loc * NUri.uri * NUri.uri
   | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list
   | NCoercion of loc * string *
-      NotationPt.term * NotationPt.term *
-      (string * NotationPt.term) * NotationPt.term
-  | NQed of loc
+      (NotationPt.term * NotationPt.term *
+        (string * NotationPt.term) * NotationPt.term) option
+  | NQed of loc * bool
   (* ex lexicon commands *)
   | Alias of loc * alias_spec
       (** parameters, name, type, fields *)