impredicative Set is considered as Prop in the new check implemented by CSC

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 6cbb44f8044432db90ae2cd361d2831cb132be8d..fd2819738af77561725d77067926a694b90b9480 100644 (file)
--- 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