X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAst.ml;h=d5eb9c241259efcb7fc1ff0e24d328b92f68bad8;hb=b73c1560045798ff1e77491050409a783d915345;hp=b8a89e1b6d885bf7293c8e5221f8d39e66eac22f;hpb=ca2a604c2817deb118d595611b94a0d77978eab6;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index b8a89e1b6..d5eb9c241 100644
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -126,14 +126,14 @@ type presentation_style = Declarative
 
 type 'term macro = 
   (* Whelp's stuff *)
-  | WHint of loc * 'term 
+  | WHint of loc * 'term
   | WMatch of loc * 'term 
   | WInstance of loc * 'term 
   | WLocate of loc * string
   | WElim of loc * 'term
   (* real macros *)
   | Check of loc * 'term 
-  | Hint of loc
+  | Hint of loc * bool
   | AutoInteractive of loc * (string * string) list
   | Inline of loc * presentation_style * string * string 
      (* URI or base-uri, name prefix *)