X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=59bb1bc81c92159024c6ac3abb4db919639e1d80;hb=ef51893c7f8a5f1319e122322782b734b48c205a;hp=a879ccf94ff1f380d011e71927250df3e3c46f3d;hpb=287dfa9d6e5213d4c578f5b3485fc52a86ce7934;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index a879ccf94..59bb1bc81 100644
--- 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;