The relevance list can be shorter than leftno (when the default is used).

[helm.git] / helm / software / components / ng_kernel / nCicTypeChecker.ml

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 65f17ee38ef4c356e4e5a5d1f6c3a3d16d36778c..8beca4cf0504285f32355529739aabfa73700e1a 100644 (file)
--- 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 =