diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-27 19:22:24 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-27 20:41:05 +0200 |
| commit | b6e39ade125862ba41ca17b06b8e35726b9b0d7d (patch) | |
| tree | 4faa9cbbc56f3b63f5ef89f98452ab69b31af887 /test-suite | |
| parent | 02b66da78e766a0eb8a1ec82a03ec9ce5418a0f0 (diff) | |
Fix semantics of matching with folded/unfolded projections to definitely
avoid looping and be compatible with unfold.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/3656.v | 10 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3662.v | 3 |
2 files changed, 9 insertions, 4 deletions
diff --git a/test-suite/bugs/closed/3656.v b/test-suite/bugs/closed/3656.v index 218cb755b..cbd773d07 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 0de92b131..753fb33ca 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. + |