admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)

- no more inconsistent Axiom in the Prelude
- STM can now process Admitted proofs asynchronously
  - the quick chain can stock "Admitted" jobs in .vio files
  - the vio2vo step checks the jobs but does not stock the result
    in the opaque tables (they have no slot)
- Admitted emits a warning if the proof is complete
- Admitted uses the (partial) proof term to infer section variables
  used (if not given with Proof using), like for Qed
- test-suite: extra line Require TestSuite.admit to each file making
  use of admit
- test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to
  find TestSuite.admit

111 files changed, 114 insertions, 4 deletions

diff --git a/test-suite/_CoqProject b/test-suite/_CoqProject
new file mode 100644
index 000000000..dc121311d
--- /dev/null
+++ b/test-suite/_CoqProject
@@ -0,0 +1 @@
+-Q prerequisite TestSuite
diff --git a/test-suite/bugs/closed/1704.v b/test-suite/bugs/closed/1704.v
index 4b02d5f93..7d8ba5b8d 100644
--- a/test-suite/bugs/closed/1704.v
+++ b/test-suite/bugs/closed/1704.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 
 Require Import Setoid.
 Parameter E : nat -> nat -> Prop.
diff --git a/test-suite/bugs/closed/2378.v b/test-suite/bugs/closed/2378.v
index 35c69db2f..85ad41d1c 100644
--- a/test-suite/bugs/closed/2378.v
+++ b/test-suite/bugs/closed/2378.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* test with Coq 8.3rc1 *)
 
 Require Import Program.
diff --git a/test-suite/bugs/closed/2473.v b/test-suite/bugs/closed/2473.v
index 4c3025128..fb676c7e4 100644
--- a/test-suite/bugs/closed/2473.v
+++ b/test-suite/bugs/closed/2473.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 
 Require Import Relations Program Setoid Morphisms.
 
diff --git a/test-suite/bugs/closed/2590.v b/test-suite/bugs/closed/2590.v
index e594e9693..4300de16e 100644
--- a/test-suite/bugs/closed/2590.v
+++ b/test-suite/bugs/closed/2590.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Require Import Relation_Definitions RelationClasses Setoid SetoidClass.
 
 Section Bug.
diff --git a/test-suite/bugs/closed/2613.v b/test-suite/bugs/closed/2613.v
index 4f0470b1d..15f3bf52c 100644
--- a/test-suite/bugs/closed/2613.v
+++ b/test-suite/bugs/closed/2613.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* Check that eq_sym is still pointing to Logic.eq_sym after use of Function *)
 
 Require Import ZArith.
diff --git a/test-suite/bugs/closed/2615.v b/test-suite/bugs/closed/2615.v
index dde6a6a5e..38c1cfc84 100644
--- a/test-suite/bugs/closed/2615.v
+++ b/test-suite/bugs/closed/2615.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* This failed with an anomaly in pre-8.4 because of let-in not
    properly taken into account in the test for unification pattern *)
 
diff --git a/test-suite/bugs/closed/2883.v b/test-suite/bugs/closed/2883.v
index 5a5d90a40..f027b5eb2 100644
--- a/test-suite/bugs/closed/2883.v
+++ b/test-suite/bugs/closed/2883.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Require Import List.
 Require Import Coq.Program.Equality.
 
diff --git a/test-suite/bugs/closed/2969.v b/test-suite/bugs/closed/2969.v
index ff75a1f32..a03adbd73 100644
--- a/test-suite/bugs/closed/2969.v
+++ b/test-suite/bugs/closed/2969.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* Check that Goal.V82.byps and Goal.V82.env are consistent *)
 
 (* This is a shorten variant of the initial bug which raised anomaly *)
diff --git a/test-suite/bugs/closed/2996.v b/test-suite/bugs/closed/2996.v
index 440cda617..d5409289c 100644
--- a/test-suite/bugs/closed/2996.v
+++ b/test-suite/bugs/closed/2996.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* Test on definitions referring to section variables that are not any
    longer in the current context *)
 
diff --git a/test-suite/bugs/closed/3068.v b/test-suite/bugs/closed/3068.v
index 03e5af61b..ced6d9594 100644
--- a/test-suite/bugs/closed/3068.v
+++ b/test-suite/bugs/closed/3068.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Section Counted_list.
 
   Variable A : Type.
diff --git a/test-suite/bugs/closed/3258.v b/test-suite/bugs/closed/3258.v
index a1390e302..b263c6baf 100644
--- a/test-suite/bugs/closed/3258.v
+++ b/test-suite/bugs/closed/3258.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Require Import Coq.Classes.Morphisms Coq.Classes.RelationClasses Coq.Program.Program Coq.Setoids.Setoid.
 
 Global Set Implicit Arguments.
diff --git a/test-suite/bugs/closed/3259.v b/test-suite/bugs/closed/3259.v
index 0306c6866..aa91fc3de 100644
--- a/test-suite/bugs/closed/3259.v
+++ b/test-suite/bugs/closed/3259.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Goal forall m n, n+n = m+m -> m+m = m+m.
 Proof.
 intros.
diff --git a/test-suite/bugs/closed/3298.v b/test-suite/bugs/closed/3298.v
index 3a7de4567..f07ee1e6c 100644
--- a/test-suite/bugs/closed/3298.v
+++ b/test-suite/bugs/closed/3298.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Module JGross.
   Hint Extern 1 => match goal with |- match ?E with end => case E end.
 
