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/bugs/closed/3662.v | |
| 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/bugs/closed/3662.v')
| -rw-r--r-- | test-suite/bugs/closed/3662.v | 3 |
1 files changed, 2 insertions, 1 deletions
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. + |