From 77839ae306380e99a8ceac0bf26ff86ec9159346 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 18 Jun 2014 12:04:42 +0200
Subject: Code factorization in LMap.

---
 pretyping/evd.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 53d1a8a0e6..8b9631b4bd 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -966,7 +966,7 @@ let merge_uctx rigid uctx ctx' =
     | UnivRigid -> uctx
     | UnivFlexible b ->
       let uvars' = Univ.LMap.subst_union uctx.uctx_univ_variables 
-	(Univ.LMap.of_set (Univ.ContextSet.levels ctx') None) in
+	(Univ.LMap.bind (fun _ -> None) (Univ.ContextSet.levels ctx')) in
 	if b then
 	  { uctx with uctx_univ_variables = uvars';
 	  uctx_univ_algebraic = Univ.LSet.union uctx.uctx_univ_algebraic 
-- 
cgit v1.2.3