diff --git a/test-suite/bugs/closed/3309.v b/test-suite/bugs/closed/3309.v
index 049589325..980431576 100644
--- a/test-suite/bugs/closed/3309.v
+++ b/test-suite/bugs/closed/3309.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* -*- coq-prog-args: ("-emacs" "-impredicative-set") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348 lines to 320 lines, then from 328 lines to 302 lines *)
 Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/3314.v b/test-suite/bugs/closed/3314.v
index 647862637..e63c46da0 100644
--- a/test-suite/bugs/closed/3314.v
+++ b/test-suite/bugs/closed/3314.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Set Universe Polymorphism.
 Definition Lift
 : $(let U1 := constr:(Type) in
diff --git a/test-suite/bugs/closed/3319.v b/test-suite/bugs/closed/3319.v
index bb5853ddd..3b37e39e5 100644
--- a/test-suite/bugs/closed/3319.v
+++ b/test-suite/bugs/closed/3319.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 5353 lines to 4545 lines, then from 4513 lines to 4504 lines, then from 4515 lines to 4508 lines, then from 4519 lines to 132 lines, then from 111 lines to 66 lines, then from 68 lines to 35 lines *)
 Set Implicit Arguments.
 Inductive paths {A : Type} (a : A) : A -> Type :=
diff --git a/test-suite/bugs/closed/3321.v b/test-suite/bugs/closed/3321.v
index 07e3b3cb5..b6f10e533 100644
--- a/test-suite/bugs/closed/3321.v
+++ b/test-suite/bugs/closed/3321.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 5302 lines to 4649 lines, then from 4660 lines to 355 lines, then from 360 lines to 269 lines, then from 269 lines to 175 lines, then from 144 lines to 119 lines, then from 103 lines to 83 lines, then from 86 lines to 36 lines, then from 37 lines to 17 lines *)
 
 Axiom admit : forall {T}, T.
diff --git a/test-suite/bugs/closed/3322.v b/test-suite/bugs/closed/3322.v
index 925f22a21..ab3025a6a 100644
--- a/test-suite/bugs/closed/3322.v
+++ b/test-suite/bugs/closed/3322.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 11971 lines to 11753 lines, then from 7702 lines to 564 lines, then from 571 lines to 61 lines *)
 Set Asymmetric Patterns.
 Axiom admit : forall {T}, T.
diff --git a/test-suite/bugs/closed/3323.v b/test-suite/bugs/closed/3323.v
index fb5a8a7eb..22b1603b6 100644
--- a/test-suite/bugs/closed/3323.v
+++ b/test-suite/bugs/closed/3323.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* -*- coq-prog-args: ("-emacs" "-indices-matter") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 5302 lines to 4649 lines, then from 4660 lines to 355 lines, then from 360 lines to 269 lines, then from 269 lines to 175 lines, then from 144 lines to 119 lines, then from 297 lines to 117 lines, then from 95 lines to 79 lines, then from 82 lines to 68 lines *)
 
diff --git a/test-suite/bugs/closed/3324.v b/test-suite/bugs/closed/3324.v
index 9cd6e4c2e..45dbb57aa 100644
--- a/test-suite/bugs/closed/3324.v
+++ b/test-suite/bugs/closed/3324.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Module ETassi.
   Axiom admit : forall {T}, T.
   Class IsHProp (A : Type) : Type := {}.
diff --git a/test-suite/bugs/closed/3329.v b/test-suite/bugs/closed/3329.v
index f7e368f8f..ecb09e843 100644
--- a/test-suite/bugs/closed/3329.v
+++ b/test-suite/bugs/closed/3329.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 12095 lines to 869 lines, then from 792 lines to 504 lines, then from 487 lines to 353 lines, then from 258 lines to 174 lines, then from 164 lines to 132 lines, then from 129 lines to 99 lines *)
 Set Universe Polymorphism.
 Generalizable All Variables.
diff --git a/test-suite/bugs/closed/3330.v b/test-suite/bugs/closed/3330.v
index 15303cca4..4cd7c39e8 100644
--- a/test-suite/bugs/closed/3330.v
+++ b/test-suite/bugs/closed/3330.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 12106 lines to 1070 lines *)
 Set Universe Polymorphism.
 Definition setleq (A : Type@{i}) (B : Type@{j}) := A : Type@{j}.
diff --git a/test-suite/bugs/closed/3344.v b/test-suite/bugs/closed/3344.v
index 8255fd6cc..880851c56 100644
--- a/test-suite/bugs/closed/3344.v
+++ b/test-suite/bugs/closed/3344.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 716 lines to 197 lines, then from 206 lines to 162 lines, then from 163 lines to 73 lines *)
 Require Import Coq.Sets.Ensembles.
 Require Import Coq.Strings.String.
diff --git a/test-suite/bugs/closed/3347.v b/test-suite/bugs/closed/3347.v
index 37c0d87ee..63d5c7a57 100644
--- a/test-suite/bugs/closed/3347.v
+++ b/test-suite/bugs/closed/3347.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 12653 lines to 12453 lines, then from 11673 lines to 681 lines, then from 693 lines to 469 lines, then from 375 lines to 56 lines *)
 Set Universe Polymorphism.
 Notation Type1 := $(let U := constr:(Type) in let gt := constr:(Set : U) in exact U)$ (only parsing).
