"include" command implemented.

[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.ml

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 25c15c575f9c763e33962106b2912456ed3554d1..760b34a423ac926cca31c9f4cc35e0893048e01d 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -635,14 +635,16 @@ EXTEND
             ind_types
         in
         TacticAst.Obj (loc,TacticAst.Inductive (params, ind_types))
-    | [ IDENT "coercion" ] ; name = IDENT -> 
+    | IDENT "coercion" ; name = IDENT -> 
         TacticAst.Coercion (loc, CicAst.Ident (name,Some []))
-    | [ IDENT "coercion" ] ; name = URI -> 
+    | IDENT "coercion" ; name = URI -> 
         TacticAst.Coercion (loc, CicAst.Uri (name,Some []))
-    | [ IDENT "alias"   ]; spec = alias_spec ->
+    | IDENT "alias" ; spec = alias_spec ->
         TacticAst.Alias (loc, spec)
-    | [ IDENT "record" ]; (params,name,ty,fields) = record_spec ->
+    | IDENT "record" ; (params,name,ty,fields) = record_spec ->
         TacticAst.Obj (loc,TacticAst.Record (params,name,ty,fields))
+    | IDENT "include" ; path = QSTRING ->
+        TacticAst.Include (loc,path)
   ]];
 
   executable: [
@@ -718,7 +720,8 @@ module EnvironmentP3 =
             s :: acc)
           env []
       in
-      String.concat "\n" (List.sort compare aliases)
+      String.concat "\n" (List.sort compare aliases) ^
+       (if aliases = [] then "" else "\n")
 
     EXTEND
       GLOBAL: aliases;