new pp function for proofs

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

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 8848efad6ce3865660fd2b4ed797ab050bf001d9..e83152226f257cb21132fbb3abee6b0f3c271ae7 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -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: [ [
@@ -528,11 +531,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