From c1f70486cd62cbd65176c8799077b48dd2c93797 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 23 Jun 2020 09:32:22 +0200
Subject: Add a test for the strange behaviour encountered with this change.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_12532.v b/test-suite/bugs/closed/bug_12532.v
new file mode 100644
index 0000000000..665f6643e6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12532.v
@@ -0,0 +1,56 @@
+(** This is a change of behaviour introduced by PR #12532. It is not clear
+    whether it is a legit behaviour but it is worth having it in the test
+    suite. *)
+
+Module Foo.
+
+Axiom whatever : Type.
+Axiom name : Type.
+Axiom nw : forall (P : Type), name -> P.
+Axiom raft_data : Type.
+Axiom In : raft_data -> Prop.
+
+Axiom foo : forall st st', In st -> In st'.
+
+Definition params := prod whatever raft_data.
+
+Goal forall
+  (d : raft_data),
+  (forall (h : name), In (@snd whatever raft_data (@nw params h))) ->
+  In d.
+Proof.
+intros.
+eapply foo.
+solve [debug eauto].
+Abort.
+
+End Foo.
+
+Module Bar.
+
+Axiom whatever : Type.
+Axiom AppendEntries : whatever -> Prop.
+Axiom name : Type.
+Axiom nw : forall (P : Type), name -> P.
+Axiom raft_data : Type.
+Axiom In : raft_data -> Prop.
+
+Axiom foo :
+  forall st st' lid,
+    (AppendEntries lid -> In st) -> AppendEntries lid -> In st'.
+
+Definition params := prod whatever raft_data.
+
+Goal forall
+  (d : raft_data),
+  (forall (h : name) (w : whatever),
+    AppendEntries w -> In (@snd whatever raft_data (@nw params h))) ->
+  In d.
+Proof.
+intros.
+eapply foo.
+intros.
+solve [debug eauto].
+Abort.
+
+End Bar.
-- 
cgit v1.2.3