Merge PR #8893: Moving evars_of_term from constr to econstr

Ack-by: SkySkimmer
Reviewed-by: gares
Ack-by: herbelin
Reviewed-by: maximedenes
Reviewed-by: ppedrot

1 files changed, 4 insertions, 3 deletions

diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 12df3215ad..d2c986fe5c 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -88,11 +88,12 @@ let do_definition ~ontop ~program_mode ?hook ident k univdecl bl red_option c ct
     let (c,ctx), sideff = Future.force ce.const_entry_body in
     assert(Safe_typing.empty_private_constants = sideff);
     assert(Univ.ContextSet.is_empty ctx);
+    Obligations.check_evars env evd;
+    let c = EConstr.of_constr c in
     let typ = match ce.const_entry_type with
-      | Some t -> t
-      | None -> EConstr.to_constr ~abort_on_undefined_evars:false evd (Retyping.get_type_of env evd (EConstr.of_constr c))
+      | Some t -> EConstr.of_constr t
+      | None -> Retyping.get_type_of env evd c
     in
-    Obligations.check_evars env evd;
     let obls, _, c, cty =
       Obligations.eterm_obligations env ident evd 0 c typ
     in