i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
pl true
else
+ let pl_and_cl =
+ try
+ List.combine pl cl
+ with
+ Invalid_argument _ ->
+ raise (TypeCheckerFailure "not enough patterns")
+ in
List.fold_right
(fun (p,(_,c)) i ->
let rl' =
in
i &&
check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
- ) (List.combine pl cl) true
+ ) pl_and_cl true
| C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
let (tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
pl true
else
+ let pl_and_cl =
+ try
+ List.combine pl cl
+ with
+ Invalid_argument _ ->
+ raise (TypeCheckerFailure "not enough patterns")
+ in
(*CSC: supponiamo come prima che nessun controllo sia necessario*)
(*CSC: sugli argomenti di una applicazione *)
List.fold_right
in
i &&
check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
- ) (List.combine pl cl) true
+ ) pl_and_cl true
| _ ->
List.fold_right
(fun p i ->
i && guarded_by_destructors context n nn kl x safes p)
pl true
else
+ let pl_and_cl =
+ try
+ List.combine pl cl
+ with
+ Invalid_argument _ ->
+ raise (TypeCheckerFailure "not enough patterns")
+ in
guarded_by_destructors context n nn kl x safes outtype &&
(*CSC: manca ??? il controllo sul tipo di term? *)
List.fold_right
in
i &&
guarded_by_destructors context' n' nn' kl x' safes' e
- ) (List.combine pl cl) true
+ ) pl_and_cl true
| C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
let (tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
i && guarded_by_destructors context n nn kl x safes p)
pl true
else
+ let pl_and_cl =
+ try
+ List.combine pl cl
+ with
+ Invalid_argument _ ->
+ raise (TypeCheckerFailure "not enough patterns")
+ in
guarded_by_destructors context n nn kl x safes outtype &&
(*CSC: manca ??? il controllo sul tipo di term? *)
List.fold_right
in
i &&
guarded_by_destructors context' n' nn' kl x' safes' e
- ) (List.combine pl cl) true
+ ) pl_and_cl true
| _ ->
guarded_by_destructors context n nn kl x safes outtype &&
guarded_by_destructors context n nn kl x safes term &&