diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-08-01 13:01:53 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-08-01 13:01:53 +0200 |
commit | 89fa6804337ca0ca091b32261d0b4684ba30432d (patch) | |
tree | d3171707fc94d4851e0498ea58a051528e294d57 /engine/termops.ml | |
parent | 72c69399c0d4b37174f9d91ac79fc359619eb63c (diff) | |
parent | d5ee6e2d24d0f9b42499b507fe9d03555c9ddf45 (diff) |
Merge PR #913: Less allocations in Detyping
Diffstat (limited to 'engine/termops.ml')
-rw-r--r-- | engine/termops.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index cf7c0cc20..2bd0c06d6 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -994,12 +994,14 @@ let rec strip_outer_cast sigma c = match EConstr.kind sigma c with (* flattens application lists throwing casts in-between *) let collapse_appl sigma c = match EConstr.kind sigma c with | App (f,cl) -> + if EConstr.isCast sigma f then let rec collapse_rec f cl2 = match EConstr.kind sigma (strip_outer_cast sigma f) with | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) | _ -> EConstr.mkApp (f,cl2) in collapse_rec f cl + else c | _ -> c (* First utilities for avoiding telescope computation for subst_term *) |