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.
---
 library/global.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/global.ml b/library/global.ml
index 44e4a9b7e1..d28ca0acc1 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -141,7 +141,7 @@ let body_of_constant_body access env cb =
   | Def c ->
     let u = match cb.const_universes with
     | Monomorphic _ -> Opaqueproof.PrivateMonomorphic ()
-    | Polymorphic _ -> Opaqueproof.PrivatePolymorphic Univ.ContextSet.empty
+    | Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty)
     in
     Some (Mod_subst.force_constr c, u, Declareops.constant_polymorphic_context cb)
   | OpaqueDef o ->
-- 
cgit v1.2.3