From 6e78a98aaa51df2975595a6adcbe263febbccadc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 1 Feb 2002 22:08:39 +0000
Subject: Ajout tactiques Rename et Pose; modifications pour Inversion

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2449 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 syntax/PPTactic.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'syntax')

diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v
index a149b0f070..517c522f4e 100644
--- a/syntax/PPTactic.v
+++ b/syntax/PPTactic.v
@@ -259,7 +259,9 @@ Syntax tactic
   | cut [<<(Cut $C)>>] -> ["Cut " $C]
   | truecutid [<<(TrueCut $C $id)>>] -> ["Assert " $id " : " $C]
   | truecut [<<(TrueCut $C)>>] -> ["Assert " $C]
-  | forward [<<(Forward $C $id)>>] -> ["Assert " $id " := " $C]
+  | forward [<<(Forward _ $C $id)>>] -> ["Assert " $id " := " $C]
+  | pose_named [<<(Forward "KeepBody" $C $id)>>] -> ["Pose " $id " := " $C]
+  | pose_anon  [<<(Forward "KeepBody" $C)>>] -> ["Pose " $C]
 
   | lettac_cons [<<(LetTac $id $c (LETPATTERNS $p ($LIST $pl)))>>] -> 
 	["LetTac" [1 1] $id ":=" $c [1 1] "in" [1 1] (LETPATTERNS $p ($LIST $pl))]
-- 
cgit v1.2.3