From e937a197c1123e9adc6b2036ae47c7952ebbf138 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 2 May 2005 12:52:59 +0000
Subject: [PATCH] added ast for Match

---
 helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 1 +
 helm/ocaml/cic_transformations/tacticAst.ml        | 1 +
 2 files changed, 2 insertions(+)

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index e1623f3d2..a7c7a9ae2 100644
--- 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 a7b0fbeaf..d4e94b28b 100644
--- 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
-- 
2.39.2