tests/* ==> *

[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 a879ccf94ff1f380d011e71927250df3e3c46f3d..59bb1bc81c92159024c6ac3abb4db919639e1d80 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -181,7 +181,7 @@ EXTEND
     [ defs = LIST1 [
         name = IDENT;
         args = LIST1 [arg = arg -> arg];
-        index_name = OPT [ IDENT "on"; idx = IDENT -> idx ];
+        index_name = OPT [ "on"; idx = IDENT -> idx ];
         ty = OPT [ SYMBOL ":" ; t = term -> t ];
         SYMBOL <:unicode<def>> (* ≝ *);
         t1 = term ->
@@ -635,14 +635,19 @@ 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)
+    | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
+       let uris = List.map UriManager.uri_of_string uris in
+        TacticAst.Default (loc,what,uris)
   ]];
 
   executable: [
@@ -718,7 +723,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;