From b6e39ade125862ba41ca17b06b8e35726b9b0d7d Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 27 Sep 2014 19:22:24 +0200
Subject: Fix semantics of matching with folded/unfolded projections to
 definitely avoid looping and be compatible with unfold.

---
 test-suite/bugs/closed/3656.v | 10 +++++++---
 test-suite/bugs/closed/3662.v |  3 ++-
 2 files changed, 9 insertions(+), 4 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3656.v b/test-suite/bugs/closed/3656.v
index 218cb755b2..cbd773d079 100644
--- a/test-suite/bugs/closed/3656.v
+++ b/test-suite/bugs/closed/3656.v
@@ -26,7 +26,7 @@ Ltac head_hnf_under_binders x :=
     | ?y => y
   end.
 Goal forall s : @hSet nat, True.
-intros. 
+intros.
 let x := head_hnf_under_binders setT in pose x.
 
 set (foo := eq_refl (@setT nat)). generalize foo. simpl. cbn. 
@@ -42,8 +42,12 @@ Ltac head_hnf_under_binders x :=
     | ?y => y
   end.
 Goal setT = setT.
- Fail progress unfold setT. (* should not succeed *)
+ progress unfold setT. (* should not succeed *)
  match goal with
     | |- (fun h => setT h) = (fun h => setT h) => fail 1 "should not eta-expand"
     | _ => idtac
-  end. (* should not fail *)
\ No newline at end of file
+  end. (* should not fail *)
+Abort.
+
+Goal forall h, setT h = setT h.
+Proof. intro. progress unfold setT. 
diff --git a/test-suite/bugs/closed/3662.v b/test-suite/bugs/closed/3662.v
index 0de92b131e..753fb33ca2 100644
--- a/test-suite/bugs/closed/3662.v
+++ b/test-suite/bugs/closed/3662.v
@@ -44,4 +44,5 @@ Goal forall x : prod nat nat, fst x = 0.
   match goal with
     | [ |- fst ?x = 0 ] => idtac
   end.
-Abort.
\ No newline at end of file
+Abort.
+
-- 
cgit v1.2.3