diff options
Diffstat (limited to 'parsing/pcoq.ml')
| -rw-r--r-- | parsing/pcoq.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 9787af826..c5823440a 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -338,6 +338,7 @@ module Vernac_ = let vernac_eoi = eoi_entry vernac let rec_definition = gec_vernac "Vernac.rec_definition" let red_expr = make_gen_entry utactic "red_expr" + let hint_info = gec_vernac "hint_info" (* Main vernac entry *) let main_entry = Gram.entry_create "vernac" let noedit_mode = gec_vernac "noedit_command" |