From 371d69b334837c51d0dc998ddefbd072ac8dde2f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 18 Jun 2016 18:59:36 +0200
Subject: Fixing the checker.

I had to remove code handling the -type-in-type option introduced by commit
9c732a5. We should fix it at some point, but I am not sure that using the
checker with a system known to be blatantly inconsistent makes much sense
anyway.
---
 checker/typeops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker/typeops.ml')

diff --git a/checker/typeops.ml b/checker/typeops.ml
index da9842a8db..0c7e538be2 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -128,7 +128,7 @@ let sort_of_product env domsort rangsort =
     | (Prop _,  Prop Pos) -> rangsort
     (* Product rule (Type,Set,?) *)
     | (Type u1, Prop Pos) ->
-        if fst (engagement env) = ImpredicativeSet then
+        if engagement env = ImpredicativeSet then
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
         else
-- 
cgit v1.2.3