[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`]

1 files changed, 0 insertions, 7 deletions

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