From 75514fe2207992ebc549822a7cbd5d37688690ac Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 8 May 2009 16:29:45 +0000 Subject: [PATCH] The relevance list can be shorter than leftno (when the default is used). --- helm/software/components/ng_kernel/nCicTypeChecker.ml | 4 +++- helm/software/components/ng_refiner/nCicRefiner.ml | 4 +++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 65f17ee38..8beca4cf0 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -730,7 +730,9 @@ and check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl = let sx_context_ty_rev,_ = HExtlib.split_nth leftno (List.rev context) in List.iter (fun (k_relev,_,te) -> - let _,k_relev = HExtlib.split_nth leftno k_relev in + let k_relev = + try snd (HExtlib.split_nth leftno k_relev) + with Failure _ -> k_relev in let te = debruijn uri len [] te in let context,te = NCicReduction.split_prods ~subst tys leftno te in let _,chopped_context_rev = diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index e38842ac8..d5270c192 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -617,7 +617,9 @@ let typeof_obj hdb let metasenv,subst,cl = List.fold_right (fun (k_relev,n,te) (metasenv,subst,res) -> - let _,k_relev = HExtlib.split_nth leftno k_relev in + let k_relev = + try snd (HExtlib.split_nth leftno k_relev) + with Failure _ -> k_relev in let te = NCicTypeChecker.debruijn uri len [] te in let context,te = NCicReduction.split_prods ~subst tys leftno te in let _,chopped_context_rev = -- 2.39.2