- hExtlib: added debugging information for split_nth

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

diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index 0364803c73d82c8552aa4e01b9e3b7d6b1c1f165..72cdab58c2a0ea200a33a463c04b315dedfbe866 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -99,7 +99,9 @@ let rec opt_letin g st es c name v w t =
          | v when H.is_proof c v && H.is_atomic v          ->
            let x = S.subst v t in
            opt_proof g (info st "Optimizer: remove 5") true c x 
-        | v                                               ->
+(*      | v when t = C.Rel 1                              ->
+           g (info st "Optimizer: remove 6") v 
+*)      | v                                               ->
            g st (C.LetIn (name, v, w, t))
       in
       if es then opt_term g st es c v else g st v
@@ -146,7 +148,7 @@ and opt_appl g st es c t vs =
               let classes, conclusion = Cl.classify c (H.get_type "opt_appl 3" c t) in
               let csno, vsno = List.length classes, List.length vs in
               if csno < vsno then
-                 let vvs, vs = HEL.split_nth csno vs in
+                 let vvs, vs = HEL.split_nth "PO 1" csno vs in
                  let x = C.Appl (define c (C.Appl (t :: vvs)) :: vs) in
                  opt_proof g (info st "Optimizer: anticipate 2") true c x
               else match conclusion, List.rev vs with
@@ -183,7 +185,7 @@ and opt_mutcase_critical g st es c uri tyno outty arg cases =
    let eliminator = H.get_default_eliminator c uri tyno outty in
    let lpsno, (_, _, _, constructors) = H.get_ind_type uri tyno in
    let ps, sort_disp = H.get_ind_parameters c arg in
-   let lps, rps = HEL.split_nth lpsno ps in
+   let lps, rps = HEL.split_nth "PO 2" lpsno ps in
    let rpsno = List.length rps in
    if rpsno = 0 && sort_disp = 0 then
 (* FG: the transformation is not possible, we fall back into the plain case *)