diff options
Diffstat (limited to 'toplevel/vernacexpr.ml')
| -rw-r--r-- | toplevel/vernacexpr.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 0d54fb66d..8c1d77511 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -171,8 +171,8 @@ type vernac_expr = (* Syntax *) | VernacGrammar of lstring * raw_grammar_entry list - | VernacTacticGrammar of - (lstring * (lstring * grammar_production list) * raw_tactic_expr) list + | VernacTacticGrammar of int * + (lstring * grammar_production list * raw_tactic_expr) list | VernacSyntax of lstring * raw_syntax_entry list | VernacSyntaxExtension of locality_flag * (lstring * syntax_modifier list) option |