From adb721441e9ff9bf7cdb1b4603628d95ca1f016a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 17 Mar 2015 18:44:23 +0100
Subject: Add function to fix the non-substituted universe variables of an
 evar_map.

---
 pretyping/evd.ml | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'pretyping/evd.ml')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 454c51195b..bf519fb7c0 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1189,6 +1189,18 @@ let abstract_undefined_variables uctx =
   in { uctx with uctx_local = Univ.ContextSet.empty;
       uctx_univ_algebraic = vars' }
 
+let fix_undefined_variables ({ universes = uctx } as evm) =
+  let algs', vars' = 
+    Univ.LMap.fold (fun u v (algs, vars as acc) ->
+      if v == None then (Univ.LSet.remove u algs, Univ.LMap.remove u vars)
+      else acc)
+      uctx.uctx_univ_variables 
+      (uctx.uctx_univ_algebraic, uctx.uctx_univ_variables)
+  in
+    {evm with universes = 
+	{ uctx with uctx_univ_variables = vars';
+	  uctx_univ_algebraic = algs' } }
+
 
 let refresh_undefined_univ_variables uctx =
   let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in
-- 
cgit v1.2.3