added Variant theorem flavour

[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 9a4340f9fb4b692a9c797e63de88875f57c5ff6f..451d772925d8b5a50b63bdb1772af4e96c002357 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -615,6 +615,11 @@ EXTEND
         TacticAst.Set (loc, n, v)
     |  [ IDENT "drop" ] -> TacticAst.Drop loc
     | [ IDENT "qed"   ] -> TacticAst.Qed loc
+    | IDENT "variant" ; name = IDENT; SYMBOL ":"; 
+      typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
+        TacticAst.Obj (loc, 
+          TacticAst.Theorem 
+            (`Variant,name,typ,Some (CicAst.Ident (newname, None))))
     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
         TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, typ, body))