From bd3a48926a075296486c552ccef6b87e3fddd5e4 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Aug 2017 10:38:21 +0200 Subject: Prevent overallocation in Array.map_to_list and remove custom implementation from Detyping. --- pretyping/detyping.ml | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) (limited to 'pretyping/detyping.ml') diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index a27debe73..b9cb7ba1b 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -476,7 +476,7 @@ let rec detype flags avoid env sigma t = CAst.make @@ | _ -> GApp (f',args') in mkapp (detype flags avoid env sigma f) - (detype_array flags avoid env sigma args) + (Array.map_to_list (detype flags avoid env sigma) args) | Const (sp,u) -> GRef (ConstRef sp, detype_instance sigma u) | Proj (p,c) -> let noparams () = @@ -694,15 +694,6 @@ 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 - ans := detype flags avoid env sigma args.(i) :: !ans; - done; - !ans - let detype_rel_context ?(lax=false) where avoid env sigma sign = let where = Option.map (fun c -> EConstr.it_mkLambda_or_LetIn c sign) where in let rec aux avoid env = function -- cgit v1.2.3