diff options
Diffstat (limited to 'syntax')
| -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 ] |