diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/3593.v (renamed from test-suite/bugs/opened/3593.v) | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/opened/3593.v b/test-suite/bugs/closed/3593.v index d83b900607..378db68570 100644 --- a/test-suite/bugs/opened/3593.v +++ b/test-suite/bugs/closed/3593.v @@ -5,6 +5,6 @@ Record prod A B := pair { fst : A ; snd : B }. Goal forall x : prod Set Set, let f := @fst _ in f _ x = @fst _ _ x. simpl; intros. constr_eq (@fst Set Set x) (fst (A := Set) (B := Set) x). - Fail Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x). + Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x). reflexivity. Qed. |