From b35f7449426057e962d5646a216dbc63df33a046 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 5 Oct 2001 14:30:35 +0000 Subject: Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'ClearBody H' et 'Assert H := c' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2104 85f007b7-540e-0410-9357-904b9bb8a0f7 --- syntax/PPTactic.v | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'syntax') diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v index 9a9a9ee674..f4718f2f2b 100644 --- a/syntax/PPTactic.v +++ b/syntax/PPTactic.v @@ -207,6 +207,8 @@ Syntax tactic | clear [<<(Clear (CLAUSE ($LIST $l)))>>] -> [ [ "Clear " (LISTSPC ($LIST $l))] ] + | clear_body [<<(ClearBody (CLAUSE ($LIST $l)))>>] -> + [ [ "ClearBody " (LISTSPC ($LIST $l))] ] | move [<<(MoveDep $id1 $id2)>>] -> [ "Move " $id1 " after " $id2 ] @@ -255,6 +257,10 @@ Syntax tactic | absurd [<<(Absurd $C)>>] -> ["Absurd " $C] | cut [<<(Cut $C)>>] -> ["Cut " $C] + | truecutid [<<(TrueCut $C $id)>>] -> ["Assert " $id " : " $C] + | truecut [<<(TrueCut $C)>>] -> ["Assert " $C] + | forward [<<(Forward $C $id)>>] -> ["Assert " $id " := " $C] + | lettac_cons [<<(LetTac $id $c (LETPATTERNS $p ($LIST $pl)))>>] -> ["LetTac" [1 1] $id ":=" $c [1 1] "in" [1 1] (LETPATTERNS $p ($LIST $pl))] | lettac_nil [<<(LetTac $id $c (LETPATTERNS))>>] -> -- cgit v1.2.3