From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 17 May 2008 18:50:09 +0000 (+0000)
Subject: impredicative Set is considered as Prop in the new check implemented by CSC
X-Git-Tag: make_still_working~5178
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=23fa8cfe44a11df5a93d349e2520011e6722e096;p=helm.git

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 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