From 3248466ca57b5121e5a29bf6fd6619c512a52349 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 27 Feb 2015 16:23:36 +0100 Subject: Fix test-suite files for bugs #2456 and #3593, still open. --- test-suite/bugs/opened/2456.v | 4 ++-- 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. -- cgit v1.2.3