diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-15 13:42:27 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-15 13:42:27 +0200 |
| commit | 0307d06ac50caaa38d980a05f6ac3b0685720411 (patch) | |
| tree | c785b65f17f36aafef13367a4aeae0b84de525d2 /test-suite/bugs/closed/3637.v | |
| parent | 6bca54599ab2b8ab928bfc92b8ddfb0aeba4345f (diff) | |
Fix bug 3637.
Diffstat (limited to 'test-suite/bugs/closed/3637.v')
| -rw-r--r-- | test-suite/bugs/closed/3637.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/3637.v b/test-suite/bugs/closed/3637.v index a451d2997..868f45c89 100644 --- a/test-suite/bugs/closed/3637.v +++ b/test-suite/bugs/closed/3637.v @@ -5,7 +5,7 @@ Record prod A B := pair { fst : A ; snd : B }. Goal forall x y : prod Set Set, fst x = fst y. intros. lazymatch goal with - | [ |- context[@fst ?A ?B] ] => pose (@fst A B) as fst'; + | [ |- context[@fst ?A ?B] ] => pose (@fst A B) as fst'; progress change (@fst Set Set) with fst' end. Abort. |