diff options
| author | Matthieu Sozeau | 2015-04-09 18:33:07 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-04-09 18:33:07 +0200 |
| commit | 33650e275a4b3f00541ea87ee4b39892be5fdb2f (patch) | |
| tree | c1441dbda76a9678a9bfed2b3dd89ea3e7486b68 | |
| parent | 6158ec51adc31814fde0293f54151c19a5f3b1e4 (diff) | |
Better test-suite files, removing reliance on admit.
| -rw-r--r-- | test-suite/bugs/closed/3590.v | 7 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4120.v | 1 |
2 files changed, 2 insertions, 6 deletions
diff --git a/test-suite/bugs/closed/3590.v b/test-suite/bugs/closed/3590.v index 3440f0e806..3ef9270d40 100644 --- a/test-suite/bugs/closed/3590.v +++ b/test-suite/bugs/closed/3590.v @@ -1,13 +1,10 @@ -Require Import TestSuite.admit. -(* Set Primitive Projections. *) Set Implicit Arguments. Record prod A B := pair { fst : A ; snd : B }. Definition idS := Set. -Goal forall x y : prod Set Set, fst x = fst y. +Goal forall x y : prod Set Set, forall H : fst x = fst y, fst x = fst y. intros. change (@fst _ _ ?z) with (@fst Set idS z) at 2. - Unshelve. - admit. + apply H. Qed. (* Toplevel input, characters 20-58: diff --git a/test-suite/bugs/closed/4120.v b/test-suite/bugs/closed/4120.v index 4164d86dc1..00db8f7f3c 100644 --- a/test-suite/bugs/closed/4120.v +++ b/test-suite/bugs/closed/4120.v @@ -1,6 +1,5 @@ Definition id {T} (x : T) := x. Goal sigT (fun x => id x)%type. change (fun x => ?f x) with f. - Unshelve. exists Type. exact Set. Defined. (* Error: Attempt to save a proof with shelved goals (in proof Unnamed_thm) *)
\ No newline at end of file |