X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=07015ee8f984f33659bfa56e444397f6cde08ed1;hb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;hp=c38c15b931cdea943fda830e4097790503ef5501;hpb=68dbcd02022874a025a9444aa1125b0458816fbb;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index c38c15b93..07015ee8f 100644
--- 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))::_)