Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of tactic unification.

1 files changed, 16 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/7011.v b/test-suite/bugs/closed/7011.v
new file mode 100644
index 0000000000..296e4e11e5
--- /dev/null
+++ b/test-suite/bugs/closed/7011.v
@@ -0,0 +1,16 @@
+(* Fix and Cofix were missing in tactic unification *)
+
+Goal exists e, (fix foo (n : nat) : nat := match n with O => e | S n' => foo n' end)
+               = (fix foo (n : nat) : nat := match n with O => O | S n' => foo n' end).
+Proof.
+  eexists.
+  reflexivity.
+Qed.
+
+CoInductive stream := cons : nat -> stream -> stream.
+
+Goal exists e, (cofix foo := cons e foo) = (cofix foo := cons 0 foo).
+Proof.
+  eexists.
+  reflexivity.
+Qed.