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=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..c5a27efc4 100644
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -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