Merge 8.19 into 8.20

.github/dependabot.yml

@@ -17,6 +17,22 @@ updates:
       interval: "daily"
     labels:
       - "dependencies"
+  - package-ecosystem: "github-actions"
+    directory: "/"
+    target-branch: "coq-8.20"
+    schedule:
+      # Check for updates to GitHub Actions every weekday
+      interval: "daily"
+    labels:
+      - "dependencies"
+  - package-ecosystem: "github-actions"
+    directory: "/"
+    target-branch: "coq-8.19"
+    schedule:
+      # Check for updates to GitHub Actions every weekday
+      interval: "daily"
+    labels:
+      - "dependencies"
   - package-ecosystem: "github-actions"
     directory: "/"
     target-branch: "coq-8.18"

html/resources/header.html

@@ -19,7 +19,7 @@
 
     <span class="right">
       <a href="../">Project Page</a>
-      <a href="./indexpage.html"> Index </a>
+      <a href="./index.html"> Index </a>
       <a href="./toc.html"> Table of Contents </a>
     </span>
 </div>

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 :=