Merge PR #6790: Allow universe declarations for [with Definition].

6 files changed, 6 insertions, 7 deletions

diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index f235de3509..56e3243766 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -19,7 +19,7 @@ open Decl_kinds
 (** {6 Parameters/Assumptions} *)
 
 val do_assumptions : locality * polymorphic * assumption_object_kind ->
-  Vernacexpr.inline -> (Vernacexpr.ident_decl list * constr_expr) with_coercion list -> bool
+  Vernacexpr.inline -> (ident_decl list * constr_expr) with_coercion list -> bool
 
 (************************************************************************)
 (** Internal API  *)
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 0d6367291c..6f81c4575f 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
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index edfe7aa819..a794c2db06 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -14,7 +14,6 @@ open Pretyping
 open Evarutil
 open Evarconv
 open Misctypes
-open Vernacexpr
 
 module RelDecl = Context.Rel.Declaration
 
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index b181984e07..36c2993afe 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -32,7 +32,7 @@ val do_cofixpoint :
 
 type structured_fixpoint_expr = {
   fix_name : Id.t;
-  fix_univs : Vernacexpr.universe_decl_expr option;
+  fix_univs : Constrexpr.universe_decl_expr option;
   fix_annot : Misctypes.lident option;
   fix_binders : local_binder_expr list;
   fix_body : constr_expr option;
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 457a1da054..c59286d1a3 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -57,7 +57,7 @@ let push_types env idl tl =
 
 type structured_one_inductive_expr = {
   ind_name : Id.t;
-  ind_univs : Vernacexpr.universe_decl_expr option;
+  ind_univs : universe_decl_expr option;
   ind_arity : constr_expr;
   ind_lc : (Id.t * constr_expr) list
 }
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index b8d85c8d93..8339357246 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -47,7 +47,7 @@ val declare_mutual_inductive_with_eliminations :
 
 type structured_one_inductive_expr = {
   ind_name : Id.t;
-  ind_univs : Vernacexpr.universe_decl_expr option;
+  ind_univs : universe_decl_expr option;
   ind_arity : constr_expr;
   ind_lc : (Id.t * constr_expr) list
 }