- match CicReduction.whd context te with
-(*
- C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> true
-*)
- C.Appl ((C.MutInd (uri',_,_))::tl) when UriManager.eq uri' uri -> true
- | C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true
- | C.Prod (name,source,dest) when
- does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest ->
- (* dummy abstraction, so we behave as in the anonimous case *)
- strictly_positive context n nn
- (subst_inductive_type_with_dummy_mutind source) &&
- weakly_positive ((Some (name,(C.Decl source)))::context)
- (n + 1) (nn + 1) uri dest
- | C.Prod (name,source,dest) ->
- does_not_occur context n nn
- (subst_inductive_type_with_dummy_mutind source)&&
- weakly_positive ((Some (name,(C.Decl source)))::context)
- (n + 1) (nn + 1) uri dest
- | _ ->
- raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
+ let rec aux context n nn te =
+ match CicReduction.whd context te with
+ | C.Appl (C.Sort C.Prop::tl) ->
+ List.for_all (does_not_occur context n nn) tl
+ | C.Sort C.Prop -> true
+ | C.Prod (name,source,dest) when
+ does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest ->
+ (* dummy abstraction, so we behave as in the anonimous case *)
+ strictly_positive context n nn source &&
+ weakly_positive ((Some (name,(C.Decl source)))::context)
+ (n + 1) (nn + 1) uri dest
+ | C.Prod (name,source,dest) ->
+ does_not_occur context n nn source &&
+ weakly_positive ((Some (name,(C.Decl source)))::context)
+ (n + 1) (nn + 1) uri dest
+ | _ ->
+ raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
+ in
+ aux context n nn (subst_inductive_type_with_dummy te)