From 9c732a5c878bac2592cb397aca3d17cfefdcd023 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 10 Jul 2015 01:13:59 +0200 Subject: Option -type-in-type: added support in checker and making it contaminating in vo files (this was not done yet in 24d0027f0 and 090fffa57b). Reused field "engagement" to carry information about both impredicativity of set and type in type. For the record: maybe some further checks to do around the sort of the inductive types in coqchk? --- checker/indtypes.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'checker/indtypes.ml') diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 050c33e60..e1a6bc7c1 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, engagement env with + match s, fst (engagement env) with Type u, _ -> (* let u' = fresh_local_univ () in *) (* let cst = *) @@ -184,7 +184,7 @@ let check_predicativity env s small level = (* (universes env) in *) if not (Univ.check_leq (universes env) level u) then failwith "impredicative Type inductive type" - | Prop Pos, Some ImpredicativeSet -> () + | Prop Pos, ImpredicativeSet -> () | Prop Pos, _ -> if not small then failwith "impredicative Set inductive type" | Prop Null,_ -> () -- cgit v1.2.3