aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/comDefinition.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/comDefinition.mli')
-rw-r--r--vernac/comDefinition.mli4
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