From 380dfe70ad9daf766e6acaf028e2c0cedc3be688 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 21 Jul 2017 15:45:18 +0200
Subject: 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.
---
 engine/termops.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'engine')

diff --git a/engine/termops.ml b/engine/termops.ml
index 1aba2bbdd1..4b7d600196 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 *)
-- 
cgit v1.2.3