From c8e7ffe08e119132bec097424f21b4570150893b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 18 May 2020 18:40:26 +0200
Subject: [universes] [api] Provide UState.from_env

This seems like a recurring pattern, and IMO makes a bit better API.

We also remove `merge_universe_subst` as it is not needed so far, as
we were creating stale `evar_map`s just for this purpose.
---
 engine/evd.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index 5642145f6d..ff13676818 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -697,8 +697,7 @@ let empty = {
   extras = Store.empty;
 }
 
-let from_env e =
-  { empty with universes = UState.make ~lbound:(Environ.universes_lbound e) (Environ.universes e) }
+let from_env e = { empty with universes = UState.from_env e }
 
 let from_ctx ctx = { empty with universes = ctx }
 
@@ -862,9 +861,6 @@ let universe_subst evd =
 let merge_context_set ?loc ?(sideff=false) rigid evd ctx' =
   {evd with universes = UState.merge ?loc ~sideff rigid evd.universes ctx'}
 
-let merge_universe_subst evd subst =
-  {evd with universes = UState.merge_subst evd.universes subst }
-
 let with_context_set ?loc rigid d (a, ctx) =
   (merge_context_set ?loc rigid d ctx, a)
 
-- 
cgit v1.2.3