aboutsummaryrefslogtreecommitdiff
path: root/syntax
diff options
context:
space:
mode:
Diffstat (limited to 'syntax')
-rw-r--r--syntax/PPCases.v9
1 files changed, 8 insertions, 1 deletions
diff --git a/syntax/PPCases.v b/syntax/PPCases.v
index b26cd5a8c6..ef328fe77d 100644
--- a/syntax/PPCases.v
+++ b/syntax/PPCases.v
@@ -31,8 +31,15 @@ Syntax constr
-> [ "| " $eqn ]
| tomatch [(TOMATCH ($LIST $lc))] -> [(NECOMMANDLIST2 ($LIST $lc)):E]
- | pattconstruct [(PATTCONSTRUCT ($LIST $T))] -> [(APPLIST ($LIST $T))]
+ ;
+
+ level 10:
+ pattconstruct [(PATTCONSTRUCT $C $D ($LIST $T))] ->
+ [(APPLIST $C $D ($LIST $T))]
+ ;
+ level 0:
+ pattconstructatomic [(PATTCONSTRUCT $C)] -> [ $C ]
;
level 8: