]> matita.cs.unibo.it Git - helm.git/commitdiff
impredicative Set is considered as Prop in the new check implemented by CSC
authorEnrico Tassi <enrico.tassi@inria.fr>
Sat, 17 May 2008 18:50:09 +0000 (18:50 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Sat, 17 May 2008 18:50:09 +0000 (18:50 +0000)
helm/software/components/cic_proof_checking/cicTypeChecker.ml

index 6cbb44f8044432db90ae2cd361d2831cb132be8d..fd2819738af77561725d77067926a694b90b9480 100644 (file)
@@ -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