aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--parsing/g_basevernac.ml41
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 4b5c98ba7b..be3d3fe264 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -358,6 +358,7 @@ GEXTEND Gram
[[ IDENT "ast"; IDENT "list" -> AstListParser
| IDENT "ast" -> AstParser
| IDENT "constr" -> ConstrParser
+ | IDENT "cases_pattern" -> CasesPatternParser
| IDENT "tactic" -> TacticParser
| IDENT "vernac" -> VernacParser ]]
;