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

[helm.git] / helm / software / components / ng_refiner / nCicRefiner.ml

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 =