From f66b8f45d4cf397602c565f9d83f8a3daed2239d Mon Sep 17 00:00:00 2001
From: 4ever2 <3417013+4ever2@users.noreply.github.com>
Date: Fri, 8 Nov 2024 12:58:05 +0100
Subject: [PATCH] Fix substitution during eta expansion of partial application

---
 template-coq/theories/EtaExpand.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/template-coq/theories/EtaExpand.v b/template-coq/theories/EtaExpand.v
index 3b9614f36..507cd7dac 100644
--- a/template-coq/theories/EtaExpand.v
+++ b/template-coq/theories/EtaExpand.v
@@ -57,7 +57,7 @@ Section Eta.
     let prev_args := map (lift0 needed) args in
     let eta_args := rev_map tRel (seq 0 needed) in
     let remaining := firstn needed (skipn #|args| (rev (smash_context [] (decompose_prod_assum [] ty).1))) in
-    let remaining_subst := subst_context (rev args) 0 remaining in
+    let remaining_subst := rev (subst_context (rev args) 0 (rev remaining)) in
     fold_right (fun d b => Ast.tLambda d.(decl_name) d.(decl_type) b) (mkApps (lift0 needed t) (prev_args ++ eta_args)) remaining_subst.
 
   Definition eta_constructor (ind : inductive) c u args :=