diff --git a/test-suite/bugs/closed/3350.v b/test-suite/bugs/closed/3350.v
index 30fdf1694..c041c401f 100644
--- a/test-suite/bugs/closed/3350.v
+++ b/test-suite/bugs/closed/3350.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Require Coq.Vectors.Fin.
 Require Coq.Vectors.Vector.
 
diff --git a/test-suite/bugs/closed/3373.v b/test-suite/bugs/closed/3373.v
index 5ecf28015..051e69520 100644
--- a/test-suite/bugs/closed/3373.v
+++ b/test-suite/bugs/closed/3373.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 5968 lines to
 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446
 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then
diff --git a/test-suite/bugs/closed/3374.v b/test-suite/bugs/closed/3374.v
index 3c67703a2..d8e72f4f2 100644
--- a/test-suite/bugs/closed/3374.v
+++ b/test-suite/bugs/closed/3374.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348 lines to 320 lines, then from 328 lines to 302 lines, then from 331 lines to 59 lines *)
 
 Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/3375.v b/test-suite/bugs/closed/3375.v
index fe323fcb2..d7ce02ea8 100644
--- a/test-suite/bugs/closed/3375.v
+++ b/test-suite/bugs/closed/3375.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* -*- mode: coq; coq-prog-args: ("-emacs" "-impredicative-set") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348 lines to 320 lines, then from 328 lines to 302 lines, then from 330 lines to 45 lines *)
 
diff --git a/test-suite/bugs/closed/3382.v b/test-suite/bugs/closed/3382.v
index 1d8e91674..3e374d907 100644
--- a/test-suite/bugs/closed/3382.v
+++ b/test-suite/bugs/closed/3382.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from 9039 lines to 7786 lines, then from 7245 lines to 476 lines, then from 417 lines to 249 lines, then from 171 lines to 127 lines, then from 139 lines to 114 lines, then from 93 lines to 77 lines *)
 
 Set Implicit Arguments.
diff --git a/test-suite/bugs/closed/3392.v b/test-suite/bugs/closed/3392.v
index 02eca64ee..3a5986954 100644
--- a/test-suite/bugs/closed/3392.v
+++ b/test-suite/bugs/closed/3392.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 12105 lines to 142 lines, then from 83 lines to 57 lines *)
 Generalizable All Variables.
 Axiom admit : forall {T}, T.
diff --git a/test-suite/bugs/closed/3393.v b/test-suite/bugs/closed/3393.v
index ec25e6829..f7ab5f76a 100644
--- a/test-suite/bugs/closed/3393.v
+++ b/test-suite/bugs/closed/3393.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* -*- coq-prog-args: ("-emacs" "-indices-matter") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 8760 lines to 7519 lines, then from 7050 lines to 909 lines, then from 846 lines to 578 lines, then from 497 lines to 392 lines, then from 365 lines to 322 lines, then from 252 lines to 205 lines, then from 215 lines to 204 lines, then from 210 lines to 182 lines, then from 175 lines to 157 lines *)
 Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/3422.v b/test-suite/bugs/closed/3422.v
index d984f6230..460ae8f11 100644
--- a/test-suite/bugs/closed/3422.v
+++ b/test-suite/bugs/closed/3422.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Generalizable All Variables.
 Set Implicit Arguments.
 Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/3427.v b/test-suite/bugs/closed/3427.v
index 8483a4ecf..374a53928 100644
--- a/test-suite/bugs/closed/3427.v
+++ b/test-suite/bugs/closed/3427.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 0 lines to 7171 lines, then from 7184 lines to 558 lines, then from 556 lines to 209 lines *)
 Generalizable All Variables.
diff --git a/test-suite/bugs/closed/3439.v b/test-suite/bugs/closed/3439.v
index bba6140f7..1ea24bf1b 100644
--- a/test-suite/bugs/closed/3439.v
+++ b/test-suite/bugs/closed/3439.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 3154 lines to 149 lines, then from 89 lines to 55 lines, then from 44 lines to 20 lines *)
 Set Primitive Projections.
 Generalizable All Variables.
diff --git a/test-suite/bugs/closed/3480.v b/test-suite/bugs/closed/3480.v
index 99ac2efab..a81837e71 100644
--- a/test-suite/bugs/closed/3480.v
+++ b/test-suite/bugs/closed/3480.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Set Primitive Projections.
 Axiom admit : forall {T}, T.
 Notation "( x ; y )" := (existT _ x y) : fibration_scope.
diff --git a/test-suite/bugs/closed/3484.v b/test-suite/bugs/closed/3484.v
index 6c40a4266..dc88a332b 100644
--- a/test-suite/bugs/closed/3484.v
+++ b/test-suite/bugs/closed/3484.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 14259 lines to 305 lines, then from 237 lines to 120 lines, then from 100 lines to 30 lines *)
 Set Primitive Projections.
 Set Implicit Arguments.
diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v
index 80695f382..fcdfa0057 100644
--- a/test-suite/bugs/closed/3513.v
+++ b/test-suite/bugs/closed/3513.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 5752 lines to 3828 lines, then from 2707 lines to 558 lines, then from 472 lines to 168 lines, then from 110 lines to 101 lines, then from 96 lines to 77 lines, then from 80 lines to 64 lines *)
 Require Coq.Setoids.Setoid.
 Import Coq.Setoids.Setoid.
