From 875f235dd0413faa34f7d46afc25d2eb90e386e5 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 28 Sep 2016 17:01:26 +0200
Subject: Fix bug #4723 and FIXME in API for solve_by_tac

This avoids leakage of universes. Also makes
Program Lemma/Fact work again, it tries to solve the
remaining evars using the obligation tactic.
---
 test-suite/bugs/closed/4723.v | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)
 create mode 100644 test-suite/bugs/closed/4723.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4723.v b/test-suite/bugs/closed/4723.v
new file mode 100644
index 0000000000..8884812102
--- /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
-- 
cgit v1.2.3