we parametrized CicNotationPt.obj on 'term

[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 fb0128edb0ceb63c423c53832d4eedb1681dd24a..14802a629e8cd32360a33c33d1550f506fc50b84 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -35,7 +35,8 @@ type 'a localized_option =
 
 type ast_statement =
   (CicNotationPt.term, CicNotationPt.term,
-   CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string)
+   CicNotationPt.term GrafiteAst.reduction, 
+   CicNotationPt.term CicNotationPt.obj, string)
     GrafiteAst.statement
 
 type statement =
@@ -411,9 +412,15 @@ EXTEND
   macro: [
     [ [ IDENT "check"   ]; t = term ->
         GrafiteAst.Check (loc, t)
-    | [ IDENT "inline"]; suri = QSTRING; prefix = OPT QSTRING ->
-         let prefix = match prefix with None -> "" | Some prefix -> prefix in
-        GrafiteAst.Inline (loc,suri,prefix)
+    | [ IDENT "inline"]; 
+        style = OPT [ IDENT "procedural" ];
+       suri = QSTRING; prefix = OPT QSTRING ->
+         let style = match style with 
+           | None   -> GrafiteAst.Declarative
+           | Some _ -> GrafiteAst.Procedural
+        in
+        let prefix = match prefix with None -> "" | Some prefix -> prefix in
+        GrafiteAst.Inline (loc,style,suri,prefix)
     | [ IDENT "hint" ] -> GrafiteAst.Hint loc
     | [ IDENT "whelp"; "match" ] ; t = term -> 
         GrafiteAst.WMatch (loc,t)