From 098781a2a1885a4f8768518a94b5026de9d375e6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 13 Jan 2015 05:51:36 +0530
Subject: Fix bug when discharging universe constraints coming from variables
 into monomorphic constants, which was still using the de Bruijn encoding Bug
 revealed by discharging of hidden internal monomorphic definition in
 otherwise polymorphic developments. Makes coqchk work on Hurkens again.

---
 kernel/cooking.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 4435b6ca1d..be71bd7b41 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -236,7 +236,13 @@ let cook_constant env { from = cb; info } =
 	proj_eta = etab, etat;
 	proj_type = ty'; proj_body = c' }
   in
-  let univs = UContext.union abs_ctx univs in
+  let univs = 
+    let abs' = 
+      if cb.const_polymorphic then abs_ctx
+      else instantiate_univ_context abs_ctx
+    in
+      UContext.union abs' univs
+  in
     (body, typ, Option.map projection cb.const_proj, 
      cb.const_polymorphic, univs, cb.const_inline_code, 
      Some const_hyps)
-- 
cgit v1.2.3