From ee9d9415c518e703a10a53acfdea8627547565fe Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 6 Apr 2015 09:04:40 +0200
Subject: Test for bug #3815.

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

diff --git a/test-suite/bugs/closed/3815.v b/test-suite/bugs/closed/3815.v
new file mode 100644
index 0000000000..5fb4839847
--- /dev/null
+++ b/test-suite/bugs/closed/3815.v
@@ -0,0 +1,9 @@
+Require Import Setoid Coq.Program.Basics.
+Global Open Scope program_scope.
+Axiom foo : forall A (f : A -> A), f ∘ f = f.
+Require Import Coq.Program.Combinators.
+Hint Rewrite foo.
+Theorem t {A B C D} (f : A -> A) (g : B -> C) (h : C -> D)
+: f ∘ f = f.
+Proof.
+  rewrite_strat topdown (hints core).
-- 
cgit v1.2.3