- let x = H.refine c (C.Appl args) in
- HLog.warn "Optimizer: remove 3"; opt1_proof g es c x
-
-and opt1_cast g es c t w =
- let g t = HLog.warn "Optimizer: remove 4"; g t in
- if es then opt1_proof g es c t else g t
-
-and opt1_other g es c t = g t
-
-and opt1_proof g es c = function
- | C.LetIn (name, v, ty, t) -> opt1_letin g es c name v ty t
- | C.Lambda (name, w, t) -> opt1_lambda g es c name w t
- | C.Appl (t :: v :: vs) -> opt1_appl g es c t (v :: vs)
- | C.Appl [t] -> opt1_proof g es c t
- | C.MutCase (u, n, t, v, ws) -> opt1_mutcase g es c u n t v ws
- | C.Cast (t, w) -> opt1_cast g es c t w
- | t -> opt1_other g es c t
-
-and opt1_term g es c t =
- if H.is_proof c t then opt1_proof g es c t else g t
+ 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