From 7e5dc9f830bc2cdbc3b8cc8b830adafc61660055 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 26 Mar 2021 09:28:34 -0400
Subject: Fix Ltac2 `Array.init` exponential overhead

Previously, `Array.init` was computing the first element of the array
twice, resulting in exponential overhead in the number of recursive
nestings of `Array.init`.  Notably, since `Array.map` is implemented in
terms of `Array.init`, this exponential blowup shows up in any term
traversal based on `Array.map` over the arguments of application nodes.

Fixes #14011
---
 user-contrib/Ltac2/Array.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'user-contrib')

diff --git a/user-contrib/Ltac2/Array.v b/user-contrib/Ltac2/Array.v
index 5adba829c5..b5e7f37c9f 100644
--- a/user-contrib/Ltac2/Array.v
+++ b/user-contrib/Ltac2/Array.v
@@ -70,7 +70,7 @@ Ltac2 init (l : int) (f : int->'a) :=
   | true => empty ()
   | false =>
       let arr:=make l (f 0) in
-      init_aux arr 0 (length arr) f;
+      init_aux arr 1 (Int.sub l 1) f;
       arr
   end.
 
-- 
cgit v1.2.3