From 23fa8cfe44a11df5a93d349e2520011e6722e096 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 17 May 2008 18:50:09 +0000 Subject: [PATCH] impredicative Set is considered as Prop in the new check implemented by CSC --- .../components/cic_proof_checking/cicTypeChecker.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 6cbb44f80..fd2819738 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -575,12 +575,14 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = Cic.Sort (Cic.Type u1), Cic.Sort (Cic.Type u2) -> CicUniv.add_ge u2 u1 ugraph | Cic.Sort _, Cic.Sort Cic.Prop + | Cic.Sort _, Cic.Sort Cic.Set | Cic.Sort Cic.CProp, Cic.Sort Cic.CProp | Cic.Sort _, Cic.Sort Cic.Type _ -> ugraph - | _, _ -> + | a,b -> raise (TypeCheckerFailure - (lazy ("Wrong constructor or inductive arity shape"))) in + (lazy ("Wrong constructor or inductive arity shape: "^ + CicPp.ppterm a ^ " --- " ^ CicPp.ppterm b))) in (* let's check also the positivity conditions *) if not -- 2.39.2