diff options
| author | herbelin | 2001-12-13 16:19:28 +0000 |
|---|---|---|
| committer | herbelin | 2001-12-13 16:19:28 +0000 |
| commit | 33d089aa4aaebd09e8f7facdabaa7b90a9369984 (patch) | |
| tree | 00f82baa7835fe59305c9f848e2b45331eb4e66e /syntax | |
| parent | 26e752bbf63aa85e9619740df4745fc5d039b127 (diff) | |
Affichage NewInduction/NewDesctruct
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2294 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'syntax')
| -rw-r--r-- | syntax/PPTactic.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v index 3ca546f80d..a149b0f070 100644 --- a/syntax/PPTactic.v +++ b/syntax/PPTactic.v @@ -223,13 +223,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] + | newinductionid [<<(NewInduction $id)>>] -> ["NewInduction " $id] + | newinductionnum [<<(NewInduction ($NUM $n))>>] -> ["NewInduction " $n] | destructid [<<(Destruct $id)>>] -> ["Destruct " $id] | destructnum [<<(Destruct ($NUM $n))>>] -> ["Destruct " $n] - | newdestructid [<<(NewDestruct $id)>>] -> ["Destruct " $id] - | newdestructnum [<<(NewDestruct ($NUM $n))>>] -> ["Destruct " $n] + | newdestructid [<<(NewDestruct $id)>>] -> ["NewDestruct " $id] + | newdestructnum [<<(NewDestruct ($NUM $n))>>] -> ["NewDestruct " $n] | decomposeand [<<(DecomposeAnd $c)>>] -> [ "Decompose Record " $c ] | decomposeor [<<(DecomposeOr $c)>>] -> [ "Decompose Sum " $c ] |