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

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 =

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index e38842ac82c57c6c454582438a5726f6f89ba86a..d5270c192c1191e4b1926b8ce2484a2758530237 100644 (file)
--- 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 =