diff options
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 ] |