From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 2 May 2005 12:52:59 +0000 (+0000)
Subject: added ast for Match
X-Git-Tag: single_binding~125
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e937a197c1123e9adc6b2036ae47c7952ebbf138;p=helm.git

added ast for Match
---

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