diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2015-04-09 18:33:07 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2015-04-09 18:33:07 +0200 |
| commit | 33650e275a4b3f00541ea87ee4b39892be5fdb2f (patch) | |
| tree | c1441dbda76a9678a9bfed2b3dd89ea3e7486b68 /test-suite/bugs/closed/4120.v | |
| parent | 6158ec51adc31814fde0293f54151c19a5f3b1e4 (diff) | |
Better test-suite files, removing reliance on admit.
Diffstat (limited to 'test-suite/bugs/closed/4120.v')
| -rw-r--r-- | test-suite/bugs/closed/4120.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/4120.v b/test-suite/bugs/closed/4120.v index 4164d86dc..00db8f7f3 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 |