From c6985ba89f59d7e510319d932a991ee832011181 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 3 Jul 2020 14:38:36 +0200
Subject: Remove the last use of the Stack module in Tacred.

---
 pretyping/tacred.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index f31e5ccd95..e4b5dc1edf 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -867,10 +867,10 @@ let try_red_product env sigma c =
                  (match fix_recarg fix (Array.to_list l) with
                     | None -> raise Redelimination
                     | Some (recargnum,recarg) ->
-                        let stack = Stack.append_app l Stack.empty in
                         let recarg' = redrec env recarg in
-                        let stack' = Stack.assign stack recargnum recarg' in
-                        simpfun (Stack.zip sigma (f,stack')))
+                        let l = Array.copy l in
+                        let () = Array.set l recargnum recarg' in
+                        simpfun (mkApp (f, l)))
              | _ -> simpfun (mkApp (redrec env f, l)))
       | Cast (c,_,_) -> redrec env c
       | Prod (x,a,b) ->
-- 
cgit v1.2.3