[declareDef] Cleanup of allow_evars and check_evars

We don't the parameter anymore as the paths are too different now.

Note that this removes a duplicate `check_evars` that has been in
`master` quite some time [double check in `ComDefinition` and in
`DeclareDef.prepare_definition`]

4 files changed, 10 insertions, 23 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index e0bf9e777c..65d20a13a1 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -328,7 +328,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst
   in
   let (_, ty_constr) = instance_constructor (k,u) subst in
   let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
-  let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma ~udecl ~types:termtype in
+  let sigma, entry = DeclareDef.prepare_parameter ~poly sigma ~udecl ~types:termtype in
   let cst = Declare.declare_constant ~name
       ~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in
   DeclareUniv.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma);
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index eb70ad0ac0..73b523f0b3 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -12,7 +12,6 @@ open Pp
 open Util
 open Redexpr
 open Constrintern
-open Pretyping
 
 (* Commands of the interface: Constant definitions *)
 
@@ -70,18 +69,12 @@ let interp_definition ~program_mode pl bl ~poly red_option c ctypopt =
   let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in
   (c, tyopt), evd, udecl, imps
 
-let check_definition ~program_mode (ce, evd) =
-  let env = Global.env () in
-  check_evars_are_solved ~program_mode env evd;
-  ce
-
 let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
   let program_mode = false in
   let (body, types), evd, udecl, impargs =
     interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
   in
   let evd, ce = DeclareDef.prepare_definition ~opaque:false ~poly evd ~udecl ~types ~body in
-  let ce = check_definition ~program_mode (ce, evd) in
   let uctx = Evd.evar_universe_context evd in
   let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
   let kind = Decls.IsDefinition kind in
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index f283f700b7..2528dfd38f 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -153,23 +153,17 @@ let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe =
 
 (* Preparing proof entries *)
 
-let check_definition_evars ~allow_evars sigma =
-  let env = Global.env () in
-  if not allow_evars then Pretyping.check_evars_are_solved ~program_mode:false env sigma
-
 let prepare_definition ?opaque ?inline ~poly ~udecl ~types ~body sigma =
-  let allow_evars = false in
-  check_definition_evars ~allow_evars sigma;
-  let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars)
+  let env = Global.env () in
+  Pretyping.check_evars_are_solved ~program_mode:false env sigma;
+  let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:true
       sigma (fun nf -> nf body, Option.map nf types)
   in
   let univs = Evd.check_univ_decl ~poly sigma udecl in
   sigma, definition_entry ?opaque ?inline ?types ~univs body
 
 let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma =
-  let allow_evars = true in
-  check_definition_evars ~allow_evars sigma;
-  let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars)
+  let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false
       sigma (fun nf -> nf body, Option.map nf types)
   in
   let univs = Evd.check_univ_decl ~poly sigma udecl in
@@ -188,9 +182,10 @@ let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma =
   let uctx = Evd.evar_universe_context sigma in
   c, cty, uctx, obls
 
-let prepare_parameter ~allow_evars ~poly ~udecl ~types sigma =
-  check_definition_evars ~allow_evars sigma;
-  let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars)
+let prepare_parameter ~poly ~udecl ~types sigma =
+  let env = Global.env () in
+  Pretyping.check_evars_are_solved ~program_mode:false env sigma;
+  let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:true
       sigma (fun nf -> nf types)
   in
   let univs = Evd.check_univ_decl ~poly sigma udecl in
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 27d9460382..f72954d8c2 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -110,8 +110,7 @@ val prepare_obligation
   -> Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info
 
 val prepare_parameter
-  : allow_evars:bool
-  -> poly:bool
+  : poly:bool
   -> udecl:UState.universe_decl
   -> types:EConstr.types
   -> Evd.evar_map