aboutsummaryrefslogtreecommitdiff
path: root/syntax
diff options
context:
space:
mode:
Diffstat (limited to 'syntax')
-rw-r--r--syntax/PPTactic.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v
index a72a70ee57..3ca546f80d 100644
--- a/syntax/PPTactic.v
+++ b/syntax/PPTactic.v
@@ -370,6 +370,7 @@ Syntax tactic
| intropatconj [<<(CONJPATTERN ($LIST $cp))>>] ->
[ "(" [<hov 0> (LISTCOMA ($LIST $cp))] ")" ]
| intropatid [<<(IDENTIFIER ($VAR $id))>>] -> [ $id ]
+ | intropatwild [<<(WILDCAR)>>] -> [ "_" ]
| patterncons [<<(NEPATTERNLIST $H ($LIST $T))>>]