- Changed ApplyTransformation API to return both the mathml and acic,

[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 00b4c4418cf7847d82b8dcee13dfb1c6b00e97d3..478e97d390531fe2df2e77f29570a0e0c17455cb 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -392,7 +392,7 @@ EXTEND
     tl = OPT [ "with";
       types = LIST1 [
         name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
-        OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
+       OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
           (name, true, typ, constructors) ] SEP "with" -> types
     ] ->
       let params =
@@ -427,6 +427,10 @@ EXTEND
             ind_types
         in
         return_command loc (TacticAst.Inductive (params, ind_types))
+    | [ IDENT "coercion" | IDENT "Coercion" ] ; name = IDENT -> 
+        return_command loc (TacticAst.Coercion (CicAst.Ident (name,Some [])))
+    | [ IDENT "coercion" | IDENT "Coercion" ] ; name = URI -> 
+        return_command loc (TacticAst.Coercion (CicAst.Uri (name,Some [])))
     | [ IDENT "goal" | IDENT "Goal" ]; typ = term;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
         return_command loc (TacticAst.Theorem (`Goal, None, typ, body))