X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralOptimizer.ml;h=c5a27efc44942bbd8e7b028a99791779e9be9a47;hb=36270146f49052f621553b0b45afe23813ed7e64;hp=72cdab58c2a0ea200a33a463c04b315dedfbe866;hpb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index 72cdab58c..c5a27efc4 100644
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -148,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 "PO 1" csno vs in
+	          let vvs, vs = HEL.split_nth 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
@@ -185,13 +185,17 @@ 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 "PO 2" lpsno ps in
+   let lps, rps = HEL.split_nth 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 *)
       opt_mutcase_plain g st es c uri tyno outty arg cases
    else
    let predicate = clear_absts rpsno (1 - sort_disp) outty in   
+   if H.occurs c ~what:(C.Rel 0) ~where:predicate then
+(* FG: the transformation is not possible, we fall back into the plain case *)
+      opt_mutcase_plain g st es c uri tyno outty arg cases
+   else
    let is_recursive t =
       I.S.mem tyno (I.get_mutinds_of_uri uri t) 
    in
@@ -211,8 +215,13 @@ and opt_mutcase_critical g st es c uri tyno outty arg cases =
    in
    let lifted_cases = List.map2 map2 cases constructors in
    let args = eliminator :: lps @ predicate :: lifted_cases @ rps @ [arg] in
-   let x = H.refine c (C.Appl args) in
-   opt_proof g (info st "Optimizer: remove 3") es c x
+   try 
+      let x = H.refine c (C.Appl args) in
+      opt_proof g (info st "Optimizer: remove 3") es c x	 
+   with e ->
+(* FG: the transformation is not possible, we fall back into the plain case *)
+      let st = info st ("Optimizer: refine_error: " ^ Printexc.to_string e) in
+      opt_mutcase_plain g st es c uri tyno outty arg cases
 
 and opt_mutcase_plain g st es c uri tyno outty arg cases =
    let g st v =