Merge branch 'v8.5'

4 files changed, 15 insertions, 0 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index ce3e91db7f..40409fe7fd 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -940,6 +940,9 @@ let add_universe_name evd s l =
 
 let universes evd = UState.ugraph evd.universes
 
+let update_sigma_env evd env =
+  { evd with universes = UState.update_sigma_env evd.universes env }
+
 (* Conversion w.r.t. an evar map and its local universes. *)
 
 let conversion_gen env evd pb t u =
diff --git a/engine/evd.mli b/engine/evd.mli
index b295a431aa..3a95b77f06 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -558,6 +558,8 @@ val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_sub
 
 val nf_constraints : evar_map -> evar_map
 
+val update_sigma_env : evar_map -> env -> evar_map
+
 (** Polymorphic universes *)
 
 val fresh_sort_in_family : ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts
diff --git a/engine/uState.ml b/engine/uState.ml
index 61ab5a8fca..0901d81e9e 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -465,3 +465,11 @@ let universe_of_name uctx s =
 let add_universe_name uctx s l =
   let names' = add_uctx_names s l uctx.uctx_names in
   { uctx with uctx_names = names' }
+
+let update_sigma_env uctx env =
+  let univs = Environ.universes env in
+  let eunivs =
+    { uctx with uctx_initial_universes = univs;
+                         uctx_universes = univs }
+  in
+  merge true univ_rigid eunivs eunivs.uctx_local
diff --git a/engine/uState.mli b/engine/uState.mli
index 6861035fac..3a6f77e14e 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -110,6 +110,8 @@ val normalize : t -> t
 
 val universe_context : ?names:(Id.t Loc.located) list -> t -> (Id.t * Univ.Level.t) list * Univ.universe_context
 
+val update_sigma_env : t -> Environ.env -> t
+
 (** {5 Pretty-printing} *)
 
 val pr_uctx_level : t -> Univ.Level.t -> Pp.std_ppcmds