From 5316d205993bb3fe3f69e8984fe53d4d50aa8d2a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 4 Jun 2019 13:44:05 +0200
Subject: Allow to delay polymorphic opaque constants.

We had to move the private opaque constraints out of the constant declaration
into the opaque table. The API is not very pretty yet due to a pervasive
confusion between monomorphic global constraints and polymorphic local ones,
but once we get rid of futures in the kernel this should be magically solved.
---
 stm/stm.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index d77e37c910..bae51d1794 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1746,14 +1746,18 @@ end = struct (* {{{ *)
            the call to [check_task_aux] above. *)
         let uc = Opaqueproof.force_constraints Library.indirect_accessor (Global.opaque_tables ()) o in
         let uc = Univ.hcons_universe_context_set uc in
-        let (pr, ctx) = Option.get (Global.body_of_constant_body Library.indirect_accessor c) in
+        let (pr, priv, ctx) = Option.get (Global.body_of_constant_body Library.indirect_accessor c) in
         (* We only manipulate monomorphic terms here. *)
         let () = assert (Univ.AUContext.is_empty ctx) in
+        let () = match priv with
+        | Opaqueproof.PrivateMonomorphic () -> ()
+        | Opaqueproof.PrivatePolymorphic ctx -> assert (Univ.ContextSet.is_empty ctx)
+        in
         let pr = Constr.hcons pr in
         let (ci, univs, dummy) = p.(bucket) in
         let () = assert (Option.is_empty dummy) in
         let () = assert (Int.equal (Univ.AUContext.size ctx) univs) in
-        p.(bucket) <- ci, univs, Some pr;
+        p.(bucket) <- ci, univs, Some (pr, priv);
         Univ.ContextSet.union cst uc, false
 
   let check_task name l i =
-- 
cgit v1.2.3


From a69bb15b1d76b71628b61bc42eb8d79c098074a8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 10 Jun 2019 12:27:37 +0200
Subject: Merge universe quantification and delayed constraints in opaque
 proofs.

This enforces more invariants statically.
---
 stm/stm.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index bae51d1794..6577309909 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1751,13 +1751,14 @@ end = struct (* {{{ *)
         let () = assert (Univ.AUContext.is_empty ctx) in
         let () = match priv with
         | Opaqueproof.PrivateMonomorphic () -> ()
-        | Opaqueproof.PrivatePolymorphic ctx -> assert (Univ.ContextSet.is_empty ctx)
+        | Opaqueproof.PrivatePolymorphic (univs, uctx) ->
+          let () = assert (Int.equal (Univ.AUContext.size ctx) univs) in
+          assert (Univ.ContextSet.is_empty uctx)
         in
         let pr = Constr.hcons pr in
-        let (ci, univs, dummy) = p.(bucket) in
+        let (ci, dummy) = p.(bucket) in
         let () = assert (Option.is_empty dummy) in
-        let () = assert (Int.equal (Univ.AUContext.size ctx) univs) in
-        p.(bucket) <- ci, univs, Some (pr, priv);
+        p.(bucket) <- ci, Some (pr, priv);
         Univ.ContextSet.union cst uc, false
 
   let check_task name l i =
-- 
cgit v1.2.3