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

1 files changed, 1 insertions, 1 deletions

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.