diff options
| author | Vincent Laporte | 2018-10-02 13:44:46 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-10-04 08:01:34 +0000 |
| commit | db22ae6140259dd065fdd80af4cb3c3bab41c184 (patch) | |
| tree | e17ad7016014a4e2dd4001d826575342c2812fc3 /test-suite/bugs/closed/3560.v | |
| parent | 53929e9bacf251f60c85d4ff24d46fec2c42ab4b (diff) | |
rename test files (do not start by a digit)
Diffstat (limited to 'test-suite/bugs/closed/3560.v')
| -rw-r--r-- | test-suite/bugs/closed/3560.v | 15 |
1 files changed, 0 insertions, 15 deletions
diff --git a/test-suite/bugs/closed/3560.v b/test-suite/bugs/closed/3560.v deleted file mode 100644 index a740675f30..0000000000 --- a/test-suite/bugs/closed/3560.v +++ /dev/null @@ -1,15 +0,0 @@ - -(* File reduced by coq-bug-finder from original input, then from 6236 lines to 1049 lines, then from 920 lines to 209 lines, then from 179 lines to 30 lines *) -(* coqc version trunk (August 2014) compiled on Aug 31 2014 10:12:32 with OCaml 4.01.0 - coqtop version cagnode17:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (437b91a3ffd7327975a129b95b24d3f66ad7f3e4) *) - -Set Primitive Projections. -Set Implicit Arguments. -Record prod (A B : Type) := pair { fst : A ; snd : B }. -Notation "x * y" := (prod x y) : type_scope. -Record Equiv A B := { equiv_fun :> A -> B ; equiv_isequiv : forall P, P equiv_fun }. -Goal forall (A B : Type) (C : Type), Equiv (A -> B -> C) (A * B -> C). -Proof. - intros. - exists (fun u => fun x => u (fst x) (snd x)). -Abort. |