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.
---
 kernel/term_typing.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/term_typing.ml')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 9ec3269375..6c065292d4 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -181,7 +181,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         let _ = Typeops.judge_of_cast env j DEFAULTcast tj in
         let def = Vars.subst_univs_level_constr usubst j.uj_val in
         let () = feedback_completion_typecheck feedback_id in
-        def, Opaqueproof.PrivatePolymorphic private_univs
+        def, Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, private_univs)
       end in
       let def = OpaqueDef proofterm in
       let typ = Vars.subst_univs_level_constr usubst tj.utj_val in
@@ -402,7 +402,7 @@ let translate_local_def env _id centry =
         the body by virtue of the typing of [Entries.section_def_entry]. *)
     let () = match cst with
     | Opaqueproof.PrivateMonomorphic ctx -> assert (Univ.ContextSet.is_empty ctx)
-    | Opaqueproof.PrivatePolymorphic ctx -> assert (Univ.ContextSet.is_empty ctx)
+    | Opaqueproof.PrivatePolymorphic (_, ctx) -> assert (Univ.ContextSet.is_empty ctx)
     in
     p
   | Undef _ | Primitive _ -> assert false
-- 
cgit v1.2.3