X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteParser.ml;h=081055ce84d64ffea17c354bc635e4e091100775;hb=6e01bb1ae52fe45ce77a7f950efb5feb295e82b1;hp=24d1b3feb441b864d977807b931196e1c3ea33f5;hpb=78ed249d75b6b65847e4739dabf7c18b8288c7d8;p=helm.git

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 24d1b3feb..081055ce8 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/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 -> 
@@ -638,9 +639,11 @@ EXTEND
             ind_types
         in
         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
-    | IDENT "coercion" ; suri = URI ; arity = OPT int ->
+    | IDENT "coercion" ; suri = URI ; arity = OPT int ; saturations = OPT int ->
         let arity = match arity with None -> 0 | Some x -> x in
-        GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity)
+        let saturations = match saturations with None -> 0 | Some x -> x in
+        GrafiteAst.Coercion
+         (loc, UriManager.uri_of_string suri, true, arity, saturations)
     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
         GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->