Merge branch 'bug4723' into v8.6

1 files changed, 28 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4723.v b/test-suite/bugs/closed/4723.v
new file mode 100644
index 000000000..888481210
--- /dev/null
+++ b/test-suite/bugs/closed/4723.v
@@ -0,0 +1,28 @@
+
+Require Coq.Program.Tactics.
+
+Record Matrix (m n : nat).
+
+Definition kp {m n p q: nat} (A: Matrix m n) (B: Matrix p q):
+  Matrix (m*p) (n*q). Admitted.
+
+Fail Program Fact kp_assoc
+        (xr xc yr yc zr zc: nat)
+        (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc):
+  kp x (kp y z) = kp (kp x y) z.
+
+Ltac Obligation Tactic := admit.
+Fail Program Fact kp_assoc
+        (xr xc yr yc zr zc: nat)
+        (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc):
+  kp x (kp y z) = kp (kp x y) z.
+
+Axiom cheat : forall {A}, A.
+Obligation Tactic := apply cheat.
+
+Program Fact kp_assoc
+        (xr xc yr yc zr zc: nat)
+        (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc):
+  kp x (kp y z) = kp (kp x y) z.
+admit.
+Admitted.
\ No newline at end of file