Merge PR #10042: [Classes] Use prepare_parameter from DeclareDef.

Reviewed-by: SkySkimmer

2 files changed, 8 insertions, 7 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 05a75ab435..5a7f60584a 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -318,6 +318,7 @@ let instance_hook k info global imps ?hook cst =
   (match hook with Some h -> h cst | None -> ())
 
 let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype =
+  (* XXX: Duplication of the declare_constant path *)
   let kind = IsDefinition Instance in
   let sigma =
     let levels = Univ.LSet.union (CVars.universes_of_constr termtype)
@@ -339,14 +340,9 @@ let do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst
   in
   let (_, ty_constr) = instance_constructor (k,u) subst in
   let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
-  let sigma = Evd.minimize_universes sigma in
-  Pretyping.check_evars env (Evd.from_env env) sigma termtype;
-  let univs = Evd.check_univ_decl ~poly sigma decl in
-  let termtype = to_constr sigma termtype in
+  let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in
   let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
-      (ParameterEntry
-         (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
-  in
+      (ParameterEntry entry, Decl_kinds.IsAssumption Decl_kinds.Logical) in
   Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma);
   instance_hook k pri global imps (ConstRef cst)
 
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 3406b6276f..27e31f486d 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -173,6 +173,11 @@ let do_assumptions ~pstate ~program_mode kind nl l =
       uvars, (coe,t,imps))
       Univ.LSet.empty l
   in
+  (* XXX: Using `DeclareDef.prepare_parameter` here directly is not
+     possible as we indeed declare several parameters; however,
+     restrict_universe_context should be called in a centralized place
+     IMO, thus I think we should adapt `prepare_parameter` to handle
+     this case too. *)
   let sigma = Evd.restrict_universe_context sigma uvars in
   let uctx = Evd.check_univ_decl ~poly:(pi2 kind) sigma udecl in
   let ubinders = Evd.universe_binders sigma in