X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralOptimizer.ml;h=2faade402402068c51a1137976cd2c91facd5dd9;hb=233826389b4c0c4192c1eb1cacc8cfa99b2750f4;hp=8a7e5bea5047cd0e3bcdddc9b9d50e130834751d;hpb=fcf9d69625a32a27c2a37e93ecd8de5bb9494c51;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index 8a7e5bea5..2faade402 100644
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -42,7 +42,7 @@ module Cl   = ProceduralClassify
 
 (* debugging ****************************************************************)
 
-let debug = ref false
+let debug = ref true
 
 (* term optimization ********************************************************)
 
@@ -192,6 +192,10 @@ and opt_mutcase_critical g st es c uri tyno outty arg cases =
       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