From 19da31e8e92bb9990e90af162ce1652c6ac71977 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 28 May 2019 15:19:25 +0200
Subject: Checker: don't use monomorphic universes attached to a constant

They are supposed to be included in the module's constraints.

The old behaviour would allow a crafted vo, using
~~~coq
Definition a := Type.
Definition b := Type.

Definition b_in_a : a := b.
Definition a_in_b : b := a.
~~~
with the constraints for b_in_a and a_in_b not included in the module
constraints, then a proof of false may be derived in the usual way.
---
 checker/mod_checking.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 1cf07e7cc7..c450ff854c 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -24,7 +24,7 @@ let check_constant_declaration env kn cb =
   (* [env'] contains De Bruijn universe variables *)
   let poly, env' =
     match cb.const_universes with
-    | Monomorphic ctx -> false, push_context_set ~strict:true ctx env
+    | Monomorphic ctx -> false, env
     | Polymorphic auctx ->
       let ctx = Univ.AUContext.repr auctx in
       let env = push_context ~strict:false ctx env in
-- 
cgit v1.2.3