diff options
Diffstat (limited to 'syntax')
| -rw-r--r-- | syntax/PPTactic.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v index 6c0e1a2792..1406b9d233 100644 --- a/syntax/PPTactic.v +++ b/syntax/PPTactic.v @@ -227,7 +227,7 @@ Syntax tactic | decomposeand [<<(DecomposeAnd $c)>>] -> [ "Decompose Record " $c ] | decomposeor [<<(DecomposeOr $c)>>] -> [ "Decompose Sum " $c ] - | decomposethese [<<(DecomposeThese (CLAUSE ($LIST $l)) $c )>>] -> + | decomposethese [<<(DecomposeThese $c ($LIST $l))>>] -> ["Decompose" [1 1] [<hov 0> "[" (LISTSPC ($LIST $l)) "]" ] [1 1] $c] | mutualcofixtactic [<<(Cofix $id $cfe ($LIST $fd))>>] @@ -389,6 +389,10 @@ Syntax tactic | clause_none [<<(CLAUSE)>>] -> [ ] + (* Hypotheses *) + | inhyp [<<(INHYP $x)>>] -> [ $x ] + | inhyptype [<<(INHYPTYPE $x)>>] -> [ "(Type of " $x ")" ] + (* Lists with separators *) | listspc_cons [<<(LISTSPC $x ($LIST $l))>>] -> [ $x [1 0] (LISTSPC ($LIST $l)) ] |