From d5ee6e2d24d0f9b42499b507fe9d03555c9ddf45 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 26 Jul 2017 15:29:16 +0200
Subject: Add a comment regarding the specialization of the combinator in
 Detyping.

---
 pretyping/detyping.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 98f6c24aa4..ebd270e9f9 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -694,6 +694,8 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c =
       let t = if s != InProp  && not !Flags.raw_print then None else Some (detype (lax,false) avoid env sigma ty) in
       GLetIn (na', c, t, r)
 
+(** We use a dedicated function here to prevent overallocation from
+    Array.map_to_list. *)
 and detype_array flags avoid env sigma args =
   let ans = ref [] in
   for i = Array.length args - 1 downto 0 do
-- 
cgit v1.2.3