diff --git a/test-suite/bugs/closed/3531.v b/test-suite/bugs/closed/3531.v
index fd080a6b0..764a7334e 100644
--- a/test-suite/bugs/closed/3531.v
+++ b/test-suite/bugs/closed/3531.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 270 lines to
 198 lines, then from 178 lines to 82 lines, then from 88 lines to 59 lines *)
 (* coqc version trunk (August 2014) compiled on Aug 19 2014 14:40:15 with OCaml
diff --git a/test-suite/bugs/closed/3561.v b/test-suite/bugs/closed/3561.v
index b4dfd17f5..f6cbc9299 100644
--- a/test-suite/bugs/closed/3561.v
+++ b/test-suite/bugs/closed/3561.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 6343 lines to 2362 lines, then from 2115 lines to 303 lines, then from 321 lines to 90 lines, then from 95 lines to 41 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) *)
diff --git a/test-suite/bugs/closed/3590.v b/test-suite/bugs/closed/3590.v
index 51d6744c5..3440f0e80 100644
--- a/test-suite/bugs/closed/3590.v
+++ b/test-suite/bugs/closed/3590.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* Set Primitive Projections. *)
 Set Implicit Arguments.
 Record prod A B := pair { fst : A ; snd : B }.
diff --git a/test-suite/bugs/closed/3596.v b/test-suite/bugs/closed/3596.v
index d6c1c949d..49dd7be5a 100644
--- a/test-suite/bugs/closed/3596.v
+++ b/test-suite/bugs/closed/3596.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Set Implicit Arguments.
 Record foo := { fx : nat }.
 Set Primitive Projections.
diff --git a/test-suite/bugs/closed/3625.v b/test-suite/bugs/closed/3625.v
index 3d30b62f8..d4b2cc5cc 100644
--- a/test-suite/bugs/closed/3625.v
+++ b/test-suite/bugs/closed/3625.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Set Implicit Arguments.
 Set Primitive Projections.
 Record prod A B := pair { fst : A ; snd : B }.
diff --git a/test-suite/bugs/closed/3647.v b/test-suite/bugs/closed/3647.v
index cd542c8a5..495e67e09 100644
--- a/test-suite/bugs/closed/3647.v
+++ b/test-suite/bugs/closed/3647.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Require Coq.Setoids.Setoid.
 
 Axiom BITS : nat -> Set.
diff --git a/test-suite/bugs/closed/3653.v b/test-suite/bugs/closed/3653.v
index 947b36017..b97689676 100644
--- a/test-suite/bugs/closed/3653.v
+++ b/test-suite/bugs/closed/3653.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Require Setoid.
 
 Variables P Q : forall {T : Set}, T -> Prop.
diff --git a/test-suite/bugs/closed/3658.v b/test-suite/bugs/closed/3658.v
index b1158b9a4..622c3c94a 100644
--- a/test-suite/bugs/closed/3658.v
+++ b/test-suite/bugs/closed/3658.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 12178 lines to 457 lines, then from 500 lines to 147 lines, then from 175 lines to 56 lines *)
 (* coqc version trunk (September 2014) compiled on Sep 21 2014 16:34:4 with OCaml 4.01.0
    coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (eaf864354c3fda9ddc1f03f0b1c7807b6fd44322) *)
diff --git a/test-suite/bugs/closed/3660.v b/test-suite/bugs/closed/3660.v
index ed8964ce1..39eb89c40 100644
--- a/test-suite/bugs/closed/3660.v
+++ b/test-suite/bugs/closed/3660.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Generalizable All Variables.
 Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x).
 Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope.
diff --git a/test-suite/bugs/closed/3664.v b/test-suite/bugs/closed/3664.v
index 41de74ff3..63a81b6d0 100644
--- a/test-suite/bugs/closed/3664.v
+++ b/test-suite/bugs/closed/3664.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Module NonPrim.
   Unset Primitive Projections.
   Record c := { d : Set }.
diff --git a/test-suite/bugs/closed/3668.v b/test-suite/bugs/closed/3668.v
index 547159b95..da01ed00e 100644
--- a/test-suite/bugs/closed/3668.v
+++ b/test-suite/bugs/closed/3668.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 6329 lines to 110 lines, then from 115 lines to 88 lines, then from 93 lines to 72 lines *)
 (* coqc version trunk (September 2014) compiled on Sep 25 2014 2:53:46 with OCaml 4.01.0
    coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (bec7e0914f4a7144cd4efa8ffaccc9f72dbdb790) *)
