From 1e83ae578feea41d34c3ba26a1f74c3c715620a2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 22 May 2019 17:46:37 +0200
Subject: More precise type for Safe_typing export and inlining of private
 constants.

We get rid of the future wrappers, as all callers are immediately forcing
the result.
---
 proofs/pfedit.ml | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 52e15f466f..7333114eae 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -142,12 +142,11 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
   let gk = Global, poly, Proof Theorem in
   let ce, status, univs =
     build_constant_by_tactic id sigma sign ~goal_kind:gk typ tac in
-  let ce =
-    if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce
-    else { ce with
-      const_entry_body = Future.chain ce.const_entry_body
-        (fun (pt, _) -> pt, ()) } in
-  let (cb, ctx), () = Future.force ce.const_entry_body in
+  let body = Future.force ce.const_entry_body in
+  let (cb, ctx) =
+    if side_eff then Safe_typing.inline_private_constants env body
+    else fst body
+  in
   let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in
   cb, status, univs
 
@@ -197,5 +196,5 @@ let refine_by_tactic ~name ~poly env sigma ty tac =
      other goals that were already present during its invocation, so that
      those goals rely on effects that are not present anymore. Hopefully,
      this hack will work in most cases. *)
-  let ans = Safe_typing.inline_private_constants_in_constr env ans neff in
+  let (ans, _) = Safe_typing.inline_private_constants env ((ans, Univ.ContextSet.empty), neff) in
   ans, sigma
-- 
cgit v1.2.3