diff options
Diffstat (limited to 'parsing/pcoq.ml4')
| -rw-r--r-- | parsing/pcoq.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index a20c0d1ef8..b0e4fc1f15 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -415,7 +415,7 @@ module Vernac_ = let syntax = gec_vernac "syntax_command" let vernac = gec_vernac "Vernac.vernac" let vernac_eoi = eoi_entry vernac - + let rec_definition = gec_vernac "Vernac.rec_definition" (* Main vernac entry *) let main_entry = Gram.entry_create "vernac" |