aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/opened
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/opened')
-rw-r--r--test-suite/bugs/opened/3263.v1
-rw-r--r--test-suite/bugs/opened/3345.v1
-rw-r--r--test-suite/bugs/opened/3395.v1
-rw-r--r--test-suite/bugs/opened/3509.v1
-rw-r--r--test-suite/bugs/opened/3510.v1
-rw-r--r--test-suite/bugs/opened/3685.v1
-rw-r--r--test-suite/bugs/opened/3754.v1
-rw-r--r--test-suite/bugs/opened/3848.v1
-rw-r--r--test-suite/bugs/opened/HoTT_coq_120.v1
9 files changed, 9 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/3263.v b/test-suite/bugs/opened/3263.v
index 6de13f74e..f0c707bd1 100644
--- a/test-suite/bugs/opened/3263.v
+++ b/test-suite/bugs/opened/3263.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
(* File reduced by coq-bug-finder from originally 10918 lines, then 3649 lines to 3177 lines, then from 3189 lines to 3164 lines, then from 2653 lines to 2496 lines, 2653 lines, then from 1642 lines to 651 lines, then from 736 lines to 473 lines, then from 433 lines to 275 lines, then from 258 lines to 235 lines. *)
Generalizable All Variables.
Set Implicit Arguments.
diff --git a/test-suite/bugs/opened/3345.v b/test-suite/bugs/opened/3345.v
index b61174a86..3e3da6df7 100644
--- a/test-suite/bugs/opened/3345.v
+++ b/test-suite/bugs/opened/3345.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
(* File reduced by coq-bug-finder from original input, then from 1972 lines to 136 lines, then from 119 lines to 105 lines *)
Global Set Implicit Arguments.
Require Import Coq.Lists.List Program.
diff --git a/test-suite/bugs/opened/3395.v b/test-suite/bugs/opened/3395.v
index ff0dbf974..5ca48fc9d 100644
--- a/test-suite/bugs/opened/3395.v
+++ b/test-suite/bugs/opened/3395.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
(* File reduced by coq-bug-finder from originally 10918 lines, then 3649 lines to 3177 lines, then from 3189 lines to 3164 lines, then from 2653 lines to 2496 lines, 2653 lines, then from 1642 lines to 651 lines, then from 736 lines to 473 lines, then from 433 lines to 275 lines, then from 258 lines to 235 lines. *)
Generalizable All Variables.
Set Implicit Arguments.
diff --git a/test-suite/bugs/opened/3509.v b/test-suite/bugs/opened/3509.v
index 02e47a8b4..3913bbb43 100644
--- a/test-suite/bugs/opened/3509.v
+++ b/test-suite/bugs/opened/3509.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
Lemma match_bool_fn b A B xT xF
: match b as b return forall x : A, B b x with
| true => xT
diff --git a/test-suite/bugs/opened/3510.v b/test-suite/bugs/opened/3510.v
index 25285636b..daf265071 100644
--- a/test-suite/bugs/opened/3510.v
+++ b/test-suite/bugs/opened/3510.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
Lemma match_option_fn T (b : option T) A B s n
: match b as b return forall x : A, B b x with
| Some k => s k
diff --git a/test-suite/bugs/opened/3685.v b/test-suite/bugs/opened/3685.v
index d647b5a83..b2b5db6be 100644
--- a/test-suite/bugs/opened/3685.v
+++ b/test-suite/bugs/opened/3685.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
Set Universe Polymorphism.
Class Funext := { }.
Delimit Scope category_scope with category.
diff --git a/test-suite/bugs/opened/3754.v b/test-suite/bugs/opened/3754.v
index c74418820..9b3f94d91 100644
--- a/test-suite/bugs/opened/3754.v
+++ b/test-suite/bugs/opened/3754.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
(* File reduced by coq-bug-finder from original input, then from 9113 lines to 279 lines *)
(* coqc version trunk (October 2014) compiled on Oct 19 2014 18:56:9 with OCaml 3.12.1
coqtop version trunk (October 2014) *)
diff --git a/test-suite/bugs/opened/3848.v b/test-suite/bugs/opened/3848.v
index 9413daa04..a03e8ffda 100644
--- a/test-suite/bugs/opened/3848.v
+++ b/test-suite/bugs/opened/3848.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y.
Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing).
Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := forall x : A, r (s x) = x.
diff --git a/test-suite/bugs/opened/HoTT_coq_120.v b/test-suite/bugs/opened/HoTT_coq_120.v
index 7847c5e44..05ee6c7b6 100644
--- a/test-suite/bugs/opened/HoTT_coq_120.v
+++ b/test-suite/bugs/opened/HoTT_coq_120.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
(* File reduced by coq-bug-finder from original input, then from 8249 lines to 907 lines, then from 843 lines to 357 lines, then from 351 lines to 260 lines, then from 208 lines to 162 lines, then from 167 lines to 154 lines *)
Set Universe Polymorphism.
Generalizable All Variables.