From 090fffa57b2235f70d4355f5dc85d73fa2634655 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 17 Nov 2014 18:09:48 +0100
Subject: Option -type-in-type continued (deactivate test for inferred sort of
 inductive types + deactivate test for equality of sort + deactivate the check
 that the constraints Prop/Set <= Type are declared).

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

(limited to 'pretyping/evarconv.ml')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 799ca25233..0dc7961103 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -711,7 +711,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	    (try
 	       let evd' =
 		 if pbty == CONV
-		 then Evd.set_eq_sort evd s1 s2
+		 then Evd.set_eq_sort env evd s1 s2
 		 else Evd.set_leq_sort env evd s1 s2
 	       in Success evd'
 	     with Univ.UniverseInconsistency p ->
-- 
cgit v1.2.3