From 04ee4f9160dec2d854bd45fcff4dac08ada39b61 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 15 Oct 2014 10:43:03 +0200
Subject: Implement a different strategy to expand primitive projections only
 when required, i.e. in first-order unification cases where the head of the
 other side is a hole or the eta-expanded constant.

---
 test-suite/bugs/closed/3625.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/3625.v b/test-suite/bugs/closed/3625.v
index a0f977eeae..3d30b62f80 100644
--- a/test-suite/bugs/closed/3625.v
+++ b/test-suite/bugs/closed/3625.v
@@ -4,6 +4,8 @@ Record prod A B := pair { fst : A ; snd : B }.
 
 Goal forall x y : prod Set Set, x.(@fst _ _) = y.(@fst _ _).
  intros.
+ refine (f_equal _ _).
+ Undo.
  apply f_equal.
  admit.
 Qed.
-- 
cgit v1.2.3