added ast for Match

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index e1623f3d2bbcec6387f688798e5d253adb40af0d..a7c7a9ae21329089fc0c3983ca8c6618a08b1a69 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -480,6 +480,7 @@ EXTEND
     | [ IDENT "check"   ]; t = term ->
         TacticAst.Check (loc, t)
     | [ IDENT "hint" ] -> TacticAst.Hint loc
+    | [ IDENT "pmatch" ] ; t = term -> TacticAst.Match (loc,t)
     | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name)
   ]];
 

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index a7b0fbeafa523dc402ab4df99cc9e93c8aefd215..d4e94b28bea16ce511ca4341b6489378becedde4 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -96,6 +96,7 @@ type 'term macro =
   | Print of loc * string
   | Check of loc * 'term 
   | Hint of loc
+  | Match of loc * 'term 
   | Quit of loc
   | Redo of loc * int option
   | Undo of loc * int option