Merge universe quantification and delayed constraints in opaque proofs.

This enforces more invariants statically.

1 files changed, 8 insertions, 11 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 596fcd210c..7e7734b247 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -728,7 +728,8 @@ let export_side_effects mb env (b_ctx, eff) =
               let map cu =
                 let (c, u) = Future.force cu in
                 let () = match u with
-                | Opaqueproof.PrivateMonomorphic ctx | Opaqueproof.PrivatePolymorphic ctx ->
+                | Opaqueproof.PrivateMonomorphic ctx
+                | Opaqueproof.PrivatePolymorphic (_, ctx) ->
                   assert (Univ.ContextSet.is_empty ctx)
                 in
                 c
@@ -748,11 +749,11 @@ let export_side_effects mb env (b_ctx, eff) =
 let export_private_constants ~in_section ce senv =
   let exported, ce = export_side_effects senv.revstruct senv.env ce in
   let map univs p =
-    let univs, local = match univs with
-    | Monomorphic _ -> 0, Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty
-    | Polymorphic auctx -> Univ.AUContext.size auctx, Opaqueproof.PrivatePolymorphic Univ.ContextSet.empty
+    let local = match univs with
+    | Monomorphic _ -> Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty
+    | Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty)
     in
-    Opaqueproof.create ~univs (Future.from_val (p, local))
+    Opaqueproof.create (Future.from_val (p, local))
   in
   let map (kn, cb) = (kn, map_constant (fun c -> map cb.const_universes c) cb) in
   let bodies = List.map map exported in
@@ -781,11 +782,7 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen
         Term_typing.translate_constant Term_typing.Pure senv.env kn ce
     in
   let senv =
-    let univs = match cb.const_universes with
-    | Monomorphic _ -> 0
-    | Polymorphic auctx -> Univ.AUContext.size auctx
-    in
-    let cb = map_constant (fun c -> Opaqueproof.create ~univs c) cb in
+    let cb = map_constant (fun c -> Opaqueproof.create c) cb in
     add_constant_aux ~in_section senv (kn, cb) in
   let senv =
     match decl with
@@ -805,7 +802,7 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen
       match cb.const_universes, delayed with
       | Monomorphic ctx', Opaqueproof.PrivateMonomorphic ctx ->
         OpaqueDef b, Monomorphic (Univ.ContextSet.union ctx ctx')
-      | Polymorphic auctx, Opaqueproof.PrivatePolymorphic ctx ->
+      | Polymorphic auctx, Opaqueproof.PrivatePolymorphic (_, ctx) ->
         (* Upper layers enforce that there are no internal constraints *)
         let () = assert (Univ.ContextSet.is_empty ctx) in
         OpaqueDef b, Polymorphic auctx