diff --git a/test-suite/bugs/closed/3682.v b/test-suite/bugs/closed/3682.v
index b8c5b4d52..2a282d221 100644
--- a/test-suite/bugs/closed/3682.v
+++ b/test-suite/bugs/closed/3682.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Class Foo.
 Definition bar `{Foo} (x : Set) := Set.
 Instance: Foo.
diff --git a/test-suite/bugs/closed/3684.v b/test-suite/bugs/closed/3684.v
index 94ce4a608..f7b137386 100644
--- a/test-suite/bugs/closed/3684.v
+++ b/test-suite/bugs/closed/3684.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Definition foo : Set.
 Proof.
   refine ($(abstract admit)$).
diff --git a/test-suite/bugs/closed/3686.v b/test-suite/bugs/closed/3686.v
index ee6b334ba..b650920b2 100644
--- a/test-suite/bugs/closed/3686.v
+++ b/test-suite/bugs/closed/3686.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Set Universe Polymorphism.
 Set Implicit Arguments.
 Record PreCategory := { object :> Type ; morphism : object -> object -> Type }.
diff --git a/test-suite/bugs/closed/3698.v b/test-suite/bugs/closed/3698.v
index 3c53d243e..31de8ec45 100644
--- a/test-suite/bugs/closed/3698.v
+++ b/test-suite/bugs/closed/3698.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 5479 lines to 4682 lines, then from 4214 lines to 86 lines, then from 60 lines to 25 lines *)
 (* coqc version trunk (October 2014) compiled on Oct 1 2014 18:13:54 with OCaml 4.01.0
    coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (68846802a7be637ec805a5e374655a426b5723a5) *)
diff --git a/test-suite/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v
index 99b3d79e1..62137f0c0 100644
--- a/test-suite/bugs/closed/3699.v
+++ b/test-suite/bugs/closed/3699.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 9593 lines to 104 lines, then from 187 lines to 103 lines, then from 113 lines to 90 lines *)
 (* coqc version trunk (October 2014) compiled on Oct 1 2014 18:13:54 with OCaml 4.01.0
    coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (68846802a7be637ec805a5e374655a426b5723a5) *)
diff --git a/test-suite/bugs/closed/3703.v b/test-suite/bugs/closed/3703.v
index 8f7fe0a09..728250076 100644
--- a/test-suite/bugs/closed/3703.v
+++ b/test-suite/bugs/closed/3703.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 6746 lines to 4190 lines, then from 29 lines to 18 lines, then fro\
 m 30 lines to 19 lines *)
 (* coqc version trunk (October 2014) compiled on Oct 7 2014 12:42:41 with OCaml 4.01.0
diff --git a/test-suite/bugs/closed/3709.v b/test-suite/bugs/closed/3709.v
index 7f01be7ab..815f5b950 100644
--- a/test-suite/bugs/closed/3709.v
+++ b/test-suite/bugs/closed/3709.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Module NonPrim.
   Unset Primitive Projections.
   Record hProp := hp { hproptype :> Type }.
diff --git a/test-suite/bugs/closed/3732.v b/test-suite/bugs/closed/3732.v
index 6e5952a52..76beedf68 100644
--- a/test-suite/bugs/closed/3732.v
+++ b/test-suite/bugs/closed/3732.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 2073 lines to 358 lines, then from 359 lines to 218 lines, then from 107 lines to 92 lines *)
 (* coqc version trunk (October 2014) compiled on Oct 11 2014 1:13:41 with OCaml 4.01.0
    coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (d65496f09c4b68fa318783e53f9cd6d5c18e1eb7) *)
diff --git a/test-suite/bugs/closed/3782.v b/test-suite/bugs/closed/3782.v
index 08d456fc6..2dc50c17d 100644
--- a/test-suite/bugs/closed/3782.v
+++ b/test-suite/bugs/closed/3782.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 2674 lines to 136 lines, then from 115 lines to 61 lines *)
 (* coqc version trunk (October 2014) compiled on Oct 28 2014 14:33:38 with OCaml 4.01.0
    coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-trunk,(no branch) (53bfe9cf58a3c40e6eb7120d25c1633a9cea3126) *)
diff --git a/test-suite/bugs/closed/3783.v b/test-suite/bugs/closed/3783.v
index 33ca9651a..e21712968 100644
--- a/test-suite/bugs/closed/3783.v
+++ b/test-suite/bugs/closed/3783.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Fixpoint exp (n : nat) (T : Set)
   := match n with
        | 0 => T
diff --git a/test-suite/bugs/closed/3786.v b/test-suite/bugs/closed/3786.v
index fd3bd7bd7..23d19e946 100644
--- a/test-suite/bugs/closed/3786.v
+++ b/test-suite/bugs/closed/3786.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Require Coq.Lists.List.
 Require Coq.Sets.Ensembles.
 Import Coq.Sets.Ensembles.
diff --git a/test-suite/bugs/closed/3798.v b/test-suite/bugs/closed/3798.v
index 623822e99..b9f0daa71 100644
--- a/test-suite/bugs/closed/3798.v
+++ b/test-suite/bugs/closed/3798.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Require Setoid.
 
 Parameter f : nat -> nat.
diff --git a/test-suite/bugs/closed/3854.v b/test-suite/bugs/closed/3854.v
index f8329cdd2..7e915f202 100644
--- a/test-suite/bugs/closed/3854.v
+++ b/test-suite/bugs/closed/3854.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Definition relation (A : Type) := A -> A -> Type.
 Class Reflexive {A} (R : relation A) := reflexivity : forall x : A, R x x.
 Axiom IsHProp : Type -> Type.
diff --git a/test-suite/bugs/closed/3922.v b/test-suite/bugs/closed/3922.v
index 6b5241175..932084891 100644
--- a/test-suite/bugs/closed/3922.v
+++ b/test-suite/bugs/closed/3922.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Set Universe Polymorphism.
 Notation Type0 := Set.
 
diff --git a/test-suite/bugs/closed/3938.v b/test-suite/bugs/closed/3938.v
index 984431338..859e9f017 100644
--- a/test-suite/bugs/closed/3938.v
+++ b/test-suite/bugs/closed/3938.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Require Import Coq.Arith.PeanoNat.
 Hint Extern 1 => admit : typeclass_instances.
 Require Import Setoid.
diff --git a/test-suite/bugs/closed/4089.v b/test-suite/bugs/closed/4089.v
index 0ccbf5652..1449f242b 100644
--- a/test-suite/bugs/closed/4089.v
+++ b/test-suite/bugs/closed/4089.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 6522 lines to 318 lines, then from 1139 lines to 361 lines *)
 (* coqc version 8.5beta1 (February 2015) compiled on Feb 23 2015 18:32:3 with OCaml 4.01.0
diff --git a/test-suite/bugs/closed/4097.v b/test-suite/bugs/closed/4097.v
index 2109a4cd9..02aa25e09 100644
--- a/test-suite/bugs/closed/4097.v
+++ b/test-suite/bugs/closed/4097.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 6082 lines to 81 lines, then from 436 lines to 93 lines *)
 (* coqc version 8.5beta1 (February 2015) compiled on Feb 27 2015 15:10:37 with OCaml 4.01.0
    coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (fc1b3ef9d7270938cd83c524aae0383093b7a4b5) *)
diff --git a/test-suite/bugs/closed/HoTT_coq_007.v b/test-suite/bugs/closed/HoTT_coq_007.v
index 8592c729d..0b8bb2353 100644
--- a/test-suite/bugs/closed/HoTT_coq_007.v
+++ b/test-suite/bugs/closed/HoTT_coq_007.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Module Comment1.
   Set Implicit Arguments.
 
diff --git a/test-suite/bugs/closed/HoTT_coq_014.v b/test-suite/bugs/closed/HoTT_coq_014.v
index 63548a644..d00a707bd 100644
--- a/test-suite/bugs/closed/HoTT_coq_014.v
+++ b/test-suite/bugs/closed/HoTT_coq_014.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Set Implicit Arguments.
 Generalizable All Variables.
 Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/HoTT_coq_020.v b/test-suite/bugs/closed/HoTT_coq_020.v
index b16c1df2b..4938b80f9 100644
--- a/test-suite/bugs/closed/HoTT_coq_020.v
+++ b/test-suite/bugs/closed/HoTT_coq_020.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Set Implicit Arguments.
 
 Generalizable All Variables.
diff --git a/test-suite/bugs/closed/HoTT_coq_029.v b/test-suite/bugs/closed/HoTT_coq_029.v
index 4fd54b569..161c4d21e 100644
--- a/test-suite/bugs/closed/HoTT_coq_029.v
+++ b/test-suite/bugs/closed/HoTT_coq_029.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Module FirstComment.
   Set Implicit Arguments.
   Generalizable All Variables.
diff --git a/test-suite/bugs/closed/HoTT_coq_030.v b/test-suite/bugs/closed/HoTT_coq_030.v
index fa5ee25ca..9f8924834 100644
--- a/test-suite/bugs/closed/HoTT_coq_030.v
+++ b/test-suite/bugs/closed/HoTT_coq_030.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Set Implicit Arguments.
 Generalizable All Variables.
 Set Asymmetric Patterns.
diff --git a/test-suite/bugs/closed/HoTT_coq_035.v b/test-suite/bugs/closed/HoTT_coq_035.v
index 4ad2fc023..133bf6c73 100644
--- a/test-suite/bugs/closed/HoTT_coq_035.v
+++ b/test-suite/bugs/closed/HoTT_coq_035.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Fail Check Prop : Prop. (* Prop:Prop
      : Prop *)
 Fail Check Set : Prop. (* Set:Prop
diff --git a/test-suite/bugs/closed/HoTT_coq_042.v b/test-suite/bugs/closed/HoTT_coq_042.v
index 6b206a2f5..432cf7054 100644
--- a/test-suite/bugs/closed/HoTT_coq_042.v
+++ b/test-suite/bugs/closed/HoTT_coq_042.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Set Implicit Arguments.
 Set Universe Polymorphism.
 Generalizable All Variables.
diff --git a/test-suite/bugs/closed/HoTT_coq_055.v b/test-suite/bugs/closed/HoTT_coq_055.v
index 92d70ad13..a25098771 100644
--- a/test-suite/bugs/closed/HoTT_coq_055.v
+++ b/test-suite/bugs/closed/HoTT_coq_055.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
 Set Universe Polymorphism.
 
diff --git a/test-suite/bugs/closed/HoTT_coq_056.v b/test-suite/bugs/closed/HoTT_coq_056.v
index 6e65320d1..3e3a987a7 100644
--- a/test-suite/bugs/closed/HoTT_coq_056.v
+++ b/test-suite/bugs/closed/HoTT_coq_056.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from 10455 lines to 8350 lines, then from 7790 lines to 710 lines, then from 7790 lines to 710 lines, then from 566 lines to 340 lines, then from 191 lines to 171 lines, then from 191 lines to 171 lines. *)
 
 Set Implicit Arguments.
diff --git a/test-suite/bugs/closed/HoTT_coq_058.v b/test-suite/bugs/closed/HoTT_coq_058.v
index 9ce7dba97..5e5d5ab3e 100644
--- a/test-suite/bugs/closed/HoTT_coq_058.v
+++ b/test-suite/bugs/closed/HoTT_coq_058.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from 10044 lines to 493 lines, then from 425 lines to 160 lines. *)
 Set Universe Polymorphism.
 Notation idmap := (fun x => x).
diff --git a/test-suite/bugs/closed/HoTT_coq_061.v b/test-suite/bugs/closed/HoTT_coq_061.v
index 26c1f963d..19551dc92 100644
--- a/test-suite/bugs/closed/HoTT_coq_061.v
+++ b/test-suite/bugs/closed/HoTT_coq_061.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* There are some problems in materialize_evar with local definitions,
    as CO below; this is not completely sorted out yet, but at least
    it fails in a smooth way at the time of today [HH] *)
diff --git a/test-suite/bugs/closed/HoTT_coq_062.v b/test-suite/bugs/closed/HoTT_coq_062.v
index db8953168..b7db22a69 100644
--- a/test-suite/bugs/closed/HoTT_coq_062.v
+++ b/test-suite/bugs/closed/HoTT_coq_062.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
 (* File reduced by coq-bug-finder from 5012 lines to 4659 lines, then from 4220 lines to 501 lines, then from 513 lines to 495 lines, then from 513 lines to 495 lines, then from 412 lines to 79 lines, then from 412 lines to 79 lines. *)
 Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/HoTT_coq_064.v b/test-suite/bugs/closed/HoTT_coq_064.v
index 5f0a541b0..b4c745375 100644
--- a/test-suite/bugs/closed/HoTT_coq_064.v
+++ b/test-suite/bugs/closed/HoTT_coq_064.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from 279 lines to 219 lines. *)
 
 Set Implicit Arguments.
diff --git a/test-suite/bugs/closed/HoTT_coq_067.v b/test-suite/bugs/closed/HoTT_coq_067.v
index ad32a60c6..84a5bc029 100644
--- a/test-suite/bugs/closed/HoTT_coq_067.v
+++ b/test-suite/bugs/closed/HoTT_coq_067.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Set Universe Polymorphism.
 Inductive paths {A : Type} (a : A) : A -> Type :=
   idpath : paths a a.
diff --git a/test-suite/bugs/closed/HoTT_coq_088.v b/test-suite/bugs/closed/HoTT_coq_088.v
index b3e1df579..0428af0d4 100644
--- a/test-suite/bugs/closed/HoTT_coq_088.v
+++ b/test-suite/bugs/closed/HoTT_coq_088.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Inductive paths {A : Type} (a : A) : A -> Type :=
   idpath : paths a a.
 
diff --git a/test-suite/bugs/closed/HoTT_coq_090.v b/test-suite/bugs/closed/HoTT_coq_090.v
index 5c7041471..5fa167038 100644
--- a/test-suite/bugs/closed/HoTT_coq_090.v
+++ b/test-suite/bugs/closed/HoTT_coq_090.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (** I'm not sure if this tests what I want it to test... *)
 Set Implicit Arguments.
 Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/HoTT_coq_098.v b/test-suite/bugs/closed/HoTT_coq_098.v
index fc99daab6..bdcd8ba97 100644
--- a/test-suite/bugs/closed/HoTT_coq_098.v
+++ b/test-suite/bugs/closed/HoTT_coq_098.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Set Implicit Arguments.
 Generalizable All Variables.
 
diff --git a/test-suite/bugs/closed/HoTT_coq_099.v b/test-suite/bugs/closed/HoTT_coq_099.v
index 9b6ace824..cd5b0c8ff 100644
--- a/test-suite/bugs/closed/HoTT_coq_099.v
+++ b/test-suite/bugs/closed/HoTT_coq_099.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from 138 lines to 78 lines. *)
 Set Implicit Arguments.
 Generalizable All Variables.
diff --git a/test-suite/bugs/closed/HoTT_coq_100.v b/test-suite/bugs/closed/HoTT_coq_100.v
index c39b70934..663b6280e 100644
--- a/test-suite/bugs/closed/HoTT_coq_100.v
+++ b/test-suite/bugs/closed/HoTT_coq_100.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from 335 lines to 115 lines. *)
 Set Implicit Arguments.
 Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/HoTT_coq_101.v b/test-suite/bugs/closed/HoTT_coq_101.v
index 9c89a6ab9..3ef56892b 100644
--- a/test-suite/bugs/closed/HoTT_coq_101.v
+++ b/test-suite/bugs/closed/HoTT_coq_101.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
diff --git a/test-suite/bugs/closed/HoTT_coq_102.v b/test-suite/bugs/closed/HoTT_coq_102.v
index 71becfd2e..996aaaa49 100644
--- a/test-suite/bugs/closed/HoTT_coq_102.v
+++ b/test-suite/bugs/closed/HoTT_coq_102.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from 64 lines to 30 lines. *)
 Set Implicit Arguments.
 Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/HoTT_coq_107.v b/test-suite/bugs/closed/HoTT_coq_107.v
index c3a83627e..9a1da16bf 100644
--- a/test-suite/bugs/closed/HoTT_coq_107.v
+++ b/test-suite/bugs/closed/HoTT_coq_107.v
@@ -59,7 +59,7 @@ Instance trunc_sigma `{P : A -> Type}
 
 Proof.
   generalize dependent A.
