- hExtlib: added debugging information for split_nth

[helm.git] / helm / software / components / tactics / destructTactic.ml

diff --git a/helm/software/components/tactics/destructTactic.ml b/helm/software/components/tactics/destructTactic.ml
index f6fb61ac1ddf0e4a5511cf4c639bcc0bb0d17423..c658e2cc9beb75d66be75720b0306ef14efc8772 100644 (file)
--- 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