- 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