diff options
Diffstat (limited to 'vernac/comDefinition.mli')
-rw-r--r-- | vernac/comDefinition.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 0d6367291..6f81c4575 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -17,7 +17,7 @@ open Constrexpr (** {6 Definitions/Let} *) val do_definition : program_mode:bool -> - Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option -> + Id.t -> definition_kind -> universe_decl_expr option -> local_binder_expr list -> red_expr option -> constr_expr -> constr_expr option -> unit Lemmas.declaration_hook -> unit @@ -27,6 +27,6 @@ val do_definition : program_mode:bool -> (** Not used anywhere. *) val interp_definition : - Vernacexpr.universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr -> + universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr -> constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * Univdecls.universe_decl * Impargs.manual_implicits |