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