"include" command implemented.

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;

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index c4f2a29ac4a389cc7ff9ac7e128fb8ea0e2b1efb..a051c2af6336d2a93e4a54b2d84b18ae2b9a1211 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -126,6 +126,7 @@ type obj =
       (string * CicAst.term) list
 
 type ('term,'obj) command =
+  | Include of loc * string
   | Set of loc * string * string
   | Drop of loc
   | Qed of loc

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index 86c7185ecf1308d75e1f34707059c1cc77f3fc1f..3a8b5213c805484e4bf9b36249244cfe19cfe3d1 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -220,6 +220,7 @@ let pp_obj = function
 
 
 let pp_command = function
+  | Include (_,path) -> "include " ^ path
   | Qed _ -> "qed"
   | Drop _ -> "drop"
   | Set (_, name, value) -> sprintf "Set \"%s\" \"%s\"" name value