Behaviour of CicRefine.type_of_aux' on MutCases changed: branches are now

[helm.git] / components / grafite_parser / grafiteParser.ml

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 054bff6215e1f64ec1b6d90813a3f7a316b88089..2d37892217407440aac8957ee8c9029ff1bc9613 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -220,7 +220,8 @@ EXTEND
         GrafiteAst.Reflexivity loc
     | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
         GrafiteAst.Replace (loc, p, t)
-    | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec ->
+    | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
+       xnames = OPT [ "as"; n = ident_list0 -> n ] ->
        let (pt,_,_) = p in
         if pt <> None then
          raise
@@ -228,7 +229,8 @@ EXTEND
            (CicNotationParser.Parse_error
             "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
         else
-         GrafiteAst.Rewrite (loc, d, t, p)
+        let n = match xnames with None -> [] | Some names -> names in 
+         GrafiteAst.Rewrite (loc, d, t, p, n)
     | IDENT "right" ->
         GrafiteAst.Right loc
     | IDENT "ring" ->
@@ -424,11 +426,11 @@ EXTEND
     [ [ IDENT "check"   ]; t = term ->
         GrafiteAst.Check (loc, t)
     | [ IDENT "inline"]; 
-        style = OPT [ IDENT "procedural" ];
+        style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
        suri = QSTRING; prefix = OPT QSTRING ->
          let style = match style with 
-           | None   -> GrafiteAst.Declarative
-           | Some _ -> GrafiteAst.Procedural
+           | None       -> GrafiteAst.Declarative
+           | Some depth -> GrafiteAst.Procedural depth
         in
         let prefix = match prefix with None -> "" | Some prefix -> prefix in
         GrafiteAst.Inline (loc,style,suri,prefix)