From 371d69b334837c51d0dc998ddefbd072ac8dde2f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
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/indtypes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker/indtypes.ml')

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index a667bb8a3..29b16392b 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -176,7 +176,7 @@ let typecheck_arity env params inds =
 (* Allowed eliminations *)
 
 let check_predicativity env s small level =
-  match s, fst (engagement env) with
+  match s, engagement env with
       Type u, _ ->
         (* let u' = fresh_local_univ () in *)
         (* let cst = *)
-- 
cgit v1.2.3