diff options
| -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 |