New command default "foo" uri1 ... urin

[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 760b34a423ac926cca31c9f4cc35e0893048e01d..59bb1bc81c92159024c6ac3abb4db919639e1d80 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -645,6 +645,9 @@ EXTEND
         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: [