From fd8357fad3f4d608f62afce848a4d4bf1bbb3d70 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 4 Aug 2014 23:30:55 +0200
Subject: Small code simplification.

---
 pretyping/evd.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index a003716f9b..cd02d7228a 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -959,12 +959,12 @@ let merge_uctx rigid uctx ctx' =
     match rigid with
     | UnivRigid -> uctx
     | UnivFlexible b ->
-      let uvars' = Univ.LMap.subst_union uctx.uctx_univ_variables 
-	(Univ.LMap.bind (fun _ -> None) (Univ.ContextSet.levels ctx')) in
+      let levels = Univ.ContextSet.levels ctx' in
+      let uvars' = Univ.LMap.bind (fun _ -> None) levels in
+      let uvars' = Univ.LMap.fold Univ.LMap.add uctx.uctx_univ_variables uvars' in
 	if b then
 	  { uctx with uctx_univ_variables = uvars';
-	  uctx_univ_algebraic = Univ.LSet.union uctx.uctx_univ_algebraic 
-	      (Univ.ContextSet.levels ctx') }
+	  uctx_univ_algebraic = Univ.LSet.union uctx.uctx_univ_algebraic levels }
 	else { uctx with uctx_univ_variables = uvars' }
   in
     { uctx with uctx_local = Univ.ContextSet.union uctx.uctx_local ctx';
-- 
cgit v1.2.3