From 4ceadecf179e9210eed42ef4847aa5ab8fa28bd6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 19 Jun 2019 21:17:09 +0200
Subject: Take advantage of the change of entry representation to split opacity
 status.

Mere isomorphism for now, but will allow more invariants ultimately.
---
 kernel/safe_typing.ml | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a980d22e42..c99edccda7 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -688,13 +688,21 @@ let constant_entry_of_side_effect eff =
     | OpaqueDef b -> b
     | Def b -> Mod_subst.force_constr b
     | _ -> assert false in
+  if Declareops.is_opaque cb then
+  OpaqueEntry {
+    const_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
+    const_entry_secctx = None;
+    const_entry_feedback = None;
+    const_entry_type = Some cb.const_type;
+    const_entry_universes = univs;
+    const_entry_inline_code = cb.const_inline_code }
+  else
   DefinitionEntry {
     const_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
     const_entry_secctx = None;
     const_entry_feedback = None;
     const_entry_type = Some cb.const_type;
     const_entry_universes = univs;
-    const_entry_opaque = Declareops.is_opaque cb;
     const_entry_inline_code = cb.const_inline_code }
 
 let export_eff eff =
-- 
cgit v1.2.3


From be3bba54e39a316ded975b7c5ac5723fed41aa88 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 19 Jun 2019 21:24:36 +0200
Subject: Enforce that transparent entries are forced beforehand.

---
 kernel/safe_typing.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index c99edccda7..ab58321ac7 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -698,7 +698,7 @@ let constant_entry_of_side_effect eff =
     const_entry_inline_code = cb.const_inline_code }
   else
   DefinitionEntry {
-    const_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
+    const_entry_body = (p, Univ.ContextSet.empty);
     const_entry_secctx = None;
     const_entry_feedback = None;
     const_entry_type = Some cb.const_type;
-- 
cgit v1.2.3


From bbec0ea51b4dfef1ddb09a2f876323aa1547f643 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 20 Jun 2019 08:14:28 +0200
Subject: Dedicated type for opaque entries in the kernel.

Even more invariants can be enforced this way.
---
 kernel/safe_typing.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ab58321ac7..5dac469a40 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -690,12 +690,12 @@ let constant_entry_of_side_effect eff =
     | _ -> assert false in
   if Declareops.is_opaque cb then
   OpaqueEntry {
-    const_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
-    const_entry_secctx = None;
-    const_entry_feedback = None;
-    const_entry_type = Some cb.const_type;
-    const_entry_universes = univs;
-    const_entry_inline_code = cb.const_inline_code }
+    opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
+    opaque_entry_secctx = None;
+    opaque_entry_feedback = None;
+    opaque_entry_type = Some cb.const_type;
+    opaque_entry_universes = univs;
+    opaque_entry_inline_code = cb.const_inline_code }
   else
   DefinitionEntry {
     const_entry_body = (p, Univ.ContextSet.empty);
-- 
cgit v1.2.3


From c20eb3a73c4868533bb50555d1979f5b9d821256 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 20 Jun 2019 08:22:28 +0200
Subject: Enforce that opaque entries carry their type.

---
 kernel/safe_typing.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 5dac469a40..6cb7a22a15 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -693,7 +693,7 @@ let constant_entry_of_side_effect eff =
     opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
     opaque_entry_secctx = None;
     opaque_entry_feedback = None;
-    opaque_entry_type = Some cb.const_type;
+    opaque_entry_type = cb.const_type;
     opaque_entry_universes = univs;
     opaque_entry_inline_code = cb.const_inline_code }
   else
-- 
cgit v1.2.3


From 5de7daa41e677798e4169a3e6350af0df12017e8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 20 Jun 2019 09:32:25 +0200
Subject: Remove the unused opaque_entry_inline_code field from opaque entries.

---
 kernel/safe_typing.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 6cb7a22a15..a0cc2974d9 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -695,7 +695,7 @@ let constant_entry_of_side_effect eff =
     opaque_entry_feedback = None;
     opaque_entry_type = cb.const_type;
     opaque_entry_universes = univs;
-    opaque_entry_inline_code = cb.const_inline_code }
+  }
   else
   DefinitionEntry {
     const_entry_body = (p, Univ.ContextSet.empty);
-- 
cgit v1.2.3