From e12716e7877ff622ac5e15eda31de0b49bd6f681 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 4 Apr 2020 05:10:53 -0400
Subject: [declare] Remove dead code in prepare_obligation

---
 vernac/declare.ml | 13 ++++---------
 1 file changed, 4 insertions(+), 9 deletions(-)

diff --git a/vernac/declare.ml b/vernac/declare.ml
index c291890dce..030539c36b 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -1011,19 +1011,14 @@ let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma =
   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
-  let ce = definition_entry ?opaque ?inline ?types ~univs body in
   let env = Global.env () in
-  let (c,ctx), sideff = Future.force ce.proof_entry_body in
-  assert(Safe_typing.is_empty_private_constants sideff.Evd.seff_private);
-  assert(Univ.ContextSet.is_empty ctx);
   RetrieveObl.check_evars env sigma;
-  let c = EConstr.of_constr c in
-  let typ = match ce.proof_entry_type with
+  let body = EConstr.of_constr body in
+  let typ = match types with
     | Some t -> EConstr.of_constr t
-    | None -> Retyping.get_type_of env sigma c
+    | None -> Retyping.get_type_of env sigma body
   in
-  let obls, _, c, cty = RetrieveObl.retrieve_obligations env name sigma 0 c typ in
+  let obls, _, c, cty = RetrieveObl.retrieve_obligations env name sigma 0 body typ in
   let uctx = Evd.evar_universe_context sigma in
   c, cty, uctx, obls
 
-- 
cgit v1.2.3