Checker was forgetting to register global universes introduced by opaque

proofs.

5 files changed, 15 insertions, 13 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 2bc470aea..21c8f1c5b 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -46,7 +46,7 @@ type library_t = {
   library_opaques : Cic.opaque_table;
   library_deps : Cic.library_deps;
   library_digest : Cic.vodigest;
-  library_extra_univs : Univ.constraints }
+  library_extra_univs : Univ.ContextSet.t }
 
 module LibraryOrdered =
   struct
@@ -97,7 +97,7 @@ let access_opaque_univ_table dp i =
     let t = LibraryMap.find dp !opaque_univ_tables in
     assert (i < Array.length t);
     Future.force t.(i)
-  with Not_found -> Univ.empty_constraint
+  with Not_found -> Univ.ContextSet.empty
 
 
 let _ = Declarations.indirect_opaque_access := access_opaque_table
@@ -347,9 +347,8 @@ let intern_from_file (dir, f) =
       LibraryMap.add sd.md_name opaque_csts !opaque_univ_tables)
     opaque_csts;
   let extra_cst =
-    Option.default Univ.empty_constraint
-      (Option.map (fun (_,cs,_) ->
-         Univ.ContextSet.constraints cs) opaque_csts) in
+    Option.default Univ.ContextSet.empty
+      (Option.map (fun (_,cs,_) -> cs) opaque_csts) in
   mk_library sd md f table digest extra_cst
 
 let get_deps (dir, f) =
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 36e6a7cab..32d1713a8 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -426,7 +426,7 @@ let subst_lazy_constr sub = function
 let indirect_opaque_access =
   ref ((fun dp i -> assert false) : DirPath.t -> int -> constr)
 let indirect_opaque_univ_access =
-  ref ((fun dp i -> assert false) : DirPath.t -> int -> Univ.constraints)
+  ref ((fun dp i -> assert false) : DirPath.t -> int -> Univ.ContextSet.t)
 
 let force_lazy_constr = function
   | Indirect (l,dp,i) ->
@@ -435,7 +435,7 @@ let force_lazy_constr = function
 
 let force_lazy_constr_univs = function
   | OpaqueDef (Indirect (l,dp,i)) -> !indirect_opaque_univ_access dp i
-  | _ -> Univ.empty_constraint
+  | _ -> Univ.ContextSet.empty
 
 let subst_constant_def sub = function
   | Undef inl -> Undef inl
@@ -457,6 +457,8 @@ let is_opaque cb = match cb.const_body with
   | OpaqueDef _ -> true
   | Def _ | Undef _ -> false
 
+let opaque_univ_context cb = force_lazy_constr_univs cb.const_body
+
 let subst_rel_declaration sub (id,copt,t as x) =
   let copt' = Option.smartmap (subst_mps sub) copt in
   let t' = subst_mps sub t in
diff --git a/checker/declarations.mli b/checker/declarations.mli
index 3c6db6ab7..456df8369 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -2,17 +2,18 @@ open Names
 open Cic
 
 val force_constr : constr_substituted -> constr
-val force_lazy_constr_univs : Cic.constant_def -> Univ.constraints
+val force_lazy_constr_univs : Cic.constant_def -> Univ.ContextSet.t
 val from_val : constr -> constr_substituted
 
 val indirect_opaque_access : (DirPath.t -> int -> constr) ref
-val indirect_opaque_univ_access : (DirPath.t -> int -> Univ.constraints) ref
+val indirect_opaque_univ_access : (DirPath.t -> int -> Univ.ContextSet.t) ref
 
 (** Constant_body *)
 
 val body_of_constant : constant_body -> constr option
 val constant_has_body : constant_body -> bool
 val is_opaque : constant_body -> bool
+val opaque_univ_context : constant_body -> Univ.ContextSet.t
 
 (* Mutual inductives *)
 
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index d3bc8373a..81a3cc035 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -28,7 +28,7 @@ let set_engagement c =
 let full_add_module dp mb univs digest =
   let env = !genv in
   let env = push_context_set ~strict:true mb.mod_constraints env in
-  let env = add_constraints univs env in
+  let env = push_context_set ~strict:true univs env in
   let env = Modops.add_module mb env in
   genv := add_digest env dp digest
 
@@ -83,7 +83,7 @@ let import file clib univs digest =
   check_engagement env clib.comp_enga;
   let mb = clib.comp_mod in
   Mod_checking.check_module
-    (add_constraints univs
+    (push_context_set ~strict:true univs
       (push_context_set ~strict:true mb.mod_constraints env)) mb.mod_mp mb;
   stamp_library file digest;
   full_add_module clib.comp_name mb univs digest
diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli
index e16e64e6a..892a8d2cc 100644
--- a/checker/safe_typing.mli
+++ b/checker/safe_typing.mli
@@ -15,6 +15,6 @@ val get_env : unit -> env
 
 val set_engagement : engagement -> unit
 val import         :
-  CUnix.physical_path -> compiled_library -> Univ.constraints -> Cic.vodigest -> unit
+  CUnix.physical_path -> compiled_library -> Univ.ContextSet.t -> Cic.vodigest -> unit
 val unsafe_import  :
-  CUnix.physical_path -> compiled_library -> Univ.constraints -> Cic.vodigest -> unit
+  CUnix.physical_path -> compiled_library -> Univ.ContextSet.t -> Cic.vodigest -> unit