-  induction n; [ | admit ]; simpl; intros A P ac Pc.
+  induction n; [ | apply admit ]; simpl; intros A P ac Pc.
   (exists (existT _ (center A) (center (P (center A))))).
   intros [a ?].
   refine (path_sigma' P (contr a) (path_contr _ _)).
@@ -102,5 +102,5 @@ The term
         | false => B
         end))" (Universe inconsistency: Cannot enforce Top.197 = Set)).
  *)
-  admit.
+  apply admit.
 Defined.
diff --git a/test-suite/bugs/closed/HoTT_coq_108.v b/test-suite/bugs/closed/HoTT_coq_108.v
index cc3048027..4f5ef9974 100644
--- a/test-suite/bugs/closed/HoTT_coq_108.v
+++ b/test-suite/bugs/closed/HoTT_coq_108.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
 (* NOTE: This bug is only triggered with -load-vernac-source / in interactive mode. *)
 (* File reduced by coq-bug-finder from 139 lines to 124 lines. *)
diff --git a/test-suite/bugs/closed/HoTT_coq_112.v b/test-suite/bugs/closed/HoTT_coq_112.v
index 150f2ecc8..5bee69fcd 100644
--- a/test-suite/bugs/closed/HoTT_coq_112.v
+++ b/test-suite/bugs/closed/HoTT_coq_112.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from 4464 lines to 4137 lines, then from 3683 lines to 118 lines, then from 124 lines to 75 lines. *)
 Set Universe Polymorphism.
 Definition admit {T} : T.
