- hExtlib: added debugging information for split_nth

[helm.git] / helm / software / components / acic_procedural / procedural2.ml

diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml
index e41dd101b896b8f64bea8fbae0a22d6331d15c84..7ac82a0a63989326d736864adab9ca2e866d372f 100644 (file)
--- a/helm/software/components/acic_procedural/procedural2.ml
+++ b/helm/software/components/acic_procedural/procedural2.ml
@@ -64,8 +64,8 @@ let debug = ref false
 let split2_last l1 l2 =
 try
    let n = pred (List.length l1) in
-   let before1, after1 = HEL.split_nth n l1 in
-   let before2, after2 = HEL.split_nth n l2 in
+   let before1, after1 = HEL.split_nth "P2 1" n l1 in
+   let before2, after2 = HEL.split_nth "P2 2" n l2 in
    before1, before2, List.hd after1, List.hd after2
 with Invalid_argument _ -> failwith "A2P.split2_last"
    
@@ -388,7 +388,7 @@ and proc_case st what uri tyno u v ts =
       let qs = proc_bkd_proofs (next st) synth names classes ts in
       let lpsno, _ = H.get_ind_type uri tyno in
       let ps, _ = H.get_ind_parameters st.context (H.cic v) in
-      let _, rps = HEL.split_nth lpsno ps in
+      let _, rps = HEL.split_nth "P2 3" lpsno ps in
       let rpsno = List.length rps in 
       let e = Cn.mk_pattern rpsno u in
       let text = "" in