diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-02-27 16:23:36 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-02-27 16:23:55 +0100 |
| commit | 3248466ca57b5121e5a29bf6fd6619c512a52349 (patch) | |
| tree | 571ccd7024c5fb3b413f1aa6f66a32e9faa70415 | |
| parent | f4d7d60b90ee03179479f8e3427bd1a5729135f2 (diff) | |
Fix test-suite files for bugs #2456 and #3593, still open.
| -rw-r--r-- | test-suite/bugs/opened/2456.v | 4 | ||||
| -rw-r--r-- | test-suite/bugs/opened/3593.v | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/bugs/opened/2456.v b/test-suite/bugs/opened/2456.v index 56f046c4d..6cca5c9fb 100644 --- a/test-suite/bugs/opened/2456.v +++ b/test-suite/bugs/opened/2456.v @@ -46,8 +46,8 @@ Lemma CatchCommuteUnique2 : Proof with auto. intros. set (X := commute2). -dependent destruction commute1; +Fail dependent destruction commute1; dependent destruction catchCommuteDetails; dependent destruction commute2; dependent destruction catchCommuteDetails generalizing X. -Admitted.
\ No newline at end of file +Admitted. diff --git a/test-suite/bugs/opened/3593.v b/test-suite/bugs/opened/3593.v index 25f9db6b2..d83b90060 100644 --- a/test-suite/bugs/opened/3593.v +++ b/test-suite/bugs/opened/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 progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x). + Fail Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x). reflexivity. Qed. |