From 334cfab0007591b4c75a17da178d0d8b0347d7fe Mon Sep 17 00:00:00 2001
From: Andrej Dudenhefner <mrhaandi@gmail.com>
Date: Wed, 26 Oct 2022 13:49:50 +0200
Subject: [PATCH] made Vector.nth substructural added test-case

---
 .../11-standard-library/16731-stdlib-vector.rst   |  5 +++++
 test-suite/bugs/bug_16738.v                       | 11 +++++++++++
 theories/Vectors/VectorDef.v                      | 15 +++++++++------
 3 files changed, 25 insertions(+), 6 deletions(-)
 create mode 100644 doc/changelog/11-standard-library/16731-stdlib-vector.rst
 create mode 100644 test-suite/bugs/bug_16738.v

diff --git a/doc/changelog/11-standard-library/16731-stdlib-vector.rst b/doc/changelog/11-standard-library/16731-stdlib-vector.rst
new file mode 100644
index 000000000000..5db568e34cd6
--- /dev/null
+++ b/doc/changelog/11-standard-library/16731-stdlib-vector.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+  implementation of :g:`Vector.nth` to follow OCaml and compute strict subterms
+  (`#16731 <https://github.com/coq/coq/pull/16731>`_,
+  fixes `#16738 <https://github.com/coq/coq/issues/16738>`_,
+  by Andrej Dudenhefner).
diff --git a/test-suite/bugs/bug_16738.v b/test-suite/bugs/bug_16738.v
new file mode 100644
index 000000000000..5d86c1c1f0fe
--- /dev/null
+++ b/test-suite/bugs/bug_16738.v
@@ -0,0 +1,11 @@
+Require Vector.
+
+Inductive container : Type :=
+  | container_v : Vector.t container 2 -> container
+  | container_0 : container.
+
+Fixpoint test (c : container) : unit :=
+  match c with
+  | container_0 => tt
+  | container_v v => test (Vector.nth v (Fin.FS Fin.F1))
+  end.
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 3693169d2ed0..db13da5ffced 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -106,12 +106,15 @@ Definition const {A} (a:A) := nat_rect _ [] (fun n x => cons _ a n x).
 Computational behavior of this function should be the same as
 ocaml function. *)
 Definition nth {A} :=
-fix nth_fix {m} (v' : t A m) (p : Fin.t m) {struct v'} : A :=
-match p in Fin.t m' return t A m' -> A with
- |Fin.F1 => caseS (fun n v' => A) (fun h n t => h)
- |Fin.FS p' => fun v => (caseS (fun n v' => Fin.t n -> A)
-   (fun h n t p0 => nth_fix t p0) v) p'
-end v'.
+  fix nth_fix {n : nat} (v : t A n) {struct v} : Fin.t n -> A :=
+    match v with
+    | nil _ => fun p => False_rect A (Fin.case0 _ p)
+    | cons _ x m v' => fun p =>
+      match p in (Fin.t m') return t A (pred m') -> A with
+      | Fin.F1 => fun _ => x
+      | Fin.FS p' => fun v' => nth_fix v' p'
+      end v'
+    end.
 
 (** An equivalent definition of [nth]. *)
 Definition nth_order {A} {n} (v: t A n) {p} (H: p < n) :=