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/uState.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'engine/uState.ml')

diff --git a/engine/uState.ml b/engine/uState.ml
index 99ac5f2ce8..7c60d8317c 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -63,6 +63,8 @@ let make ~lbound u =
     uctx_universes_lbound = lbound;
     uctx_initial_universes = u}
 
+let from_env e = make ~lbound:(Environ.universes_lbound e) (Environ.universes e)
+
 let is_empty ctx =
   ContextSet.is_empty ctx.uctx_local &&
     LMap.is_empty ctx.uctx_univ_variables
-- 
cgit v1.2.3