From b6edcae7b61ea6ccc0e65223cecb71cab0dd55cc Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 8 Oct 2015 16:00:06 +0200
Subject: Univs: fix bug #3807

Add a flag to disallow minimization to set
---
 pretyping/evd.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'pretyping/evd.ml')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 412fb92b3d..3d912ca4ce 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1324,8 +1324,7 @@ let normalize_evar_universe_context uctx =
       Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables
         uctx.uctx_univ_algebraic
     in
-      if Univ.LSet.equal (fst us') (fst uctx.uctx_local) then 
-        uctx
+      if Univ.ContextSet.equal us' uctx.uctx_local then uctx
       else
 	let us', universes = Universes.refresh_constraints uctx.uctx_initial_universes us' in
 	let uctx' = 
-- 
cgit v1.2.3