diff options
| author | herbelin | 2001-08-05 18:46:45 +0000 |
|---|---|---|
| committer | herbelin | 2001-08-05 18:46:45 +0000 |
| commit | eaf89ab5428046bb3a7ccf6ccfd602b8b812c454 (patch) | |
| tree | c54808ee676b4e8ea73639496deb3ce893662d04 /syntax/PPTactic.v | |
| parent | eb4d45fa494a306d15617ac4881be41775db7177 (diff) | |
Mise en place d'un nouveau Destruct sur le modèle du nouvel Induction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1874 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'syntax/PPTactic.v')
| -rw-r--r-- | syntax/PPTactic.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v index 1406b9d233..9a9a9ee674 100644 --- a/syntax/PPTactic.v +++ b/syntax/PPTactic.v @@ -221,9 +221,13 @@ Syntax tactic | inductionid [<<(Induction $id)>>] -> ["Induction " $id] | inductionnum [<<(Induction ($NUM $n))>>] -> ["Induction " $n] + | newinductionid [<<(NewInduction $id)>>] -> ["Induction " $id] + | newinductionnum [<<(NewInduction ($NUM $n))>>] -> ["Induction " $n] | destructid [<<(Destruct $id)>>] -> ["Destruct " $id] | destructnum [<<(Destruct ($NUM $n))>>] -> ["Destruct " $n] + | newdestructid [<<(NewDestruct $id)>>] -> ["Destruct " $id] + | newdestructnum [<<(NewDestruct ($NUM $n))>>] -> ["Destruct " $n] | decomposeand [<<(DecomposeAnd $c)>>] -> [ "Decompose Record " $c ] | decomposeor [<<(DecomposeOr $c)>>] -> [ "Decompose Sum " $c ] |