-and opt1_proof g es c = function
- | C.LetIn (name, v, t) -> opt1_letin g es c name v 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
-
-(* term preprocessing: optomization 2 ***************************************)
-
-let expanded_premise = "EXPANDED"
-
-let eta_expand g tys t =
- assert (tys <> []);
- let name i = Printf.sprintf "%s%u" expanded_premise i in
- let lambda i ty t = C.Lambda (C.Name (name i), ty, t) in
- let arg i = C.Rel (succ i) in
- let rec aux i f a = function
- | [] -> f, a
- | (_, ty) :: tl -> aux (succ i) (H.compose f (lambda i ty)) (arg i :: a) tl
- in
- let n = List.length tys in
- let absts, args = aux 0 H.identity [] tys in
- let t = match S.lift n t with
- | C.Appl ts -> C.Appl (ts @ args)
- | t -> C.Appl (t :: args)
+and opt_mutcase_plain g st es c uri tyno outty arg cases =
+ let g st v =
+ let g (st, ts) = g st (C.MutCase (uri, tyno, outty, v, ts)) in
+ let map h v (st, vs) =
+ let h st vv = h (st, vv :: vs) in opt_proof h st es c v
+ in
+ if es then H.list_fold_right_cps g map cases (st, []) else g (st, cases)