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


From d97499e1dc8644821a0b9d70bf4dcd479bd1df26 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 4 Apr 2020 05:17:20 -0400
Subject: [declare] Minor tweaks in prepare_obligation

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

diff --git a/vernac/declare.ml b/vernac/declare.ml
index 030539c36b..0b03a63d09 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -1008,19 +1008,19 @@ let declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook
   declare_entry ~name ~scope ~kind ~impargs ?obls ?hook ~uctx entry
 
 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 env = Global.env () in
-  RetrieveObl.check_evars env sigma;
-  let body = EConstr.of_constr body in
-  let typ = match types with
-    | Some t -> EConstr.of_constr t
+  let types = match types with
+    | Some t -> t
     | None -> Retyping.get_type_of env sigma body
   in
-  let obls, _, c, cty = RetrieveObl.retrieve_obligations env name sigma 0 body typ in
+  let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false
+      sigma (fun nf -> nf body, nf types)
+  in
+  RetrieveObl.check_evars env sigma;
+  let body, types = EConstr.(of_constr body, of_constr types) in
+  let obls, _, body, cty = RetrieveObl.retrieve_obligations env name sigma 0 body types in
   let uctx = Evd.evar_universe_context sigma in
-  c, cty, uctx, obls
+  body, cty, uctx, obls
 
 let prepare_parameter ~poly ~udecl ~types sigma =
   let env = Global.env () in
-- 
cgit v1.2.3


From 0643873397552cc2fe4d1486c14f206968dea672 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 4 Apr 2020 05:20:46 -0400
Subject: [declare] Remove unused parameters in prepare_obligation

---
 vernac/comDefinition.ml | 2 +-
 vernac/declare.ml       | 2 +-
 vernac/declare.mli      | 6 +-----
 3 files changed, 3 insertions(+), 7 deletions(-)

diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index eac8f92e2e..d56917271c 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -126,7 +126,7 @@ let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c c
   let (body, types), evd, udecl, impargs =
     interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
   in
-  let term, ty, uctx, obls = Declare.prepare_obligation ~name ~poly ~body ~types ~udecl evd in
+  let term, ty, uctx, obls = Declare.prepare_obligation ~name ~body ~types evd in
   let _ : Declare.Obls.progress =
     Obligations.add_definition
       ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 0b03a63d09..3ffde76790 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -1007,7 +1007,7 @@ let declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook
   let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in
   declare_entry ~name ~scope ~kind ~impargs ?obls ?hook ~uctx entry
 
-let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma =
+let prepare_obligation ~name ~types ~body sigma =
   let env = Global.env () in
   let types = match types with
     | Some t -> t
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 82b0cff8d9..62bc6a34bf 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -367,11 +367,7 @@ val declare_mutually_recursive
 
 (** Prepare API, to be removed once we provide the corresponding 1-step API *)
 val prepare_obligation
-  :  ?opaque:bool
-  -> ?inline:bool
-  -> name:Id.t
-  -> poly:bool
-  -> udecl:UState.universe_decl
+  :  name:Id.t
   -> types:EConstr.t option
   -> body:EConstr.t
   -> Evd.evar_map
-- 
cgit v1.2.3