X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FdestructTactic.ml;h=c658e2cc9beb75d66be75720b0306ef14efc8772;hb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;hp=f6fb61ac1ddf0e4a5511cf4c639bcc0bb0d17423;hpb=68dbcd02022874a025a9444aa1125b0458816fbb;p=helm.git

diff --git a/helm/software/components/tactics/destructTactic.ml b/helm/software/components/tactics/destructTactic.ml
index f6fb61ac1..c658e2cc9 100644
--- a/helm/software/components/tactics/destructTactic.ml
+++ b/helm/software/components/tactics/destructTactic.ml
@@ -305,7 +305,7 @@ let injection_tac ~lterm ~i ~continuation ~recur =
       let patterns,outtype =
         match fst (CicEnvironment.get_obj CU.oblivion_ugraph turi) with
         | C.InductiveDefinition (ind_type_list,_,paramsno,_)->
-           let left_params, right_params = HExtlib.split_nth paramsno params in
+           let left_params, right_params = HExtlib.split_nth "DT 1" paramsno params in
            let _,_,_,constructor_list = List.nth ind_type_list typeno in
            let i_constr_id,_ = List.nth constructor_list (consno - 1) in
            let patterns =
@@ -354,7 +354,7 @@ let injection_tac ~lterm ~i ~continuation ~recur =
                match S.lift 1 tty with
                | C.MutInd _ as tty' -> tty'
                | C.Appl l ->
-                   let keep,abstract = HExtlib.split_nth (paramsno +1) l in
+                   let keep,abstract = HExtlib.split_nth "DT 2" (paramsno +1) l in
                    let keep = List.map (S.lift paramsno) keep in
                    C.Appl (keep@mk_rels (List.length abstract))
                | _ -> assert false