diff --git a/test-suite/bugs/closed/HoTT_coq_113.v b/test-suite/bugs/closed/HoTT_coq_113.v
index 3ef531bc9..05e767840 100644
--- a/test-suite/bugs/closed/HoTT_coq_113.v
+++ b/test-suite/bugs/closed/HoTT_coq_113.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 3329 lines to 153 lines, then from 118 lines to 49 lines, then from 55 lines to 38 lines, then from 46 lines to 16 lines *)
 
 Generalizable All Variables.
diff --git a/test-suite/bugs/closed/HoTT_coq_118.v b/test-suite/bugs/closed/HoTT_coq_118.v
index 14ad0e49d..e41689cba 100644
--- a/test-suite/bugs/closed/HoTT_coq_118.v
+++ b/test-suite/bugs/closed/HoTT_coq_118.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 5631 lines to 557 lines, then from 526 lines to 181 lines, then from 189 lines to 154 lines, then from 153 lines to 107 lines, then from 97 lines to 56 lines, then from 50 lines to 37 lines *)
 Generalizable All Variables.
 Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/HoTT_coq_121.v b/test-suite/bugs/closed/HoTT_coq_121.v
index cce288cff..90493a530 100644
--- a/test-suite/bugs/closed/HoTT_coq_121.v
+++ b/test-suite/bugs/closed/HoTT_coq_121.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, then from 146 lines to 72 lines, then from 82 lines to 70 lines, then from 79 lines to 49 lines, then from 59 lines to 16 lines *)
 
 Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/HoTT_coq_123.v b/test-suite/bugs/closed/HoTT_coq_123.v
