diff options
Diffstat (limited to 'syntax/PPCases.v')
| -rw-r--r-- | syntax/PPCases.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/syntax/PPCases.v b/syntax/PPCases.v index 3bdf47feb..356f6b214 100644 --- a/syntax/PPCases.v +++ b/syntax/PPCases.v @@ -95,3 +95,4 @@ Syntax constr [1 1] [<hov 0> $tomatch:L ] ] [1 0] "in " [<hov 0> $c:L ] ] ] . + |