diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-11 20:47:06 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-11 20:47:06 +0200 |
| commit | 580b25e05c7cc9e7a31430b3d9edb14ae12b7598 (patch) | |
| tree | 0d2a0d9590d2e5af4b8a06611c26c6da19e8e30d /test-suite/bugs/closed/3559.v | |
| parent | 2378b5ccee0e62d0b93935aa69c0bfedd2ac720e (diff) | |
Fix test-suite files, and move some opened to closed.
Diffstat (limited to 'test-suite/bugs/closed/3559.v')
| -rw-r--r-- | test-suite/bugs/closed/3559.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/3559.v b/test-suite/bugs/closed/3559.v index a193f3888..66d653c52 100644 --- a/test-suite/bugs/closed/3559.v +++ b/test-suite/bugs/closed/3559.v @@ -1,4 +1,3 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter" "-nois") -*- *) (* File reduced by coq-bug-finder from original input, then from 8657 lines to 4731 lines, then from 4174 lines to 192 lines, then from 161 lines to 55 lines, then from 51 lines to 37 lines, then from 43 lines to 30 lines *) @@ -19,7 +18,7 @@ Open Scope type_scope. Definition iff A B := prod (A -> B) (B -> A). Infix "<->" := iff : type_scope. -Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = +Inductive paths {A : Type@{i}} (a : A) : A -> Type@{i} := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. Class Contr_internal (A : Type) := { center : A ; contr : (forall y : A, center = y) }. |