...

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

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index aa10bdcf315e2e436b4f45479df51bd5397cda33..1b06b81c97fd64b26b4429956c25e9c573c7bdd5 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -341,7 +341,7 @@ EXTEND
         GrafiteAst.WMatch (loc,t)
     | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> 
         GrafiteAst.WInstance (loc,t)
-    | [ IDENT "whelp"; IDENT "locate" ] ; id = IDENT -> 
+    | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING -> 
         GrafiteAst.WLocate (loc,id)
     | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
         GrafiteAst.WElim (loc, t)
@@ -449,7 +449,10 @@ EXTEND
   ];
   
   include_command: [ [
-      IDENT "include" ; path = QSTRING -> loc,path
+      IDENT "include" ; path = QSTRING -> 
+        loc,path,LexiconAst.WithPreferences
+    | IDENT "include'" ; path = QSTRING -> 
+        loc,path,LexiconAst.WithoutPreferences
    ]];
 
   grafite_command: [ [
@@ -469,6 +472,8 @@ EXTEND
       body = term ->
         GrafiteAst.Obj (loc,
           Ast.Theorem (flavour, name, Ast.Implicit, Some body))
+    | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
+        GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
     | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
         defs = CicNotationParser.let_defs -> 
           let name,ty = 
@@ -528,11 +533,11 @@ EXTEND
        fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
     | com = comment ->
        fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
-    | (iloc,fname) = include_command ; SYMBOL "."  ->
+    | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
        fun ~include_paths status ->
         let path = DependenciesParser.baseuri_of_script ~include_paths fname in
         let status =
-         LexiconEngine.eval_command status (LexiconAst.Include (iloc,path))
+         LexiconEngine.eval_command status (LexiconAst.Include (iloc,path,mode))
         in
          status,
           LSome