- hExtlib: added debugging information for split_nth

[helm.git] / helm / software / components / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index c38c15b931cdea943fda830e4097790503ef5501..07015ee8f984f33659bfa56e444397f6cde08ed1 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -367,7 +367,7 @@ and weakly_positive context n nn uri indparamsno posuri te =
       C.MutInd (uri',0,_) when UriManager.eq uri' uri ->
        dummy
     | C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri ->
-       let _, rargs = HExtlib.split_nth leftno tl in
+       let _, rargs = HExtlib.split_nth "TC 1" leftno tl in
        if rargs = [] then dummy else Cic.Appl (dummy :: rargs)
     | C.Cast (te,ty) -> subst_inductive_type_with_dummy te
     | C.Prod (name,so,ta) ->
@@ -753,7 +753,7 @@ and specialize_inductive_type ~logger ~subst ~metasenv context t =
       let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
       (match o with
       | Cic.InductiveDefinition (tl,_,paramsno,_) ->
-          let left_args,_ = HExtlib.split_nth paramsno args in
+          let left_args,_ = HExtlib.split_nth "TC 2" paramsno args in
           List.map (fun (name, isind, arity, cl) ->
             let arity = CicSubstitution.subst_vars exp arity in
             let arity = instantiate_parameters left_args arity in
@@ -1081,7 +1081,7 @@ and guarded_by_constructors ~logger ~subst ~metasenv indURI =
          ("Too many args for constructor: " ^ String.concat " "
          (List.map (fun x-> CicPp.ppterm x) args))))
       in
-      let left, args = HExtlib.split_nth paramsno tl in
+      let left, args = HExtlib.split_nth "TC 3" paramsno tl in
       List.for_all (does_not_occur ~subst context n nn) left &&
       analyse_instantiated_type rec_params args
    | C.Appl ((C.MutCase (_,_,out,te,pl))::_)