- decompose tactic: decomposable constants are now allowed (they are unfolded)

[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 9b9a5da22ed93d8534681ce02a4ef18042b9338e..b41ae8ebcd8468c14415e86ca2e17c7eed149cc4 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -401,8 +401,9 @@ EXTEND
   macro: [
     [ [ IDENT "check"   ]; t = term ->
         GrafiteAst.Check (loc, t)
-    | [ IDENT "inline"]; suri = QSTRING ->
-         GrafiteAst.Inline (loc,suri)
+    | [ IDENT "inline"]; suri = QSTRING; prefix = OPT QSTRING ->
+         let prefix = match prefix with None -> "" | Some prefix -> prefix in
+        GrafiteAst.Inline (loc,suri,prefix)
     | [ IDENT "hint" ] -> GrafiteAst.Hint loc
     | [ IDENT "whelp"; "match" ] ; t = term -> 
         GrafiteAst.WMatch (loc,t)