From 66b098b04971f4bc08ce89afebdaec1772e3f73c Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 12 Mar 2013 23:59:24 +0000
Subject: A version of Univ.check_eq with no anomaly for Evd.set_eq_sort

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16274 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evd.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 0f709e454f..6efdf04559 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -574,8 +574,9 @@ let set_eq_sort ({evars = (sigma, (us, sm))} as d) s1 s2 =
       | Type u, Type v when (is_univ_level_var us u) || (is_univ_level_var us v) ->
 	  add_constraints d (Univ.enforce_eq u1 u2 Univ.empty_constraint)
       | Prop c, Type u when is_univ_var_or_set u &&
-	  Univ.check_eq sm u1 u2 -> d
-      | Type u, Prop c when is_univ_var_or_set u && Univ.check_eq sm u1 u2 -> d
+	  Univ.lax_check_eq sm u1 u2 -> d
+      | Type u, Prop c when is_univ_var_or_set u &&
+          Univ.lax_check_eq sm u1 u2 -> d
       | Type u, Type v when is_univ_var_or_set u && is_univ_var_or_set v ->
 	  add_constraints d (Univ.enforce_eq u1 u2 Univ.empty_constraint)
       | _, _ -> raise (Univ.UniverseInconsistency (Univ.Eq, u1, u2, []))
-- 
cgit v1.2.3