diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-21 15:45:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-21 15:45:18 +0200 |
| commit | 380dfe70ad9daf766e6acaf028e2c0cedc3be688 (patch) | |
| tree | 409dffad969dd46d9dff8bfc5ef478c3cacfb647 /engine/termops.ml | |
| parent | 2f1ee61f9700e3d73e637a82f9089807efab186a (diff) | |
No useless reallocation in Termops.collapse_appl.
This function is suspicious, and reallocates a lot when it should be the
identity. This matters for detyping, where it is about the only place where
it is used.
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 1aba2bbdd..4b7d60019 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 *) |