index 994dff637..6ee6e6532 100644
--- a/test-suite/bugs/closed/HoTT_coq_123.v
+++ b/test-suite/bugs/closed/HoTT_coq_123.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") *)
 (* File reduced by coq-bug-finder from original input, then from 4988 lines to 856 lines, then from 648 lines to 398 lines, then from 401 lines to 332 lines, then from 287 lines to 250 lines, then from 257 lines to 241 lines, then from 223 lines to 175 lines *)
 Set Universe Polymorphism.
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.
diff --git a/test-suite/ide/undo020.fake b/test-suite/ide/undo020.fake
index 2adde908d..aa1d9bb2a 100644
--- a/test-suite/ide/undo020.fake
+++ b/test-suite/ide/undo020.fake
@@ -12,8 +12,8 @@ ADD { Qed. }
 # second proof
 ADD { Lemma b : False. }
 ADD { Proof using. }
-ADD { admit. }
-ADD last { Qed. }
+ADD { give_up. }
+ADD last { Admitted. }
 # We join and expect some proof to fail
 WAIT
 # Going back to the error
diff --git a/test-suite/prerequisite/admit.v b/test-suite/prerequisite/admit.v
new file mode 100644
index 000000000..fb3276632
--- /dev/null
+++ b/test-suite/prerequisite/admit.v
@@ -0,0 +1,2 @@
+Axiom proof_admitted : False.
+Ltac admit := case proof_admitted.
diff --git a/test-suite/success/AdvancedCanonicalStructure.v b/test-suite/success/AdvancedCanonicalStructure.v
index d819dc47a..563339739 100644
--- a/test-suite/success/AdvancedCanonicalStructure.v
+++ b/test-suite/success/AdvancedCanonicalStructure.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Section group_morphism.
 
 (* An example with default canonical structures *)
diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v
index d316e4a09..e38affd7f 100644
--- a/test-suite/success/Nsatz.v
+++ b/test-suite/success/Nsatz.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* compile en user    3m39.915s sur cachalot *)
 Require Import Nsatz.
 
diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v
index dbbd57ae0..61e73f858 100644
--- a/test-suite/success/proof_using.v
+++ b/test-suite/success/proof_using.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Section Foo.
 
 Variable a : nat.
diff --git a/test-suite/success/rewrite_dep.v b/test-suite/success/rewrite_dep.v
index fe250ae88..d0aafd383 100644
--- a/test-suite/success/rewrite_dep.v
+++ b/test-suite/success/rewrite_dep.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Require Import Setoid.
 Require Import Morphisms.
 Require Vector.
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
index be0d49e00..0465c4b3f 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Require Import Setoid.
 
 Parameter A : Set.
diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v
index b53307796..e540ae5f3 100644
--- a/test-suite/success/simpl.v
+++ b/test-suite/success/simpl.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* Check that inversion of names of mutual inductive fixpoints works *)
 (* (cf bug #1031) *)