diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-05 14:30:35 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-05 14:30:35 +0000 |
| commit | b35f7449426057e962d5646a216dbc63df33a046 (patch) | |
| tree | c61b75f1ba2cb292556d6d7d3f66846c5fb845c6 /syntax | |
| parent | 4e81371e3c5e0c91c79c8b78b8711309932e3a60 (diff) | |
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
Diffstat (limited to 'syntax')
| -rw-r--r-- | syntax/PPTactic.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v index 9a9a9ee67..f4718f2f2 100644 --- a/syntax/PPTactic.v +++ b/syntax/PPTactic.v @@ -207,6 +207,8 @@ Syntax tactic | clear [<<(Clear (CLAUSE ($LIST $l)))>>] -> [ [<hov 3> "Clear " (LISTSPC ($LIST $l))] ] + | clear_body [<<(ClearBody (CLAUSE ($LIST $l)))>>] -> + [ [<hov 3> "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))>>] -> |