From 95d294fede1d581cec2913991961b332acfea8b3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 13 Feb 2020 16:36:35 +0100
Subject: Also check for monomorphic universes in side-effects certificates.

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

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 1f97497d60..0f92af48cb 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -262,18 +262,24 @@ struct
 
 type t = {
   certif_struc : Declarations.structure_body;
+  certif_univs : Univ.ContextSet.t;
 }
 
 let make senv = {
   certif_struc = senv.revstruct;
+  certif_univs = senv.univ;
 }
 
 let is_suffix l suf = match l with
 | [] -> false
 | _ :: l -> l == suf
 
+let is_subset (s1, cst1) (s2, cst2) =
+  Univ.LSet.subset s1 s2 && Univ.Constraint.subset cst1 cst2
+
 let check ~src ~dst =
-  is_suffix dst.certif_struc src.certif_struc
+  is_suffix dst.certif_struc src.certif_struc &&
+  is_subset src.certif_univs dst.certif_univs
 
 end
 
-- 
cgit v1.2.3