- let debrujinedte = debrujin_constructor uri len [] te in
- let augmented_term =
- List.fold_right
- (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
- itl debrujinedte
- in
- let _,ugraph' = type_of ~logger augmented_term ugraph in
+ let te = debrujin_constructor uri len [] te in
+ let context,te = split_prods ~subst:[] tys indparamsno te in
+ let con_sort,ugraph = type_of_aux' ~logger [] context te ugraph in
+ let ugraph =
+ match
+ CicReduction.whd context con_sort, CicReduction.whd [] ty_sort
+ with
+ 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: "^
+ CicPp.ppterm a ^ " --- " ^ CicPp.ppterm b))) in