X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=e2108381200b82ae16626d0a61fd11bafc419ac3;hb=b348a1a39e17b541fca17d2218a3b91bd7f1fece;hp=24d1b3feb441b864d977807b931196e1c3ea33f5;hpb=ca2a604c2817deb118d595611b94a0d77978eab6;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 24d1b3feb..e21083812 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -459,7 +459,8 @@ EXTEND
 	 in
 	 let prefix = match prefix with None -> "" | Some prefix -> prefix in
 	 GrafiteAst.Inline (loc,style,suri,prefix)
-    | [ IDENT "hint" ] -> GrafiteAst.Hint loc
+    | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite")  -> 
+         if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
     | IDENT "auto"; params = auto_params ->
         GrafiteAst.AutoInteractive (loc,params)
     | [ IDENT "whelp"; "match" ] ; t = term ->