fixed demodulation of goal

[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 aa10bdcf315e2e436b4f45479df51bd5397cda33..e83152226f257cb21132fbb3abee6b0f3c271ae7 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/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: [ [
@@ -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