diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 9f186224b..0fbf2f567 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -260,7 +260,7 @@ module Vernac_ : val noedit_mode : vernac_expr Gram.entry val command_entry : vernac_expr Gram.entry val red_expr : raw_red_expr Gram.entry - val hint_info : Vernacexpr.hint_info_expr Gram.entry + val hint_info : Typeclasses.hint_info_expr Gram.entry end (** The main entry: reads an optional vernac command *) |