- hExtlib: new function "list_assoc_all"

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

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 5a22a4b62817c6cf354d9bcfa7668aa03deacff7..e2ab011dac927cd33a05c4c741240a9c8766ed36 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -449,6 +449,16 @@ EXTEND
       (match tl with Some l -> l | None -> []),
       params
    ]
+];
+  inline_params:[
+   [ params = LIST0 
+      [ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix  
+      | IDENT "procedural" -> G.IPProcedural
+      | flavour = inline_flavour -> G.IPAs flavour
+      | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth 
+      | IDENT "nodefaults" -> G.IPNoDefaults
+      ] -> params
+   ]
 ];
   by_continuation: [
     [ WEPROVED; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,Some id,t1)
@@ -537,7 +547,7 @@ EXTEND
   inline_flavour: [
      [ attr = theorem_flavour -> attr
      | [ IDENT "axiom"     ]  -> `Axiom
-     | [ IDENT "mutual"    ]  -> `MutualDefinition
+     | [ IDENT "variant"   ]  -> `Variant
      ]
   ];
   inductive_spec: [ [
@@ -592,16 +602,8 @@ EXTEND
           G.Check (loc, t)
       | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
           G.Eval (loc, kind, t)
-      | [ IDENT "inline"]; 
-          style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
-          suri = QSTRING; prefix = OPT QSTRING;
-          flavour = OPT [ "as"; attr = inline_flavour -> attr ] ->
-           let style = match style with 
-              | None       -> G.Declarative
-              | Some depth -> G.Procedural depth
-           in
-           let prefix = match prefix with None -> "" | Some prefix -> prefix in
-           G.Inline (loc,style,suri,prefix, flavour)
+      | IDENT "inline"; suri = QSTRING; params = inline_params -> 
+           G.Inline (loc, suri, params)
       | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite")  -> 
            if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
       | IDENT "auto"; params = auto_params ->