From d3934986fb2ff0d563a1a2a89ba5fbbefb53f0fd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 24 Jan 2015 10:34:26 +0100
Subject: Test for bug #3798.

---
 test-suite/bugs/closed/3798.v | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 test-suite/bugs/closed/3798.v

diff --git a/test-suite/bugs/closed/3798.v b/test-suite/bugs/closed/3798.v
new file mode 100644
index 0000000000..623822e990
--- /dev/null
+++ b/test-suite/bugs/closed/3798.v
@@ -0,0 +1,11 @@
+Require Setoid.
+
+Parameter f : nat -> nat.
+Axiom a : forall n, 0 < n -> f n = 0.
+Hint Rewrite a using ( simpl; admit ).
+
+Goal f 1 = 0.
+Proof.
+  rewrite_strat (topdown (hints core)).
+  reflexivity.
+Qed.
-- 
cgit v1.2.3