From 4457e6d75affd20c1c13c0d798c490129525bcb5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 4 Jul 2017 13:38:22 +0200
Subject: More precise type for universe entries.

We use an algebraic type instead of a pair of a boolean and the corresponding
data. For now, this is isomorphic, but this allows later change in the structure.
---
 proofs/proof_global.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 52d6787d44..2ade797f63 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -378,6 +378,10 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
       let t = EConstr.Unsafe.to_constr t in
       let univstyp, body = make_body t p in
       let univs, typ = Future.force univstyp in
+      let univs =
+        if poly then Entries.Polymorphic_const_entry univs
+        else Entries.Monomorphic_const_entry univs
+      in
 	{ Entries.
 	  const_entry_body = body;
 	  const_entry_secctx = section_vars;
@@ -386,7 +390,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
 	  const_entry_inline_code = false;
 	  const_entry_opaque = true;
 	  const_entry_universes = univs;
-	  const_entry_polymorphic = poly})
+        })
 		fpl initial_goals in
   let binders =
     Option.map (fun names -> fst (Evd.universe_context ~names (Evd.from_ctx universes)))
-- 
cgit v1.2.3


From 665256fec8465ff0adb943063c25f07a6ca54618 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 18 Jul 2017 18:16:43 +0200
Subject: Statically ensuring that inlined entries out of the kernel have no
 effects.

This was an easy to prove property that I somehow overlooked.
---
 proofs/pfedit.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index a949c8e911..1937885587 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -157,10 +157,9 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
     if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce
     else { ce with
       const_entry_body = Future.chain ~pure:true ce.const_entry_body
-        (fun (pt, _) -> pt, Safe_typing.empty_private_constants) } in
-  let (cb, ctx), se = Future.force ce.const_entry_body in
+        (fun (pt, _) -> pt, ()) } in
+  let (cb, ctx), () = Future.force ce.const_entry_body in
   let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in
-  assert(Safe_typing.empty_private_constants = se);
   cb, status, Evd.evar_universe_context univs'
 
 let refine_by_tactic env sigma ty tac =
-- 
cgit v1.2.3