| 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
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
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 =