Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

186 files changed, 1828 insertions, 127 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 4a3a287c..cffbe481 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -273,6 +273,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out
 	    | grep -v "Welcome to Coq" \
 	    | grep -v "\[Loading ML file" \
 	    | grep -v "Skipping rcfile loading" \
+	    | grep -v "^<W>" \
 	    > $$tmpoutput; \
 	  diff -u $*.out $$tmpoutput 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
diff --git a/test-suite/_CoqProject b/test-suite/_CoqProject
new file mode 100644
index 00000000..dc121311
--- /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 4b02d5f9..7d8ba5b8 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 35c69db2..85ad41d1 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/2406.v b/test-suite/bugs/closed/2406.v
index 1bd66ffc..3766e795 100644
--- a/test-suite/bugs/closed/2406.v
+++ b/test-suite/bugs/closed/2406.v
@@ -1,6 +1,6 @@
 (* Check correct handling of unsupported notations *)
 Notation "'’'" := (fun x => x) (at level 20).
 
-(* This fails with a syntax error but it is not catched by Fail
+(* This fails with a syntax error but it is not caught by Fail
 Fail Definition crash_the_rooster f := ’.
 *)
diff --git a/test-suite/bugs/closed/2473.v b/test-suite/bugs/closed/2473.v
index 4c302512..fb676c7e 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
new file mode 100644
index 00000000..4300de16
--- /dev/null
+++ b/test-suite/bugs/closed/2590.v
@@ -0,0 +1,20 @@
+Require Import TestSuite.admit.
+Require Import Relation_Definitions RelationClasses Setoid SetoidClass.
+
+Section Bug.
+
+  Context {A : Type} (R : relation A).
+  Hypothesis pre : PreOrder R.
+  Context `{SA : Setoid A}.
+
+  Goal True.
+  set (SA' := SA).
+    assert ( forall SA0 : Setoid A,
+               @PartialOrder A (@equiv A SA0) (@setoid_equiv A SA0) R pre ).
+    rename SA into SA0.
+    intro SA.
+    admit.
+    admit.
+Qed.
+End Bug.
+
diff --git a/test-suite/bugs/closed/2602.v b/test-suite/bugs/closed/2602.v
new file mode 100644
index 00000000..f0744788
--- /dev/null
+++ b/test-suite/bugs/closed/2602.v
@@ -0,0 +1,8 @@
+Goal exists m, S m > 0.
+eexists.
+match goal with
+ | |- context [ S ?a ] =>
+     match goal with
+       | |- S a > 0 => idtac
+     end
+end.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/2613.v b/test-suite/bugs/closed/2613.v
index 4f0470b1..15f3bf52 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 dde6a6a5..38c1cfc8 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/2775.v b/test-suite/bugs/closed/2775.v
new file mode 100644
index 00000000..f1f384bd
--- /dev/null
+++ b/test-suite/bugs/closed/2775.v
@@ -0,0 +1,6 @@
+Inductive typ : forall (T:Type), list T ->  Type -> Prop :=
+  | Get : forall (T:Type) (l:list T), typ T l T.
+
+
+Derive Inversion inv with 
+(forall (X: Type) (y: list nat), typ nat y X)  Sort Prop.
diff --git a/test-suite/bugs/closed/2830.v b/test-suite/bugs/closed/2830.v
index b72c821d..bb607b78 100644
--- a/test-suite/bugs/closed/2830.v
+++ b/test-suite/bugs/closed/2830.v
@@ -123,6 +123,7 @@ Module C.
 
 Reserved Notation "a ~> b" (at level 70, right associativity).
 Reserved Notation "a ≈ b" (at level 54).
+Reserved Notation "a ∘ b" (at level 50, left associativity).
 Generalizable All Variables.
 
 Class Category (Object:Type) (Hom:Object -> Object -> Type) := {
diff --git a/test-suite/bugs/closed/2883.v b/test-suite/bugs/closed/2883.v
index 5a5d90a4..f027b5eb 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/2946.v b/test-suite/bugs/closed/2946.v
new file mode 100644
index 00000000..d8138e14
--- /dev/null
+++ b/test-suite/bugs/closed/2946.v
@@ -0,0 +1,8 @@
+Lemma toto (E : nat -> nat -> Prop) (x y : nat)  
+  (Ex_ : forall z, E x z) (E_y : forall z, E z y) : True.
+
+(* OK *)                                                                     
+assert (pairE1 := let Exy := _ in (Ex_ y, E_y _) : Exy * Exy).               
+
+(* FAIL *)                                                                   
+assert (pairE2 := let Exy := _ in (Ex_ _, E_y x) : Exy * Exy).
diff --git a/test-suite/bugs/closed/2951.v b/test-suite/bugs/closed/2951.v
new file mode 100644
index 00000000..87d54441
--- /dev/null
+++ b/test-suite/bugs/closed/2951.v
@@ -0,0 +1,2 @@
+Record C (A: Type) : Type := { f: A }.
+Existing Class C.
diff --git a/test-suite/bugs/closed/2969.v b/test-suite/bugs/closed/2969.v
index ff75a1f3..a03adbd7 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 440cda61..d5409289 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 03e5af61..ced6d959 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/opened/3071.v b/test-suite/bugs/closed/3071.v
index 611ac606..53c2ef7b 100644
--- a/test-suite/bugs/opened/3071.v
+++ b/test-suite/bugs/closed/3071.v
@@ -2,4 +2,4 @@ Definition foo := True.
 
 Section foo.
   Global Arguments foo / .
-Fail End foo.
+End foo.
diff --git a/test-suite/bugs/closed/3199.v b/test-suite/bugs/closed/3199.v
new file mode 100644
index 00000000..08bf6249
--- /dev/null
+++ b/test-suite/bugs/closed/3199.v
@@ -0,0 +1,18 @@
+Axiom P : nat -> Prop.
+Axiom admit : forall n : nat, P n -> P n -> n = S n.
+Axiom foo : forall n, P n.
+
+Create HintDb bar.
+Hint Extern 3 => symmetry : bar.
+Hint Resolve admit : bar.
+Hint Immediate foo : bar.
+
+Lemma qux : forall n : nat, n = S n.
+Proof.
+intros n.
+eauto with bar.
+Defined.
+
+Goal True.
+pose (e := eq_refl (qux 0)); unfold qux in e.
+match type of e with context [eq_sym] => fail 1 | _ => idtac end.
diff --git a/test-suite/bugs/closed/3210.v b/test-suite/bugs/closed/3210.v
new file mode 100644
index 00000000..bb673f38
--- /dev/null
+++ b/test-suite/bugs/closed/3210.v
@@ -0,0 +1,22 @@
+(* Test support of let-in in arity of inductive types *)
+
+Inductive Foo : let X := Set in X :=
+| I : Foo.
+
+Definition foo (x : Foo) : bool :=
+  match x with
+  I => true
+  end.
+
+Definition foo' (x : Foo) : x = x.
+case x.
+match goal with |- I = I => idtac end. (* check form of the goal *)
+Undo 2.
+elim x.
+match goal with |- I = I => idtac end. (* check form of the goal *)
+Undo 2.
+induction x.
+match goal with |- I = I => idtac end. (* check form of the goal *)
+Undo 2.
+destruct x.
+match goal with |- I = I => idtac end. (* check form of the goal *)
diff --git a/test-suite/bugs/closed/3249.v b/test-suite/bugs/closed/3249.v
new file mode 100644
index 00000000..d41d2317
--- /dev/null
+++ b/test-suite/bugs/closed/3249.v
@@ -0,0 +1,11 @@
+Set Implicit Arguments.
+
+Ltac ret_and_left T :=
+  let t := type of T in
+  lazymatch eval hnf in t with
+    | ?a /\ ?b => constr:(proj1 T)
+    | forall x : ?T', @?f x =>
+      constr:(fun x : T' => $(let fx := constr:(T x) in
+                              let t := ret_and_left fx in
+                              exact t)$)
+  end.
diff --git a/test-suite/bugs/closed/3258.v b/test-suite/bugs/closed/3258.v
index a1390e30..b263c6ba 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 0306c686..aa91fc3d 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/opened/3298.v b/test-suite/bugs/closed/3298.v
index bce7c3f2..f07ee1e6 100644
--- a/test-suite/bugs/opened/3298.v
+++ b/test-suite/bugs/closed/3298.v
@@ -1,11 +1,11 @@
+Require Import TestSuite.admit.
 Module JGross.
   Hint Extern 1 => match goal with |- match ?E with end => case E end.
 
   Goal forall H : False, match H return Set with end.
   Proof.
     intros.
-    Fail solve [ eauto ]. (* No applicable tactic *)
-    admit.
+    solve [ eauto ].
   Qed.
 End JGross.
 
@@ -17,7 +17,6 @@ Section BenDelaware.
   Qed.
   Goal forall (H : False), match H return Set with end.
   Proof.
-    Fail solve [ eauto ] .
-    admit.
+    solve [ eauto ] .
   Qed.
 End BenDelaware.
diff --git a/test-suite/bugs/closed/3309.v b/test-suite/bugs/closed/3309.v
index fcebdec7..98043157 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.
@@ -321,6 +322,13 @@ Definition ispartlbinopabmonoidfracrel_type : Type :=
   forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ), 
     @abmonoidfracrel X A ( ( admit + z ) )admit.
 
-Axiom ispartlbinopabmonoidfracrel : $(let t:= eval unfold ispartlbinopabmonoidfracrel_type in
+Fail Timeout 1 Axiom ispartlbinopabmonoidfracrel' : $(let t:= eval unfold ispartlbinopabmonoidfracrel_type in
+                                      ispartlbinopabmonoidfracrel_type in exact t)$.
+
+Unset Kernel Term Sharing.
+
+Axiom ispartlbinopabmonoidfracrel : forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ) , @abmonoidfracrel X A ( ( admit + z ) )admit.
+
+Axiom ispartlbinopabmonoidfracrel' : $(let t:= eval unfold ispartlbinopabmonoidfracrel_type in
                                       ispartlbinopabmonoidfracrel_type in exact t)$.
 
diff --git a/test-suite/bugs/closed/3314.v b/test-suite/bugs/closed/3314.v
index 64786263..e63c46da 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 bb5853dd..3b37e39e 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 07e3b3cb..b6f10e53 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 925f22a2..ab3025a6 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 fb5a8a7e..22b1603b 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 9cd6e4c2..45dbb57a 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 f7e368f8..ecb09e84 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 15303cca..4cd7c39e 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 8255fd6c..880851c5 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 37c0d87e..63d5c7a5 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 30fdf169..c041c401 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 5ecf2801..051e6952 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 3c67703a..d8e72f4f 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 fe323fcb..d7ce02ea 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 1d8e9167..3e374d90 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 29ee1487..3a598695 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.
@@ -24,9 +25,8 @@ Proof.
   intros.
   refine (isequiv_adjointify (functor_forall f g)
                              (functor_forall (f^-1)
-                                             (fun (x:A) (y:Q (f^-1 x)) => @eisretr _ _ f _ x # (g (f^-1 x))^-1 y
-                             )) _ _); 
-  intros h.
+                                             (fun (x:A) (y:Q (f^-1 x)) => @eisretr _ _ f H x # (g (f^-1 x))^-1 y
+                             )) _ _); intros h.
   - abstract (
         apply path_forall; intros b; unfold functor_forall;
         rewrite eisadj;
@@ -37,4 +37,4 @@ Proof.
         rewrite eissect;
         apply apD
       ).
-Defined.
+Defined.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3393.v b/test-suite/bugs/closed/3393.v
index ec25e682..f7ab5f76 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 d984f623..460ae8f1 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 8483a4ec..374a5392 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 bba6140f..1ea24bf1 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/opened/3467.v b/test-suite/bugs/closed/3467.v
index 900bfc34..7e371162 100644
--- a/test-suite/bugs/opened/3467.v
+++ b/test-suite/bugs/closed/3467.v
@@ -2,5 +2,5 @@ Module foo.
   Notation x := $(exact I)$.
 End foo.
 Module bar.
-  Fail Include foo.
+  Include foo.
 End bar.
diff --git a/test-suite/bugs/closed/3480.v b/test-suite/bugs/closed/3480.v
index 99ac2efa..a81837e7 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 6c40a426..dc88a332 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/opened/3490.v b/test-suite/bugs/closed/3490.v
index e7a5caa1..e7a5caa1 100644
--- a/test-suite/bugs/opened/3490.v
+++ b/test-suite/bugs/closed/3490.v
diff --git a/test-suite/bugs/closed/3491.v b/test-suite/bugs/closed/3491.v
new file mode 100644
index 00000000..fd394ddb
--- /dev/null
+++ b/test-suite/bugs/closed/3491.v
@@ -0,0 +1,4 @@
+(* Was failing while building the _rect scheme, due to wrong computation of *)
+(* the number of non recursively uniform parameters in the presence of let-ins*)
+Inductive list (A : Type) (T := A) : Type :=
+    nil : list A | cons : T -> list T -> list A.
diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v
new file mode 100644
index 00000000..fcdfa005
--- /dev/null
+++ b/test-suite/bugs/closed/3513.v
@@ -0,0 +1,76 @@
+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.
+Generalizable All Variables.
+Axiom admit : forall {T}, T.
+Class Equiv (A : Type) := equiv : relation A.
+Class type (A : Type) {e : Equiv A} := eq_equiv : Equivalence equiv.
+Class ILogicOps Frm := { lentails: relation Frm;
+                         ltrue: Frm;
+                         land: Frm -> Frm -> Frm;
+                         lor: Frm -> Frm -> Frm }.
+Infix "|--"  := lentails (at level 79, no associativity).
+Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }.
+Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P.
+Infix "-|-"  := lequiv (at level 85, no associativity).
+Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit.
+Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }.
+Section ILogic_Fun.
+  Context (T: Type) `{TType: type T}.
+  Context `{IL: ILogic Frm}.
+  Local Instance ILFun_Ops : ILogicOps (@ILFunFrm T _ Frm _) := admit.
+  Definition ILFun_ILogic : ILogic (@ILFunFrm T _ Frm _) := admit.
+End ILogic_Fun.
+Implicit Arguments ILFunFrm [[ILOps] [e]].
+Instance ILogicOps_Prop : ILogicOps Prop | 2 := {| lentails P Q := (P : Prop) -> Q;
+                                                   ltrue        := True;
+                                                   land     P Q := P /\ Q;
+                                                   lor      P Q := P \/ Q |}.
+Axiom Action : Set.
+Definition Actions := list Action.
+Instance ActionsEquiv : Equiv Actions := { equiv a1 a2 := a1 = a2 }.
+Definition OPred := ILFunFrm Actions Prop.
+Local Existing Instance ILFun_Ops.
+Local Existing Instance ILFun_ILogic.
+Definition catOP (P Q: OPred) : OPred := admit.
+Add Parametric Morphism : catOP with signature lentails ==> lentails ==> lentails as catOP_entails_m.
+admit.
+Defined.
+Definition catOPA (P Q R : OPred) : catOP (catOP P Q) R -|- catOP P (catOP Q R) := admit.
+Class IsPointed (T : Type) := point : T.
+Notation IsPointed_OPred P := (IsPointed (exists x : Actions, (P : OPred) x)).
+Record PointedOPred := mkPointedOPred {
+                           OPred_pred :> OPred;
+                           OPred_inhabited: IsPointed_OPred OPred_pred
+                         }.
+Existing Instance OPred_inhabited.
+Canonical Structure default_PointedOPred O `{IsPointed_OPred O} : PointedOPred
+  := {| OPred_pred := O ; OPred_inhabited := _ |}.
+Instance IsPointed_catOP `{IsPointed_OPred P, IsPointed_OPred Q} : IsPointed_OPred (catOP P Q) := admit.
+Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred)
+            (tr : T -> T) (O2 : PointedOPred) (x : T)
+            (H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0),
+     exists e1 e2,
+       catOP (O0 e1) (OPred_pred e2) |-- catOP (O1 x) O2.
+  intros; do 2 esplit.
+  rewrite <- catOPA.
+  lazymatch goal with
+  | |- ?R (?f ?a ?b) (?f ?a' ?b') =>
+    let P := constr:(fun H H' => @Morphisms.proper_prf (OPred -> OPred -> OPred)
+         (@Morphisms.respectful OPred (OPred -> OPred)
+            (@lentails OPred
+               (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop))
+            (@lentails OPred
+               (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop) ==>
+             @lentails OPred
+               (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop))) catOP
+         catOP_entails_m_Proper a a' H b b' H') in
+    pose P;
+    refine (P _ _)
+  end; unfold Basics.flip.
+  2: solve [ apply reflexivity ].
+  Undo.
+  2: reflexivity. (* Toplevel input, characters 18-29:
+Error:
+Tactic failure: The relation lentails is not a declared reflexive relation. Maybe you need to require the Setoid library. *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3531.v b/test-suite/bugs/closed/3531.v
index fd080a6b..764a7334 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/3560.v b/test-suite/bugs/closed/3560.v
new file mode 100644
index 00000000..65ce4fb6
--- /dev/null
+++ b/test-suite/bugs/closed/3560.v
@@ -0,0 +1,15 @@
+
+(* 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.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3561.v b/test-suite/bugs/closed/3561.v
index b4dfd17f..f6cbc929 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
new file mode 100644
index 00000000..3ef9270d
--- /dev/null
+++ b/test-suite/bugs/closed/3590.v
@@ -0,0 +1,12 @@
+Set Implicit Arguments.
+Record prod A B := pair { fst : A ; snd : B }.
+Definition idS := Set.
+Goal forall x y : prod Set Set, forall H : fst x = fst y, fst x = fst y.
+  intros.
+  change (@fst _ _ ?z) with (@fst Set idS z) at 2.
+  apply H.
+Qed.
+  
+(* Toplevel input, characters 20-58:
+Error: Failed to get enough information from the left-hand side to type the
+right-hand side. *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3596.v b/test-suite/bugs/closed/3596.v
index d6c1c949..49dd7be5 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/3612.v b/test-suite/bugs/closed/3612.v
new file mode 100644
index 00000000..9125ab16
--- /dev/null
+++ b/test-suite/bugs/closed/3612.v
@@ -0,0 +1,47 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter" "-nois") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 3595 lines to 3518 lines, then from 3133 lines to 2950 lines, then from 2911 lines to 415 lines, then from 431 lines to 407 \
+lines, then from 421 lines to 428 lines, then from 444 lines to 429 lines, then from 434 lines to 66 lines, then from 163 lines to 48 lines *)
+(* coqc version trunk (September 2014) compiled on Sep 11 2014 14:48:8 with OCaml 4.01.0
+   coqtop version cagnode17:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (580b25e05c7cc9e7a31430b3d9edb14ae12b7598) *)
+Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
+Reserved Notation "x = y  :>  T" (at level 70, y at next level, no associativity).
+Reserved Notation "x = y" (at level 70, no associativity).
+Open Scope type_scope.
+Global Set Universe Polymorphism.
+Notation "A -> B" := (forall (_ : A), B) : type_scope.
+Generalizable All Variables.
+Local Set Primitive Projections.
+Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
+Arguments projT1 {A P} _ / .
+Arguments projT2 {A P} _ / .
+Notation "( x ; y )" := (existT _ x y) : fibration_scope.
+Open Scope fibration_scope.
+Notation pr1 := projT1.
+Notation pr2 := projT2.
+Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
+Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+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) : path_scope.
+Local Open Scope path_scope.
+Axiom pr1_path : forall `{P : A -> Type} {u v : sigT P} (p : u = v), u.1 = v.1.
+Notation "p ..1" := (pr1_path p) (at level 3) : fibration_scope.
+Axiom pr2_path : forall `{P : A -> Type} {u v : sigT P} (p : u = v), p..1 # u.2 = v.2.
+Notation "p ..2" := (pr2_path p) (at level 3) : fibration_scope.
+Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P)
+           (p q : u = v)
+           (r : p..1 = q..1)
+           (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2),
+p = q.
+Goal forall (A : Type) (B : forall _ : A, Type) (x : @sigT A (fun x : A => B x))
+            (xx : @paths (@sigT A (fun x0 : A => B x0)) x x),
+       @paths (@paths (@sigT A (fun x0 : A => B x0)) x x) xx
+              (@idpath (@sigT A (fun x0 : A => B x0)) x).
+  intros A B x xx.
+  Set Printing All.
+  change (fun x => B x) with B in xx.
+  pose (path_path_sigma B x x xx) as x''.
+  clear x''.
+  Check (path_path_sigma B x x xx).
diff --git a/test-suite/bugs/closed/3625.v b/test-suite/bugs/closed/3625.v
index 3d30b62f..d4b2cc5c 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 cd542c8a..495e67e0 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/3649.v b/test-suite/bugs/closed/3649.v
new file mode 100644
index 00000000..06188e7b
--- /dev/null
+++ b/test-suite/bugs/closed/3649.v
@@ -0,0 +1,57 @@
+(* -*- coq-prog-args: ("-emacs" "-nois") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 9518 lines to 404 lines, then from 410 lines to 208 lines, then from 162 lines to 77 lines *)
+(* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0
+   coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *)
+Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
+Reserved Notation "x = y" (at level 70, no associativity).
+Open Scope type_scope.
+Axiom admit : forall {T}, T.
+Notation "A -> B" := (forall (_ : A), B) : type_scope.
+Reserved Infix "o" (at level 40, left associativity).
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
+Ltac constr_eq a b := let test := constr:(@idpath _ _ : a = b) in idtac.
+Global Set Primitive Projections.
+Delimit Scope morphism_scope with morphism.
+Record PreCategory :=
+  { object :> Type;
+    morphism : object -> object -> Type;
+
+    identity : forall x, morphism x x;
+    compose : forall s d d',
+                morphism d d'
+                -> morphism s d
+                -> morphism s d'
+    where "f 'o' g" := (compose f g) }.
+Infix "o" := (@compose _ _ _ _) : morphism_scope.
+Set Implicit Arguments.
+Local Open Scope morphism_scope.
+Record Functor (C D : PreCategory) :=
+  { object_of :> C -> D;
+    morphism_of : forall s d, morphism C s d
+                              -> morphism D (object_of s) (object_of d) }.
+Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) :=
+  { morphism_inverse : morphism C d s }.
+Record NaturalTransformation C D (F G : Functor C D) := { components_of :> forall c, morphism D (F c) (G c) }.
+Definition composeT C D (F F' F'' : Functor C D) (T' : NaturalTransformation F' F'') (T : NaturalTransformation F F')
+: NaturalTransformation F F''.
+  exact admit.
+Defined.
+Definition functor_category (C D : PreCategory) : PreCategory.
+  exact (@Build_PreCategory (Functor C D)
+                            (@NaturalTransformation C D)
+                            admit
+                            (@composeT C D)).
+Defined.
+Goal forall (C D : PreCategory) (G G' : Functor C D)
+            (T : @NaturalTransformation C D G G')
+            (H : @IsIsomorphism (@functor_category C D) G G' T)
+            (x : C),
+       @paths (morphism D (G x) (G x))
+              (@compose D (G x) (G' x) (G x)
+                        ((@morphism_inverse (@functor_category C D) G G' T H) x)
+                        (T x)) (@identity D (G x)).
+  intros.
+  (** This [change] succeeded, but did not progress, in 07e4438bd758c2ced8caf09a6961ccd77d84e42b, because [T0 x o T1 x] was not found in the goal *)
+  let T0 := match goal with |- context[components_of ?T0 ?x o components_of ?T1 ?x] => constr:(T0) end in
+  let T1 := match goal with |- context[components_of ?T0 ?x o components_of ?T1 ?x] => constr:(T1) end in
+  progress change (T0 x o T1 x) with ((fun y => y) (T0 x o T1 x)).
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3653.v b/test-suite/bugs/closed/3653.v
index 947b3601..b9768967 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 b1158b9a..622c3c94 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 ed8964ce..39eb89c4 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 41de74ff..63a81b6d 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 547159b9..da01ed00 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/opened/3681.v b/test-suite/bugs/closed/3681.v
index 194113c6..194113c6 100644
--- a/test-suite/bugs/opened/3681.v
+++ b/test-suite/bugs/closed/3681.v
diff --git a/test-suite/bugs/closed/3682.v b/test-suite/bugs/closed/3682.v
index b8c5b4d5..2a282d22 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 94ce4a60..f7b13738 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 ee6b334b..b650920b 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/3690.v b/test-suite/bugs/closed/3690.v
new file mode 100644
index 00000000..4069e380
--- /dev/null
+++ b/test-suite/bugs/closed/3690.v
@@ -0,0 +1,52 @@
+Set Printing Universes.
+Set Universe Polymorphism.
+Definition foo (a := Type) (b := Type) (c := Type) := Type.
+Print foo.
+(* foo =
+let a := Type@{Top.1} in
+let b := Type@{Top.2} in let c := Type@{Top.3} in Type@{Top.4}
+     : Type@{Top.4+1}
+(* Top.1
+   Top.2
+   Top.3
+   Top.4 |=  *) *)
+Check @foo. (* foo@{Top.5 Top.6 Top.7
+Top.8}
+     : Type@{Top.8+1}
+(* Top.5
+   Top.6
+   Top.7
+   Top.8 |=  *) *)
+Definition bar := $(let t := eval compute in foo in exact t)$.
+Check @bar. (* bar@{Top.13 Top.14 Top.15
+Top.16}
+     : Type@{Top.16+1}
+(* Top.13
+   Top.14
+   Top.15
+   Top.16 |=  *) *)
+(* The following should fail, since [bar] should only need one universe. *)
+Check @bar@{i j}.
+Definition baz (a := Type) (b := Type : a) (c := Type : b) := a -> c.
+Definition qux := Eval compute in baz.
+Check @qux. (* qux@{Top.24 Top.25
+Top.26}
+     : Type@{max(Top.24+1, Top.26+1)}
+(* Top.24
+   Top.25
+   Top.26 |= Top.25 < Top.24
+              Top.26 < Top.25
+               *) *)
+Print qux. (* qux =
+Type@{Top.21} -> Type@{Top.23}
+     : Type@{max(Top.21+1, Top.23+1)}
+(* Top.21
+   Top.22
+   Top.23 |= Top.22 < Top.21
+              Top.23 < Top.22
+               *) *)
+Fail Check @qux@{Set Set}.
+Fail Check @qux@{Set Set Set}.
+(* [qux] should only need two universes *)
+Check @qux@{i j k}.  (* Error: The command has not failed!, but I think this is suboptimal *)
+Fail Check @qux@{i j}.
diff --git a/test-suite/bugs/closed/3698.v b/test-suite/bugs/closed/3698.v
index 3c53d243..31de8ec4 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 99b3d79e..62137f0c 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
new file mode 100644
index 00000000..72825007
--- /dev/null
+++ b/test-suite/bugs/closed/3703.v
@@ -0,0 +1,32 @@
+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
+   coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (2313bde0116a5916912bebbaca77d291f7b2760a) *)
+Record PreCategory := { identity : forall x, x -> x }.
+Definition set_cat : PreCategory := @Build_PreCategory (fun T x => x).
+Module UnKeyed.
+  Global Unset Keyed Unification.
+  Goal forall (T : Type) (g0 g1 : T) (k : T) (H' : forall x : T, k = @identity set_cat T x),
+         ((fun x : T => x) g0) = ((fun x : T => x) g1).
+    intros T g0 g1 k H'.
+    change (identity _ _) with (fun y : T => y) in H';
+      rewrite <- H' || fail "too early".
+    Undo.
+    rewrite <- H'.
+    admit.
+  Defined.
+End UnKeyed.
+Module Keyed.
+  Global Set Keyed Unification.
+  Declare Equivalent Keys (fun x => _) identity.
+  Goal forall (T : Type) (g0 g1 : T) (k : T) (H' : forall x : T, k = @identity set_cat T x),
+         ((fun x : T => x) g0) = ((fun x : T => x) g1).
+    intros T g0 g1 k H'.
+    change (identity _ _) with (fun y : T => y) in H';
+      rewrite <- H' || fail "too early".
+    Undo.
+    rewrite <- H'.
+    admit.
+  Defined.
+End Keyed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3709.v b/test-suite/bugs/closed/3709.v
index 7f01be7a..815f5b95 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
new file mode 100644
index 00000000..76beedf6
--- /dev/null
+++ b/test-suite/bugs/closed/3732.v
@@ -0,0 +1,105 @@
+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) *)
+Require Coq.Lists.List.
+
+Import Coq.Lists.List.
+
+Set Implicit Arguments.
+Global Set Asymmetric Patterns.
+
+Section machine.
+  Variables pc state : Type.
+
+  Inductive propX (i := pc) (j := state) : list Type -> Type :=
+  | Inj : forall G, Prop -> propX G
+  | ExistsX : forall G A, propX (A :: G) -> propX G.
+
+  Implicit Arguments Inj [G].
+
+  Definition PropX := propX nil.
+  Fixpoint last (G : list Type) : Type.
+    exact (match G with
+             | nil => unit
+             | T :: nil => T
+             | _ :: G' => last G'
+           end).
+  Defined.
+  Fixpoint eatLast (G : list Type) : list Type.
+    exact (match G with
+             | nil => nil
+             | _ :: nil => nil
+             | x :: G' => x :: eatLast G'
+           end).
+  Defined.
+
+  Fixpoint subst G (p : propX G) : (last G -> PropX) -> propX (eatLast G) :=
+    match p with
+      | Inj _ P => fun _ => Inj P
+      | ExistsX G A p1 => fun p' =>
+                            match G return propX (A :: G) -> propX (eatLast (A :: G)) -> propX (eatLast G) with
+                              | nil => fun p1 _ => ExistsX p1
+                              | _ :: _ => fun _ rc => ExistsX rc
+                            end p1 (subst p1 (match G return (last G -> PropX) -> last (A :: G) -> PropX with
+                                                | nil => fun _ _ => Inj True
+                                                | _ => fun p' => p'
+                                              end p'))
+    end.
+
+  Definition spec := state -> PropX.
+  Definition codeSpec := pc -> option spec.
+
+  Inductive valid (specs : codeSpec) (G : list PropX) : PropX -> Prop := Env : forall P, In P G -> valid specs G P.
+  Definition interp specs := valid specs nil.
+End machine.
+Notation "'ExX' : A , P" := (ExistsX (A := A) P) (at level 89) : PropX_scope.
+Bind Scope PropX_scope with PropX propX.
+Variables pc state : Type.
+
+Inductive subs : list Type -> Type :=
+| SNil : subs nil
+| SCons : forall T Ts, (last (T :: Ts) -> PropX pc state) -> subs (eatLast (T :: Ts)) -> subs (T :: Ts).
+
+Fixpoint SPush G T (s : subs G) (f : T -> PropX pc state) : subs (T :: G) :=
+  match s in subs G return subs (T :: G) with
+    | SNil => SCons _ nil f SNil
+    | SCons T' Ts f' s' => SCons T (T' :: Ts) f' (SPush s' f)
+  end.
+
+Fixpoint Substs G (s : subs G) : propX pc state G -> PropX pc state :=
+  match s in subs G return propX pc state G -> PropX pc state with
+    | SNil => fun p => p
+    | SCons _ _ f s' => fun p => Substs s' (subst p f)
+  end.
+Variable specs : codeSpec pc state.
+
+Lemma simplify_fwd_ExistsX : forall G A s (p : propX pc state (A :: G)),
+                               interp specs (Substs s (ExX  : A, p))
+                               -> exists a, interp specs (Substs (SPush s a) p).
+admit.
+Defined.
+
+Goal    forall (G : list Type) (A : Type) (p : propX pc state (@cons Type A G))
+               (s : subs G)
+               (_ : @interp pc state specs (@Substs G s (@ExistsX pc state G A p)))
+               (P : forall _ : subs (@cons Type A G), Prop)
+               (_ : forall (s0 : subs (@cons Type A G))
+                           (_ : @interp pc state specs (@Substs (@cons Type A G) s0 p)),
+                      P s0),
+          @ex (forall _ : A, PropX pc state)
+              (fun a : forall _ : A, PropX pc state => P (@SPush G A s a)).
+  intros ? ? ? ? H ? H'.
+  apply simplify_fwd_ExistsX in H.
+  firstorder. 
+Qed.
+ (* Toplevel input, characters 15-19:
+Error: Illegal application:
+The term "cons" of type "forall A : Type, A -> list A -> list A"
+cannot be applied to the terms
+ "Type" : "Type"
+ "T" : "Type"
+ "G0" : "list Type"
+The 2nd term has type "Type@{Top.53}" which should be coercible to
+ "Type@{Top.12}".
+ *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3755.v b/test-suite/bugs/closed/3755.v
new file mode 100644
index 00000000..77427ace
--- /dev/null
+++ b/test-suite/bugs/closed/3755.v
@@ -0,0 +1,16 @@
+(* File reduced by coq-bug-finder from original input, then from 6729 lines to 
+411 lines, then from 148 lines to 115 lines, then from 99 lines to 70 lines, 
+then from 85 lines to 63 lines, then from 76 lines to 55 lines, then from 61 
+lines to 17 lines *)
+(* coqc version trunk (January 2015) compiled on Jan 17 2015 21:58:5 with OCaml 
+4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk 
+(9e6b28c04ad98369a012faf3bd4d630cf123a473) *)
+Set Printing Universes.
+Section param.
+  Variable typeD : Set -> Set.
+  Variable STex : forall (T : Type) (p : T -> Set), Set.
+  Definition existsEach_cons' v (P : @sigT _ typeD -> Set) :=
+    @STex _ (fun x => P (@existT _ _ v x)).
+
+  Check @existT _ _ STex STex.
diff --git a/test-suite/bugs/closed/3782.v b/test-suite/bugs/closed/3782.v
index 08d456fc..2dc50c17 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
new file mode 100644
index 00000000..e2171296
--- /dev/null
+++ b/test-suite/bugs/closed/3783.v
@@ -0,0 +1,33 @@
+Require Import TestSuite.admit.
+Fixpoint exp (n : nat) (T : Set)
+  := match n with
+       | 0 => T
+       | S n' => exp n' (T * T)
+     end.
+Definition big := Eval compute in exp 13 nat.
+Module NonPrim.
+  Unset Primitive Projections.
+  Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
+  Definition x : sigT (fun x => x).
+  Proof.
+    exists big; admit.
+  Defined.
+  Goal True.
+    pose ((fun y => y = y) (projT1 _ x)) as y.
+    Time cbv beta in y. (* 0s *)
+    admit.
+  Defined.
+End NonPrim.
+Module Prim.
+  Set Primitive Projections.
+  Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
+  Definition x : sigT (fun x => x).
+  Proof.
+    exists big; admit.
+  Defined.
+  Goal True.
+    pose ((fun y => y = y) (projT1 _ x)) as y.
+    Timeout 1 cbv beta in y. (* takes around 2s.  Grows with the value passed to [exp] above *)
+    admit.
+  Defined.
+End Prim.
\ No newline at end of file
diff --git a/test-suite/bugs/opened/3786.v b/test-suite/bugs/closed/3786.v
index 5a124115..23d19e94 100644
--- a/test-suite/bugs/opened/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.
@@ -26,15 +27,7 @@ Definition sumUniqueImpl (ls : list nat)
 Proof.
   eexists.
   match goal with
-    | [ |- refine ?a ?b ] => let a' := eval hnf in a in refine (_ : refine a' b)
-  end;
-  try setoid_rewrite (@finite_set_handle_cardinal).
-  Undo.
-  match goal with
     | [ |- refine ?a ?b ] => let a' := eval hnf in a in change (refine a' b)
   end.
-  try setoid_rewrite (@finite_set_handle_cardinal). (* Anomaly: Uncaught exception Invalid_argument("decomp_pointwise").
-Please report. *)
-  instantiate (1 := admit).
-  admit.
-Defined.
+  try setoid_rewrite (@finite_set_handle_cardinal).
+Abort.
diff --git a/test-suite/bugs/closed/3798.v b/test-suite/bugs/closed/3798.v
new file mode 100644
index 00000000..b9f0daa7
--- /dev/null
+++ b/test-suite/bugs/closed/3798.v
@@ -0,0 +1,12 @@
+Require Import TestSuite.admit.
+Require Setoid.
+
+Parameter f : nat -> nat.
+Axiom a : forall n, 0 < n -> f n = 0.
+Hint Rewrite a using ( simpl; admit ).
+
+Goal f 1 = 0.
+Proof.
+  rewrite_strat (topdown (hints core)).
+  reflexivity.
+Qed.
diff --git a/test-suite/bugs/closed/3808.v b/test-suite/bugs/closed/3808.v
new file mode 100644
index 00000000..6e19ddf8
--- /dev/null
+++ b/test-suite/bugs/closed/3808.v
@@ -0,0 +1,2 @@
+Inductive Foo : (let enforce := (fun x => x) : Type@{j} -> Type@{i} in Type@{i})
+  := foo : Foo.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3815.v b/test-suite/bugs/closed/3815.v
new file mode 100644
index 00000000..5fb48398
--- /dev/null
+++ b/test-suite/bugs/closed/3815.v
@@ -0,0 +1,9 @@
+Require Import Setoid Coq.Program.Basics.
+Global Open Scope program_scope.
+Axiom foo : forall A (f : A -> A), f ∘ f = f.
+Require Import Coq.Program.Combinators.
+Hint Rewrite foo.
+Theorem t {A B C D} (f : A -> A) (g : B -> C) (h : C -> D)
+: f ∘ f = f.
+Proof.
+  rewrite_strat topdown (hints core).
diff --git a/test-suite/bugs/closed/3854.v b/test-suite/bugs/closed/3854.v
index f8329cdd..7e915f20 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/3881.v b/test-suite/bugs/closed/3881.v
new file mode 100644
index 00000000..4408ab88
--- /dev/null
+++ b/test-suite/bugs/closed/3881.v
@@ -0,0 +1,35 @@
+(* -*- coq-prog-args: ("-emacs" "-nois" "-R" "../theories" "Coq") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 2236 lines to 1877 lines, then from 1652 lines to 160 lines, then from 102 lines to 34 lines *)
+(* coqc version trunk (December 2014) compiled on Dec 23 2014 22:6:43 with OCaml 4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (90ed6636dea41486ddf2cc0daead83f9f0788163) *)
+Generalizable All Variables.
+Require Import Coq.Init.Notations.
+Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
+Notation "A -> B" := (forall (_ : A), B) : type_scope.
+Axiom admit : forall {T}, T.
+Notation "g 'o' f" := (fun x => g (f x)) (at level 40, left associativity).
+Notation "g 'o' f" := $(let g' := g in let f' := f in exact (fun x => g' (f' x)))$ (at level 40, left associativity). (* Ensure that x is not captured in [g] or [f] in case they contain holes *)
+Inductive eq {A} (x:A) : A -> Prop := eq_refl : x = x where "x = y" := (@eq _ x y) : type_scope.
+Arguments eq_refl {_ _}.
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with eq_refl => eq_refl end.
+Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A ; eisretr : forall x, f (equiv_inv x) = x }.
+Arguments eisretr {A B} f {_} _.
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'").
+Global Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g} : IsEquiv (g o f) | 1000 := admit.
+Definition isequiv_homotopic {A B} (f : A -> B) (g : A -> B) `{IsEquiv A B f} (h : forall x, f x = g x) : IsEquiv g := admit.
+Global Instance isequiv_inverse {A B} (f : A -> B) {feq : IsEquiv f} : IsEquiv f^-1 | 10000 := admit.
+Definition cancelR_isequiv {A B C} (f : A -> B) {g : B -> C} `{IsEquiv A B f} `{IsEquiv A C (g o f)} : IsEquiv g.
+Proof.
+  pose (fun H => @isequiv_homotopic _ _ ((g o f) o f^-1) _ H
+                                    (fun b => ap g (eisretr f b))) as k.
+  revert k.
+  let x := match goal with |- let k := ?x in _ => constr:x end in
+  intro k; clear k;
+  pose (x _).
+  pose (@isequiv_homotopic _ _ ((g o f) o f^-1) g _
+                           (fun b => ap g (eisretr f b))).
+  Undo. 
+  apply (@isequiv_homotopic _ _ ((g o f) o f^-1) g _
+                           (fun b => ap g (eisretr f b))).
+Qed.
+  
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3900.v b/test-suite/bugs/closed/3900.v
new file mode 100644
index 00000000..6be2161c
--- /dev/null
+++ b/test-suite/bugs/closed/3900.v
@@ -0,0 +1,13 @@
+Global Set Primitive Projections.
+Set Implicit Arguments.
+Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
+Record PreCategory := { object :> Type ; morphism : object -> object -> Type }.
+Variable A : PreCategory.
+Variable Pobj : A -> Type.
+Local Notation obj := (sigT Pobj).
+Variable Pmor : forall s d : obj, morphism A (projT1 s) (projT1 d) -> Type.
+Class Foo (x : Type) := { _ : forall y, y }.
+Local Instance ishset_pmor {s d m} : Foo (Pmor s d m).
+Proof.
+SearchAbout ((forall _ _, _) -> Foo _).
+Abort.
diff --git a/test-suite/bugs/closed/3916.v b/test-suite/bugs/closed/3916.v
new file mode 100644
index 00000000..55c3a35c
--- /dev/null
+++ b/test-suite/bugs/closed/3916.v
@@ -0,0 +1,3 @@
+Require Import List.
+Fail Hint Resolve -> in_map.
+
diff --git a/test-suite/bugs/closed/3922.v b/test-suite/bugs/closed/3922.v
new file mode 100644
index 00000000..93208489
--- /dev/null
+++ b/test-suite/bugs/closed/3922.v
@@ -0,0 +1,84 @@
+Require Import TestSuite.admit.
+Set Universe Polymorphism.
+Notation Type0 := Set.
+
+Definition Type1 := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}.
+
+Notation compose := (fun g f x => g (f x)).
+
+Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope.
+Open Scope function_scope.
+
+Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x)
+  := forall x:A, f x = g x.
+
+Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope.
+
+Class Contr_internal (A : Type) := BuildContr {
+  center : A ;
+  contr : (forall y : A, center = y)
+}.
+
+Inductive trunc_index : Type :=
+| minus_two : trunc_index
+| trunc_S : trunc_index -> trunc_index.
+
+Notation "n .+1" := (trunc_S n) (at level 2, left associativity, format "n .+1") : trunc_scope.
+Local Open Scope trunc_scope.
+Notation "-2" := minus_two (at level 0) : trunc_scope.
+Notation "-1" := (-2.+1) (at level 0) : trunc_scope.
+
+Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
+  match n with
+    | -2 => Contr_internal A
+    | n'.+1 => forall (x y : A), IsTrunc_internal n' (x = y)
+  end.
+
+Class IsTrunc (n : trunc_index) (A : Type) : Type :=
+  Trunc_is_trunc : IsTrunc_internal n A.
+
+Notation Contr := (IsTrunc -2).
+Notation IsHProp := (IsTrunc -1).
+
+Monomorphic Axiom dummy_funext_type : Type0.
+Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }.
+
+Inductive Unit : Type1 :=
+    tt : Unit.
+
+Record TruncType (n : trunc_index) := BuildTruncType {
+  trunctype_type : Type ;
+  istrunc_trunctype_type : IsTrunc n trunctype_type
+}.
+
+Arguments BuildTruncType _ _ {_}.
+
+Coercion trunctype_type : TruncType >-> Sortclass.
+
+Notation "n -Type" := (TruncType n) (at level 1) : type_scope.
+Notation hProp := (-1)-Type.
+
+Notation BuildhProp := (BuildTruncType -1).
+
+Private Inductive Trunc (n : trunc_index) (A :Type) : Type :=
+  tr : A -> Trunc n A.
+Arguments tr {n A} a.
+
+Global Instance istrunc_truncation (n : trunc_index) (A : Type@{i})
+: IsTrunc@{j} n (Trunc@{i} n A).
+Admitted.
+
+Definition Trunc_ind {n A}
+  (P : Trunc n A -> Type) {Pt : forall aa, IsTrunc n (P aa)}
+  : (forall a, P (tr a)) -> (forall aa, P aa)
+:= (fun f aa => match aa with tr a => fun _ => f a end Pt).
+Definition merely (A : Type@{i}) : hProp@{i} := BuildhProp (Trunc -1 A).
+Definition cconst_factors_contr `{Funext}  {X Y : Type} (f : X -> Y)
+           (P : Type) `{Pc : X -> Contr P}
+           (g : X -> P) (h : P -> Y) (p : h o g == f)
+: Unit.
+Proof.
+  assert (merely X -> IsHProp P) by admit.
+  refine (let g' := Trunc_ind (fun _ => P) g : merely X -> P in _);
+    [ assumption.. | ].
+  pose (g'' := Trunc_ind (fun _ => P) g : merely X -> P).
diff --git a/test-suite/bugs/closed/3938.v b/test-suite/bugs/closed/3938.v
new file mode 100644
index 00000000..859e9f01
--- /dev/null
+++ b/test-suite/bugs/closed/3938.v
@@ -0,0 +1,8 @@
+Require Import TestSuite.admit.
+Require Import Coq.Arith.PeanoNat.
+Hint Extern 1 => admit : typeclass_instances.
+Require Import Setoid.
+Goal forall a b (f : nat -> Set) (R : nat -> nat -> Prop), 
+       Equivalence R -> R a b -> f a = f b.
+  intros a b f H.
+  intros. Fail rewrite H1. 
diff --git a/test-suite/bugs/closed/3944.v b/test-suite/bugs/closed/3944.v
new file mode 100644
index 00000000..58e60f4f
--- /dev/null
+++ b/test-suite/bugs/closed/3944.v
@@ -0,0 +1,5 @@
+Require Import Setoid.
+Definition C (T : Type) := T.
+Goal forall T (i : C T) (v : T), True.
+Proof.
+Fail setoid_rewrite plus_n_Sm.
diff --git a/test-suite/bugs/closed/3953.v b/test-suite/bugs/closed/3953.v
new file mode 100644
index 00000000..167cecea
--- /dev/null
+++ b/test-suite/bugs/closed/3953.v
@@ -0,0 +1,5 @@
+(* Checking subst on instances of evars (was bugged in 8.5 beta 1) *)
+Goal forall (a b : unit), a = b -> exists c, b = c.
+  intros.
+  eexists.
+  subst.
diff --git a/test-suite/bugs/closed/3960.v b/test-suite/bugs/closed/3960.v
new file mode 100644
index 00000000..e56dcef7
--- /dev/null
+++ b/test-suite/bugs/closed/3960.v
@@ -0,0 +1,26 @@
+Require Program.Tactics.
+
+Axiom foo : nat -> Prop.
+
+Axiom fooP : forall n, foo n.
+
+Class myClass (A: Type) :=
+  {
+    bar : A -> Prop
+  }.
+
+Program Instance myInstance : myClass nat :=
+  {
+    bar := foo
+  }.
+
+Class myClassP (A : Type)  :=
+  {
+    super :> myClass A;
+    barP : forall (a : A), bar a
+  }.
+
+Instance myInstanceP : myClassP nat :=
+  {
+    barP := fooP
+  }.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3978.v b/test-suite/bugs/closed/3978.v
new file mode 100644
index 00000000..26e021e7
--- /dev/null
+++ b/test-suite/bugs/closed/3978.v
@@ -0,0 +1,27 @@
+Require Import Structures.OrderedType.  
+Require Import Structures.OrderedTypeEx.
+
+Module Type M. Parameter X : Type.      
+
+Declare Module Export XOrd : OrderedType
+  with Definition t := X
+  with Definition eq := @Logic.eq X.
+End M.
+
+Module M' : M.
+  Definition X := nat.
+
+  Module XOrd := Nat_as_OT.
+End M'.
+
+Module Type MyOt.
+  Parameter t : Type.
+  Parameter eq : t -> t -> Prop.
+End MyOt.
+
+Module Type M2. Parameter X : Type.      
+
+Declare Module Export XOrd : MyOt
+  with Definition t := X
+  with Definition eq := @Logic.eq X.
+End M2.
diff --git a/test-suite/bugs/closed/3993.v b/test-suite/bugs/closed/3993.v
new file mode 100644
index 00000000..086d8dd0
--- /dev/null
+++ b/test-suite/bugs/closed/3993.v
@@ -0,0 +1,3 @@
+(* Test smooth failure on not fully applied term to destruct with eqn: given *)
+Goal True.
+Fail induction S eqn:H.
diff --git a/test-suite/bugs/closed/4001.v b/test-suite/bugs/closed/4001.v
new file mode 100644
index 00000000..25d78f4b
--- /dev/null
+++ b/test-suite/bugs/closed/4001.v
@@ -0,0 +1,18 @@
+(* Computing the type constraints to be satisfied when building the
+   return clause of a match with a match *)
+
+Set Implicit Arguments.
+Set Asymmetric Patterns.
+  
+Variable A : Type.
+Variable typ : A -> Type.
+
+Inductive t : list A -> Type :=
+| snil  : t nil
+| scons : forall (x : A) (e : typ x) (lx : list A) (le : t  lx), t (x::lx).
+
+Definition car (x:A) (lx : list A) (s: t (x::lx)) : typ x :=
+  match s in t l'  with
+  | snil => False
+  | scons _ e _ _ => e
+  end.
diff --git a/test-suite/bugs/closed/4012.v b/test-suite/bugs/closed/4012.v
new file mode 100644
index 00000000..1748e3ba
--- /dev/null
+++ b/test-suite/bugs/closed/4012.v
@@ -0,0 +1,5 @@
+Goal (forall T : Type, T = T) -> Type.
+Proof.
+  intro H.
+  Fail specialize (H _).
+Abort.
diff --git a/test-suite/bugs/closed/4016.v b/test-suite/bugs/closed/4016.v
new file mode 100644
index 00000000..41cb1a88
--- /dev/null
+++ b/test-suite/bugs/closed/4016.v
@@ -0,0 +1,12 @@
+Require Import Setoid.
+
+Parameter eq : relation nat.
+Declare Instance Equivalence_eq : Equivalence eq.
+
+Lemma foo : forall z, eq z 0 -> forall x, eq x 0 -> eq z x.
+Proof.
+intros z Hz x Hx.
+rewrite <- Hx in Hz.
+destruct z.
+Abort.
+
diff --git a/test-suite/bugs/closed/4017.v b/test-suite/bugs/closed/4017.v
new file mode 100644
index 00000000..aa810f4f
--- /dev/null
+++ b/test-suite/bugs/closed/4017.v
@@ -0,0 +1,8 @@
+Set Implicit Arguments.
+
+(* Use of implicit arguments was lost in multiple variable declarations *)
+Variables 
+  (A1 : Type)
+  (A2 : forall (x1 : A1), Type) 
+  (A3 : forall (x1 : A1) (x2 : A2 x1), Type)
+  (A4 : forall (x1 : A1) (x2 : A2 x1) (x3 : A3 x2), Type).
diff --git a/test-suite/bugs/closed/4018.v b/test-suite/bugs/closed/4018.v
new file mode 100644
index 00000000..8895e09e
--- /dev/null
+++ b/test-suite/bugs/closed/4018.v
@@ -0,0 +1,3 @@
+(* Catching PatternMatchingFailure was lost at some point *)
+Goal nat -> True.
+Fail intros [=].
diff --git a/test-suite/bugs/closed/4031.v b/test-suite/bugs/closed/4031.v
new file mode 100644
index 00000000..2b8641eb
--- /dev/null
+++ b/test-suite/bugs/closed/4031.v
@@ -0,0 +1,14 @@
+Definition something (P:Type) (e:P) := e.
+
+Inductive myunit : Set := mytt.
+  (* Proof below works when definition is in Type,
+     however builtin types such as unit are in Set. *)
+
+Lemma demo_hide_generic : 
+   let x := mytt in x = x.
+Proof.
+  intros.
+  change mytt with (@something _ mytt) in x.
+  subst x. (* Proof works if this line is removed *)
+  reflexivity.
+Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4035.v b/test-suite/bugs/closed/4035.v
new file mode 100644
index 00000000..ec246d09
--- /dev/null
+++ b/test-suite/bugs/closed/4035.v
@@ -0,0 +1,13 @@
+(* Supporting tactic notations within Ltac in the presence of an
+  "ident" entry which does not expect a fresh ident *)
+(* Of course, this is a matter of convention of what "ident" is
+   supposed to denote, but in practice, it seems more convenient to
+   have less constraints on ident at interpretation time, as
+   otherwise more ad hoc entries would be necessary (as e.g. a special
+   "quantified_hypothesis" entry for dependent destruction). *)
+Require Import Program.
+Goal nat -> Type.
+  intro x.
+  lazymatch goal with
+  | [ x : nat |- _ ] => dependent destruction x
+  end.
diff --git a/test-suite/bugs/closed/4046.v b/test-suite/bugs/closed/4046.v
new file mode 100644
index 00000000..8f8779b7
--- /dev/null
+++ b/test-suite/bugs/closed/4046.v
@@ -0,0 +1,6 @@
+Module Import Foo.
+  Class Foo := { foo : Type }.
+End Foo.
+
+Instance f : Foo := { foo := nat }. (* works fine *)
+Instance f' : Foo.Foo := { Foo.foo := nat }. 
diff --git a/test-suite/bugs/closed/4078.v b/test-suite/bugs/closed/4078.v
new file mode 100644
index 00000000..236cd2fb
--- /dev/null
+++ b/test-suite/bugs/closed/4078.v
@@ -0,0 +1,14 @@
+Module Type S.
+
+Axiom foo : nat.
+
+End S.
+
+Module M : S.
+
+Definition bar := 0.
+Definition foo := bar.
+
+End M.
+
+Print All Dependencies M.foo.
diff --git a/test-suite/bugs/closed/4089.v b/test-suite/bugs/closed/4089.v
new file mode 100644
index 00000000..1449f242
--- /dev/null
+++ b/test-suite/bugs/closed/4089.v
@@ -0,0 +1,374 @@
+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
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (ebfc19d792492417b129063fb511aa423e9d9e08) *)
+Open Scope type_scope.
+
+Global Set Universe Polymorphism.
+Module Export Datatypes.
+
+Set Implicit Arguments.
+
+Record prod (A B : Type) := pair { fst : A ; snd : B }.
+
+Notation "x * y" := (prod x y) : type_scope.
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
+
+End Datatypes.
+Module Export Specif.
+
+Set Implicit Arguments.
+
+Record sig {A} (P : A -> Type) := exist { proj1_sig : A ; proj2_sig : P proj1_sig }.
+
+Notation sigT := sig (only parsing).
+Notation existT := exist (only parsing).
+
+Notation "{ x : A  & P }" := (sigT (fun x:A => P)) : type_scope.
+
+Notation projT1 := proj1_sig (only parsing).
+Notation projT2 := proj2_sig (only parsing).
+
+End Specif.
+
+Ltac rapply p :=
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _) ||
+  refine (p _ _ _ _) ||
+  refine (p _ _ _) ||
+  refine (p _ _) ||
+  refine (p _) ||
+  refine p.
+
+Local Unset Elimination Schemes.
+
+Definition relation (A : Type) := A -> A -> Type.
+
+Class Symmetric {A} (R : relation A) :=
+  symmetry : forall x y, R x y -> R y x.
+
+Class Transitive {A} (R : relation A) :=
+  transitivity : forall x y z, R x y -> R y z -> R x z.
+
+Tactic Notation "etransitivity" open_constr(y) :=
+  let R := match goal with |- ?R ?x ?z => constr:(R) end in
+  let x := match goal with |- ?R ?x ?z => constr:(x) end in
+  let z := match goal with |- ?R ?x ?z => constr:(z) end in
+  let pre_proof_term_head := constr:(@transitivity _ R _) in
+  let proof_term_head := (eval cbn in pre_proof_term_head) in
+  refine (proof_term_head x y z _ _); [ change (R x y) | change (R y z) ].
+
+Ltac transitivity x := etransitivity x.
+
+Definition Type1 := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}.
+
+Notation idmap := (fun x => x).
+Delimit Scope function_scope with function.
+Delimit Scope path_scope with path.
+Delimit Scope fibration_scope with fibration.
+Open Scope fibration_scope.
+Open Scope function_scope.
+
+Notation "( x ; y )" := (existT _ x y) : fibration_scope.
+
+Notation pr1 := projT1.
+Notation pr2 := projT2.
+
+Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
+Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
+
+Notation compose := (fun g f x => g (f x)).
+
+Notation "g 'o' f" := (compose g%function f%function) (at level 40, left associativity) : function_scope.
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Arguments idpath {A a} , [A] a.
+
+Scheme paths_ind := Induction for paths Sort Type.
+
+Definition paths_rect := paths_ind.
+
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+
+Local Open Scope path_scope.
+
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
+  := match p with idpath => idpath end.
+
+Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
+  match p, q with idpath, idpath => idpath end.
+
+Arguments concat {A x y z} p q : simpl nomatch.
+
+Notation "1" := idpath : path_scope.
+
+Notation "p @ q" := (concat p%path q%path) (at level 20) : path_scope.
+
+Notation "p ^" := (inverse p%path) (at level 3, format "p '^'") : path_scope.
+
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
+  match p with idpath => u end.
+
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+
+Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x)
+  := forall x:A, f x = g x.
+
+Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope.
+
+Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g)
+  : f == g
+  := fun x => match h with idpath => 1 end.
+
+Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
+  forall x : A, r (s x) = x.
+
+Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
+  equiv_inv : B -> A ;
+  eisretr : Sect equiv_inv f;
+  eissect : Sect f equiv_inv;
+  eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
+}.
+
+Arguments eisretr {A B}%type_scope f%function_scope {_} _.
+Arguments eissect {A B}%type_scope f%function_scope {_} _.
+Arguments eisadj {A B}%type_scope f%function_scope {_} _.
+
+Record Equiv A B := BuildEquiv {
+  equiv_fun : A -> B ;
+  equiv_isequiv : IsEquiv equiv_fun
+}.
+
+Coercion equiv_fun : Equiv >-> Funclass.
+
+Global Existing Instance equiv_isequiv.
+
+Bind Scope equiv_scope with Equiv.
+
+Notation "A <~> B" := (Equiv A B) (at level 85) : type_scope.
+
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : function_scope.
+
+Inductive Unit : Type1 :=
+    tt : Unit.
+
+Ltac done :=
+  trivial; intros; solve
+    [ repeat first
+      [ solve [trivial]
+      | solve [symmetry; trivial]
+      | reflexivity
+
+      | contradiction
+      | split ]
+    | match goal with
+      H : ~ _ |- _ => solve [destruct H; trivial]
+      end ].
+Tactic Notation "by" tactic(tac) :=
+  tac; done.
+
+Definition concat_p1 {A : Type} {x y : A} (p : x = y) :
+  p @ 1 = p
+  :=
+  match p with idpath => 1 end.
+
+Definition concat_1p {A : Type} {x y : A} (p : x = y) :
+  1 @ p = p
+  :=
+  match p with idpath => 1 end.
+
+Definition ap_pp {A B : Type} (f : A -> B) {x y z : A} (p : x = y) (q : y = z) :
+  ap f (p @ q) = (ap f p) @ (ap f q)
+  :=
+  match q with
+    idpath =>
+    match p with idpath => 1 end
+  end.
+
+Definition ap_compose {A B C : Type} (f : A -> B) (g : B -> C) {x y : A} (p : x = y) :
+  ap (g o f) p = ap g (ap f p)
+  :=
+  match p with idpath => 1 end.
+
+Definition concat_A1p {A : Type} {f : A -> A} (p : forall x, f x = x) {x y : A} (q : x = y) :
+  (ap f q) @ (p y) = (p x) @ q
+  :=
+  match q with
+    | idpath => concat_1p _ @ ((concat_p1 _) ^)
+  end.
+
+Definition concat2 {A} {x y z : A} {p p' : x = y} {q q' : y = z} (h : p = p') (h' : q = q')
+  : p @ q = p' @ q'
+:= match h, h' with idpath, idpath => 1 end.
+
+Notation "p @@ q" := (concat2 p q)%path (at level 20) : path_scope.
+
+Definition whiskerL {A : Type} {x y z : A} (p : x = y)
+  {q r : y = z} (h : q = r) : p @ q = p @ r
+:= 1 @@ h.
+
+Definition ap02 {A B : Type} (f:A->B) {x y:A} {p q:x=y} (r:p=q) : ap f p = ap f q
+  := match r with idpath => 1 end.
+Module Export Equivalences.
+
+Generalizable Variables A B C f g.
+
+Global Instance isequiv_idmap (A : Type) : IsEquiv idmap | 0 :=
+  BuildIsEquiv A A idmap idmap (fun _ => 1) (fun _ => 1) (fun _ => 1).
+
+Definition equiv_idmap (A : Type) : A <~> A := BuildEquiv A A idmap _.
+
+Arguments equiv_idmap {A} , A.
+
+Notation "1" := equiv_idmap : equiv_scope.
+
+Global Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g}
+  : IsEquiv (compose g f) | 1000
+  := BuildIsEquiv A C (compose g f)
+    (compose f^-1 g^-1)
+    (fun c => ap g (eisretr f (g^-1 c)) @ eisretr g c)
+    (fun a => ap (f^-1) (eissect g (f a)) @ eissect f a)
+    (fun a =>
+      (whiskerL _ (eisadj g (f a))) @
+      (ap_pp g _ _)^ @
+      ap02 g
+      ( (concat_A1p (eisretr f) (eissect g (f a)))^ @
+        (ap_compose f^-1 f _ @@ eisadj f a) @
+        (ap_pp f _ _)^
+      ) @
+      (ap_compose f g _)^
+    ).
+
+Definition equiv_compose {A B C : Type} (g : B -> C) (f : A -> B)
+  `{IsEquiv B C g} `{IsEquiv A B f}
+  : A <~> C
+  := BuildEquiv A C (compose g f) _.
+
+Global Instance transitive_equiv : Transitive Equiv | 0 :=
+  fun _ _ _ f g => equiv_compose g f.
+
+Theorem equiv_inverse {A B : Type} : (A <~> B) -> (B <~> A).
+admit.
+Defined.
+
+Global Instance symmetric_equiv : Symmetric Equiv | 0 := @equiv_inverse.
+
+End Equivalences.
+
+Definition path_prod_uncurried {A B : Type} (z z' : A * B)
+  (pq : (fst z = fst z') * (snd z = snd z'))
+  : (z = z').
+admit.
+Defined.
+
+Global Instance isequiv_path_prod {A B : Type} {z z' : A * B}
+: IsEquiv (path_prod_uncurried z z') | 0.
+admit.
+Defined.
+
+Definition equiv_path_prod {A B : Type} (z z' : A * B)
+  : (fst z = fst z') * (snd z = snd z')  <~>  (z = z')
+  := BuildEquiv _ _ (path_prod_uncurried z z') _.
+
+Generalizable Variables X A B C f g n.
+
+Definition functor_sigma `{P : A -> Type} `{Q : B -> Type}
+           (f : A -> B) (g : forall a, P a -> Q (f a))
+: sigT P -> sigT Q
+  := fun u => (f u.1 ; g u.1 u.2).
+
+Global Instance isequiv_functor_sigma `{P : A -> Type} `{Q : B -> Type}
+         `{IsEquiv A B f} `{forall a, @IsEquiv (P a) (Q (f a)) (g a)}
+: IsEquiv (functor_sigma f g) | 1000.
+admit.
+Defined.
+
+Definition equiv_functor_sigma `{P : A -> Type} `{Q : B -> Type}
+           (f : A -> B) `{IsEquiv A B f}
+           (g : forall a, P a -> Q (f a))
+           `{forall a, @IsEquiv (P a) (Q (f a)) (g a)}
+: sigT P <~> sigT Q
+  := BuildEquiv _ _ (functor_sigma f g) _.
+
+Definition equiv_functor_sigma' `{P : A -> Type} `{Q : B -> Type}
+           (f : A <~> B)
+           (g : forall a, P a <~> Q (f a))
+: sigT P <~> sigT Q
+  := equiv_functor_sigma f g.
+
+Definition equiv_functor_sigma_id `{P : A -> Type} `{Q : A -> Type}
+           (g : forall a, P a <~> Q a)
+: sigT P <~> sigT Q
+  := equiv_functor_sigma' 1 g.
+
+Definition Bip : Type := { C : Type &  C * C }.
+
+Definition BipMor (X Y : Bip) : Type :=
+  match X, Y with (C;(c0,c1)), (D;(d0,d1)) =>
+    { f : C -> D & (f c0 = d0) * (f c1 = d1) }
+  end.
+
+Definition bipmor2map {X Y : Bip} : BipMor X Y -> X.1 -> Y.1 :=
+  match X, Y with (C;(c0,c1)), (D;(d0,d1)) => fun i =>
+    match i with (f;_) => f end
+  end.
+
+Definition bipidmor {X : Bip} : BipMor X X :=
+  match X with (C;(c0,c1)) => (idmap; (1, 1)) end.
+
+Definition bipcompmor {X Y Z : Bip} : BipMor X Y -> BipMor Y Z -> BipMor X Z :=
+  match X, Y, Z with (C;(c0,c1)), (D;(d0,d1)), (E;(e0,e1)) => fun i j =>
+    match i, j with (f;(f0,f1)), (g;(g0,g1)) =>
+      (g o f; (ap g f0 @ g0, ap g f1 @ g1))
+    end
+  end.
+
+Definition isbipequiv {X Y : Bip} (i : BipMor X Y) : Type :=
+  { l : BipMor Y X & bipcompmor i l = bipidmor } *
+  { r : BipMor Y X & bipcompmor r i = bipidmor }.
+
+Lemma bipequivEQequiv : forall {X Y : Bip} (i : BipMor X Y),
+  isbipequiv i <~> IsEquiv (bipmor2map i).
+Proof.
+assert (equivcompmor : forall {X Y : Bip} (i : BipMor X Y) j,
+(bipcompmor i j = bipidmor) <~> Unit).
+  intros; set (U := X); set (V := Y); destruct X as [C [c0 c1]], Y as [D [d0 d1]].
+  transitivity { n : (bipcompmor i j).1 = (@bipidmor U).1 &
+  (bipcompmor i j).2 = transport (fun h => (h c0 = c0) * (h c1 = c1)) n^ (@bipidmor U).2}.
+    admit.
+  destruct i as [f [f0 f1]]; destruct j as [g [g0 g1]].
+
+  transitivity { n : g o f = idmap & (ap g f0 @ g0 = apD10 n c0 @ 1) *
+  (ap g f1 @ g1 = apD10 n c1 @ 1)}.
+    apply equiv_functor_sigma_id; intro n.
+    assert (Ggen : forall (h0 h1 : C -> C) (p : h0 = h1) u0 u1 v0 v1,
+    ((u0, u1) = transport (fun h => (h c0 = c0) * (h c1 = c1)) p^ (v0, v1)) <~>
+    (u0 = apD10 p c0 @ v0) * (u1 = apD10 p c1 @ v1)).
+      induction p; intros; simpl; rewrite !concat_1p; apply symmetry.
+      by apply (equiv_path_prod (u0,u1) (v0,v1)).
+    rapply Ggen.
+    pose (@paths C).
+    Check (@paths C).
+    Undo.
+    Check (@paths C). (* Toplevel input, characters 0-17:
+Error: Illegal application:
+The term "@paths" of type "forall A : Type, A -> A -> Type"
+cannot be applied to the term
+ "C" : "Type"
+This term has type "Type@{Top.892}" which should be coercible to
+ "Type@{Top.882}".
+*)
diff --git a/test-suite/bugs/closed/4097.v b/test-suite/bugs/closed/4097.v
new file mode 100644
index 00000000..02aa25e0
--- /dev/null
+++ b/test-suite/bugs/closed/4097.v
@@ -0,0 +1,65 @@
+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) *)
+Global Set Primitive Projections.
+Record sigT {A} (P : A -> Type) := exist { projT1 : A ; projT2 : P projT1 }.
+Arguments projT1 {A P} _ / .
+Arguments projT2 {A P} _ / .
+Notation "{ x : A  & P }" := (sigT (fun x:A => P)) : type_scope.
+Delimit Scope path_scope with path.
+Delimit Scope fibration_scope with fibration.
+Open Scope path_scope.
+Open Scope fibration_scope.
+Notation "( x ; y )" := (exist _ _ x y) : fibration_scope.
+Notation pr1 := projT1.
+Notation pr2 := projT2.
+Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
+Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
+  := match p with idpath => idpath end.
+Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
+  match p, q with idpath, idpath => idpath end.
+Notation "p @ q" := (concat p%path q%path) (at level 20) : path_scope.
+Notation "p ^" := (inverse p%path) (at level 3, format "p '^'") : path_scope.
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
+  match p with idpath => u end.
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing) : path_scope.
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+Definition apD {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y):
+  p # (f x) = f y
+  :=
+  match p with idpath => idpath end.
+Lemma transport_compose {A B} {x y : A} (P : B -> Type) (f : A -> B)
+  (p : x = y) (z : P (f x))
+  : transport (fun x => P (f x)) p z  =  transport P (ap f p) z.
+admit.
+Defined.
+Generalizable Variables X A B C f g n.
+Definition pr1_path `{P : A -> Type} {u v : sigT P} (p : u = v)
+: u.1 = v.1
+  := ap pr1 p.
+Notation "p ..1" := (pr1_path p) (at level 3) : fibration_scope.
+Definition pr2_path `{P : A -> Type} {u v : sigT P} (p : u = v)
+: p..1 # u.2 = v.2
+  := (transport_compose P pr1 p u.2)^
+     @ (@apD {x:A & P x} _ pr2 _ _ p).
+Notation "p ..2" := (pr2_path p) (at level 3) : fibration_scope.
+Definition path_path_sigma_uncurried {A : Type} (P : A -> Type) (u v : sigT P)
+           (p q : u = v)
+           (rs : {r : p..1 = q..1 & transport (fun x => transport P x u.2 = v.2) r p..2 = q..2})
+: p = q.
+admit.
+Defined.
+Set Debug Unification.
+Definition path_path_sigma {A : Type} (P : A -> Type) (u v : sigT P)
+           (p q : u = v)
+           (r : p..1 = q..1)
+           (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2)
+: p = q
+  := path_path_sigma_uncurried P u v p q (r; s).
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4101.v b/test-suite/bugs/closed/4101.v
new file mode 100644
index 00000000..a38b0509
--- /dev/null
+++ b/test-suite/bugs/closed/4101.v
@@ -0,0 +1,19 @@
+(* File reduced by coq-bug-finder from original input, then from 10940 lines to 152 lines, then from 509 lines to 163 lines, then from 178 lines to 66 lines *)
+(* coqc version 8.5beta1 (March 2015) compiled on Mar 2 2015 18:53:10 with OCaml 4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (e77f178e60918f14eacd1ec0364a491d4cfd0f3f) *)
+
+Global Set Primitive Projections.
+Set Implicit Arguments.
+Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
+Axiom path_forall : forall {A : Type} {P : A -> Type} (f g : forall x : A, P x),
+                      (forall x, f x = g x) -> f = g.
+Lemma sigT_obj_eq
+: forall (T : Type) (T0 : T -> Type)
+         (s s0 : forall s : sigT T0,
+                   sigT (fun _ : T0 (projT1 s) => unit) ->
+                   sigT (fun _ : T0 (projT1 s) => unit)),
+   s0 = s.
+Proof.
+  intros.
+  Set Debug Tactic Unification.
+  apply path_forall. 
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4103.v b/test-suite/bugs/closed/4103.v
new file mode 100644
index 00000000..92cc0279
--- /dev/null
+++ b/test-suite/bugs/closed/4103.v
@@ -0,0 +1,12 @@
+Set Primitive Projections.
+
+CoInductive stream A := { hd : A; tl : stream A }.
+
+CoFixpoint ticks (n : nat) : stream unit := {| hd := tt; tl := ticks n |}.
+
+Lemma expand : exists n : nat, (ticks n) = (ticks n).(tl _).
+Proof.
+  eexists.
+  (* Set Debug Tactic Unification. *)
+  (* Set Debug RAKAM. *)
+  reflexivity.
diff --git a/test-suite/bugs/closed/4120.v b/test-suite/bugs/closed/4120.v
new file mode 100644
index 00000000..00db8f7f
--- /dev/null
+++ b/test-suite/bugs/closed/4120.v
@@ -0,0 +1,5 @@
+Definition id {T} (x : T) := x.
+Goal sigT (fun x => id x)%type.
+  change (fun x => ?f x) with f.
+  exists Type. exact Set.
+Defined. (* Error: Attempt to save a proof with shelved goals (in proof Unnamed_thm) *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4121.v b/test-suite/bugs/closed/4121.v
new file mode 100644
index 00000000..5f8c411c
--- /dev/null
+++ b/test-suite/bugs/closed/4121.v
@@ -0,0 +1,15 @@
+(* -*- coq-prog-args: ("-emacs" "-nois") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 830 lines to 47 lines, then from 25 lines to 11 lines *)
+(* coqc version 8.5beta1 (March 2015) compiled on Mar 11 2015 18:51:36 with OCaml 4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (8dbfee5c5f897af8186cb1bdfb04fd4f88eca677) *)
+
+Set Universe Polymorphism.
+Class Contr_internal (A : Type) := BuildContr { center : A }.
+Arguments center A {_}.
+Class Contr (A : Type) : Type := Contr_is_trunc : Contr_internal A.
+Hint Extern 0 => progress change Contr_internal with Contr in * : typeclass_instances.
+Definition contr_paths_contr0 {A} `{Contr A} : Contr A := {| center := center A |}.
+Instance contr_paths_contr1 {A} `{Contr A} : Contr A := {| center := center A |}.
+Check @contr_paths_contr0@{i}.
+Check @contr_paths_contr1@{i}. (* Error: Universe instance should have length 2 *)
+(** It should have length 1, just like contr_paths_contr0 *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4165.v b/test-suite/bugs/closed/4165.v
new file mode 100644
index 00000000..8e0a62d3
--- /dev/null
+++ b/test-suite/bugs/closed/4165.v
@@ -0,0 +1,7 @@
+Lemma foo : True.
+Proof.
+pose (fun x : nat => (let H:=true in x)) as s.
+match eval cbv delta [s] in s with
+| context C[true] =>
+  let C':=context C[false] in pose C' as s'
+end.
diff --git a/test-suite/bugs/closed/4190.v b/test-suite/bugs/closed/4190.v
new file mode 100644
index 00000000..2843488b
--- /dev/null
+++ b/test-suite/bugs/closed/4190.v
@@ -0,0 +1,15 @@
+Module Type A .
+ Tactic Notation "bar" := idtac "ITSME".
+End A.
+
+Module Type B.
+ Tactic Notation "foo" := fail "NOTME".
+End B.
+
+Module Type C := A <+ B.
+
+Module Type F (Import M : C).
+
+Lemma foo : True.
+Proof.
+bar.
diff --git a/test-suite/bugs/closed/4193.v b/test-suite/bugs/closed/4193.v
new file mode 100644
index 00000000..885d04a9
--- /dev/null
+++ b/test-suite/bugs/closed/4193.v
@@ -0,0 +1,7 @@
+Module Type E.
+End E.
+
+Module Type A (M : E).
+End A.
+
+Fail Module Type F (Import X : A).
diff --git a/test-suite/bugs/closed/HoTT_coq_007.v b/test-suite/bugs/closed/HoTT_coq_007.v
index 8592c729..0b8bb235 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 63548a64..ae3e50d7 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.
@@ -121,6 +122,7 @@ Section GraphObj.
 
   Definition GraphIndex_Compose s d d' (m1 : GraphIndex_Morphism d d') (m2 : GraphIndex_Morphism s d) :
     GraphIndex_Morphism s d'.
+  Proof using.  (* This makes no sense, but it makes this test behave as before the no admit commit *)
   Admitted.
 
    Definition GraphIndexingCategory : @SpecializedCategory GraphIndex.
diff --git a/test-suite/bugs/closed/HoTT_coq_020.v b/test-suite/bugs/closed/HoTT_coq_020.v
index b16c1df2..4938b80f 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 4fd54b56..161c4d21 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 fa5ee25c..9f892483 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 4ad2fc02..133bf6c7 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 6b206a2f..432cf705 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 92d70ad1..a2509877 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 6e65320d..3e3a987a 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 9ce7dba9..5e5d5ab3 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 26c1f963..19551dc9 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 db895316..b7db22a6 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 5f0a541b..b4c74537 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 ad32a60c..84a5bc02 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 b3e1df57..0428af0d 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 5c704147..5fa16703 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 fc99daab..bdcd8ba9 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 9b6ace82..cd5b0c8f 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 c39b7093..663b6280 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 9c89a6ab..3ef56892 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 71becfd2..996aaaa4 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 c3a83627..7c1ab8dc 100644
--- a/test-suite/bugs/closed/HoTT_coq_107.v
+++ b/test-suite/bugs/closed/HoTT_coq_107.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-nois" "-emacs") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-R" "../theories" "Coq") -*- *)
 (* File reduced by coq-bug-finder from 4897 lines to 2605 lines, then from 2297 lines to 236 lines, then from 239 lines to 137 lines, then from 118 lines to 67 lines, then from 520 lines to 76 lines. *)
 (** Note: The bug here is the same as the #113, that is, HoTT_coq_113.v *)
 Require Import Coq.Init.Logic.
@@ -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 cc304802..4f5ef997 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 150f2ecc..5bee69fc 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 3ef531bc..05e76784 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 14ad0e49..e41689cb 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 cce288cf..90493a53 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 994dff63..6ee6e653 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/closed/2456.v b/test-suite/bugs/opened/2456.v
index 56f046c4..6cca5c9f 100644
--- a/test-suite/bugs/closed/2456.v
+++ b/test-suite/bugs/opened/2456.v
@@ -46,8 +46,8 @@ Lemma CatchCommuteUnique2 :
 Proof with auto.
 intros.
 set (X := commute2).
-dependent destruction commute1;
+Fail dependent destruction commute1;
 dependent destruction catchCommuteDetails;
 dependent destruction commute2;
 dependent destruction catchCommuteDetails generalizing X.
-Admitted.
\ No newline at end of file
+Admitted.
diff --git a/test-suite/bugs/opened/2951.v b/test-suite/bugs/opened/2951.v
deleted file mode 100644
index 3739247b..00000000
--- a/test-suite/bugs/opened/2951.v
+++ /dev/null
@@ -1 +0,0 @@
-Class C (A: Type) : Type := { f: A }.
diff --git a/test-suite/bugs/opened/3263.v b/test-suite/bugs/opened/3263.v
index 6de13f74..f0c707bd 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 b61174a8..3e3da6df 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 ff0dbf97..5ca48fc9 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/3491.v b/test-suite/bugs/opened/3491.v
deleted file mode 100644
index 9837b0ec..00000000
--- a/test-suite/bugs/opened/3491.v
+++ /dev/null
@@ -1,2 +0,0 @@
-Fail Inductive list (A : Type) (T := A) : Type :=
-    nil : list A | cons : T -> list T -> list A.
diff --git a/test-suite/bugs/opened/3509.v b/test-suite/bugs/opened/3509.v
index 02e47a8b..3913bbb4 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 25285636..daf26507 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/closed/3593.v b/test-suite/bugs/opened/3593.v
index 25f9db6b..d83b9006 100644
--- a/test-suite/bugs/closed/3593.v
+++ b/test-suite/bugs/opened/3593.v
@@ -5,6 +5,6 @@ Record prod A B := pair { fst : A ; snd : B }.
 Goal forall x : prod Set Set, let f := @fst _ in f _ x = @fst _ _ x.
 simpl; intros.
   constr_eq (@fst Set Set x) (fst (A := Set) (B := Set) x).   
-  Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x). 
+  Fail Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x).
   reflexivity.
 Qed.
diff --git a/test-suite/bugs/opened/3685.v b/test-suite/bugs/opened/3685.v
index d647b5a8..b2b5db6b 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 c7441882..9b3f94d9 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/3794.v b/test-suite/bugs/opened/3794.v
new file mode 100644
index 00000000..99ca6cb3
--- /dev/null
+++ b/test-suite/bugs/opened/3794.v
@@ -0,0 +1,7 @@
+Hint Extern 10 ((?X = ?Y) -> False) => intros; discriminate.
+Hint Unfold not : core.
+
+Goal true<>false.
+Set Typeclasses Debug.
+Fail typeclasses eauto with core.
+Abort.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3848.v b/test-suite/bugs/opened/3848.v
index b66aecca..a03e8ffd 100644
--- a/test-suite/bugs/closed/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.
@@ -18,4 +19,4 @@ Proof.
   refine (functor_forall
             (f^-1)
             (fun (x:A) (y:Q (f^-1 x)) => eisretr f x # (g (f^-1 x))^-1 y)).
-Defined. (* Error: Attempt to save an incomplete proof *)
+Fail Defined. (* Error: Attempt to save an incomplete proof *)
diff --git a/test-suite/bugs/opened/HoTT_coq_120.v b/test-suite/bugs/opened/HoTT_coq_120.v
index 7847c5e4..05ee6c7b 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/complexity/bug4076.v b/test-suite/complexity/bug4076.v
new file mode 100644
index 00000000..3cf9e8b0
--- /dev/null
+++ b/test-suite/complexity/bug4076.v
@@ -0,0 +1,29 @@
+(* Check behavior of evar-evar subtyping problems in the presence of
+   nested let-ins *)
+(* Expected time < 2.00s *)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Parameter f : forall P, forall (i : nat), P i -> P i.
+Parameter P : nat -> Type.
+
+Time Definition g (n : nat) (a0 : P n) : P n :=
+  let a1  := f a0 in
+  let a2  := f a1 in
+  let a3  := f a2 in
+  let a4  := f a3 in
+  let a5  := f a4 in
+  let a6  := f a5 in
+  let a7  := f a6 in
+  let a8  := f a7 in
+  let a9  := f a8 in
+  let a10 := f a9 in 
+  let a11 := f a10 in
+  let a12 := f a11 in
+  let a13 := f a12 in
+  let a14 := f a13 in
+  let a15 := f a14 in
+  let a16 := f a15 in
+  let a17 := f a16 in
+  a17.
diff --git a/test-suite/complexity/bug4076bis.v b/test-suite/complexity/bug4076bis.v
new file mode 100644
index 00000000..f3996e6a
--- /dev/null
+++ b/test-suite/complexity/bug4076bis.v
@@ -0,0 +1,31 @@
+(* Another check of evar-evar subtyping problems in the presence of
+   nested let-ins *)
+(* Expected time < 2.00s *)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Parameter f : forall P, forall (i j : nat), P i j -> P i j.
+Parameter P : nat -> nat -> Type.
+
+Time Definition g (n : nat) (a0 : P n n) : P n n :=
+  let a1  := f a0 in
+  let a2  := f a1 in
+  let a3  := f a2 in
+  let a4  := f a3 in
+  let a5  := f a4 in
+  let a6  := f a5 in
+  let a7  := f a6 in
+  let a8  := f a7 in
+  let a9  := f a8 in
+  let a10 := f a9 in 
+  let a11 := f a10 in
+  let a12 := f a11 in
+  let a13 := f a12 in
+  let a14 := f a13 in
+  let a15 := f a14 in
+  let a16 := f a15 in
+  let a17 := f a16 in
+  let a18 := f a17 in
+  let a19 := f a18 in
+  a19.
diff --git a/test-suite/ide/undo020.fake b/test-suite/ide/undo020.fake
index 2adde908..aa1d9bb2 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/output/Arguments.out b/test-suite/output/Arguments.out
index 629a1ab6..2c7b04c6 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -1,13 +1,11 @@
 Nat.sub : nat -> nat -> nat
 
-Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold Nat.sub but avoid exposing match constructs
 Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
-Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold Nat.sub when applied to 1 argument
   but avoid exposing match constructs
@@ -15,7 +13,6 @@ Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
-Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold Nat.sub
   when the 1st argument evaluates to a constructor and
@@ -24,7 +21,6 @@ Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
-Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold Nat.sub when the 1st and
   2nd arguments evaluate to a constructor and when applied to 2 arguments 
@@ -32,7 +28,6 @@ Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
-Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold Nat.sub when the 1st and
   2nd arguments evaluate to a constructor 
@@ -42,7 +37,6 @@ pf :
 forall D1 C1 : Type,
 (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2
 
-pf is not universe polymorphic
 Arguments D2, C2 are implicit
 Arguments D1, C1 are implicit and maximally inserted
 Argument scopes are [foo_scope type_scope _ _ _ _ _]
@@ -51,7 +45,6 @@ pf is transparent
 Expands to: Constant Top.pf
 fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C
 
-fcomp is not universe polymorphic
 Arguments A, B, C are implicit and maximally inserted
 Argument scopes are [type_scope type_scope type_scope _ _ _]
 The reduction tactics unfold fcomp when applied to 6 arguments 
@@ -59,20 +52,17 @@ fcomp is transparent
 Expands to: Constant Top.fcomp
 volatile : nat -> nat
 
-volatile is not universe polymorphic
 Argument scope is [nat_scope]
 The reduction tactics always unfold volatile
 volatile is transparent
 Expands to: Constant Top.volatile
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
-f is not universe polymorphic
 Argument scopes are [_ _ nat_scope _ nat_scope]
 f is transparent
 Expands to: Constant Top.S1.S2.f
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
-f is not universe polymorphic
 Argument scopes are [_ _ nat_scope _ nat_scope]
 The reduction tactics unfold f when the 3rd, 4th and
   5th arguments evaluate to a constructor 
@@ -80,7 +70,6 @@ f is transparent
 Expands to: Constant Top.S1.S2.f
 f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
-f is not universe polymorphic
 Argument T2 is implicit
 Argument scopes are [type_scope _ _ nat_scope _ nat_scope]
 The reduction tactics unfold f when the 4th, 5th and
@@ -89,7 +78,6 @@ f is transparent
 Expands to: Constant Top.S1.f
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
-f is not universe polymorphic
 Arguments T1, T2 are implicit
 Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope]
 The reduction tactics unfold f when the 5th, 6th and
@@ -102,7 +90,6 @@ Expands to: Constant Top.f
      : Prop
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
-f is not universe polymorphic
 The reduction tactics unfold f when the 5th, 6th and
   7th arguments evaluate to a constructor 
 f is transparent
@@ -110,8 +97,8 @@ Expands to: Constant Top.f
 forall w : r, w 3 true = tt
      : Prop
 The command has indeed failed with message:
-=> Error: Unknown interpretation for notation "$".
+Error: Unknown interpretation for notation "$".
 w 3 true = tt
      : Prop
 The command has indeed failed with message:
-=> Error: Extra argument _.
+Error: Extra argument _.
diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out
index 71d5fc78..6643c142 100644
--- a/test-suite/output/ArgumentsScope.out
+++ b/test-suite/output/ArgumentsScope.out
@@ -1,70 +1,56 @@
 a : bool -> bool
 
-a is not universe polymorphic
 Argument scope is [bool_scope]
 Expands to: Variable a
 b : bool -> bool
 
-b is not universe polymorphic
 Argument scope is [bool_scope]
 Expands to: Variable b
 negb'' : bool -> bool
 
-negb'' is not universe polymorphic
 Argument scope is [bool_scope]
 negb'' is transparent
 Expands to: Constant Top.A.B.negb''
 negb' : bool -> bool
 
-negb' is not universe polymorphic
 Argument scope is [bool_scope]
 negb' is transparent
 Expands to: Constant Top.A.negb'
 negb : bool -> bool
 
-negb is not universe polymorphic
 Argument scope is [bool_scope]
 negb is transparent
 Expands to: Constant Coq.Init.Datatypes.negb
 a : bool -> bool
 
-a is not universe polymorphic
 Expands to: Variable a
 b : bool -> bool
 
-b is not universe polymorphic
 Expands to: Variable b
 negb : bool -> bool
 
-negb is not universe polymorphic
 negb is transparent
 Expands to: Constant Coq.Init.Datatypes.negb
 negb' : bool -> bool
 
-negb' is not universe polymorphic
 negb' is transparent
 Expands to: Constant Top.A.negb'
 negb'' : bool -> bool
 
-negb'' is not universe polymorphic
 negb'' is transparent
 Expands to: Constant Top.A.B.negb''
 a : bool -> bool
 
-a is not universe polymorphic
 Expands to: Variable a
 negb : bool -> bool
 
-negb is not universe polymorphic
 negb is transparent
 Expands to: Constant Coq.Init.Datatypes.negb
 negb' : bool -> bool
 
-negb' is not universe polymorphic
 negb' is transparent
 Expands to: Constant Top.negb'
 negb'' : bool -> bool
 
-negb'' is not universe polymorphic
 negb'' is transparent
 Expands to: Constant Top.negb''
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index c29f5649..1e3cc37d 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,8 +1,8 @@
 The command has indeed failed with message:
-=> Error: To rename arguments the "rename" flag must be specified.
+Error: To rename arguments the "rename" flag must be specified.
 Argument A renamed to B.
 The command has indeed failed with message:
-=> Error: To rename arguments the "rename" flag must be specified.
+Error: To rename arguments the "rename" flag must be specified.
 Argument A renamed to T.
 @eq_refl
      : forall (B : Type) (y : B), y = y
@@ -20,7 +20,6 @@ For eq: Argument scopes are [type_scope _ _]
 For eq_refl: Argument scopes are [type_scope _]
 eq_refl : forall (A : Type) (x : A), x = x
 
-eq_refl is not universe polymorphic
 Arguments are renamed to B, y
 When applied to no arguments:
   Arguments B, y are implicit and maximally inserted
@@ -36,7 +35,6 @@ For myEq: Argument scopes are [type_scope _ _]
 For myrefl: Argument scopes are [type_scope _ _]
 myrefl : forall (B : Type) (x : A), B -> myEq B x x
 
-myrefl is not universe polymorphic
 Arguments are renamed to C, x, _
 Argument C is implicit and maximally inserted
 Argument scopes are [type_scope _ _]
@@ -49,13 +47,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   end
      : forall T : Type, T -> nat -> nat -> nat
 
-myplus is not universe polymorphic
 Arguments are renamed to Z, t, n, m
 Argument Z is implicit and maximally inserted
 Argument scopes are [type_scope _ nat_scope nat_scope]
 myplus : forall T : Type, T -> nat -> nat -> nat
 
-myplus is not universe polymorphic
 Arguments are renamed to Z, t, n, m
 Argument Z is implicit and maximally inserted
 Argument scopes are [type_scope _ nat_scope nat_scope]
@@ -74,7 +70,6 @@ For myEq: Argument scopes are [type_scope type_scope _ _]
 For myrefl: Argument scopes are [type_scope type_scope _ _]
 myrefl : forall (A B : Type) (x : A), B -> myEq A B x x
 
-myrefl is not universe polymorphic
 Arguments are renamed to A, C, x, _
 Argument C is implicit and maximally inserted
 Argument scopes are [type_scope type_scope _ _]
@@ -89,13 +84,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   end
      : forall T : Type, T -> nat -> nat -> nat
 
-myplus is not universe polymorphic
 Arguments are renamed to Z, t, n, m
 Argument Z is implicit and maximally inserted
 Argument scopes are [type_scope _ nat_scope nat_scope]
 myplus : forall T : Type, T -> nat -> nat -> nat
 
-myplus is not universe polymorphic
 Arguments are renamed to Z, t, n, m
 Argument Z is implicit and maximally inserted
 Argument scopes are [type_scope _ nat_scope nat_scope]
@@ -106,15 +99,15 @@ Expands to: Constant Top.myplus
 @myplus
      : forall Z : Type, Z -> nat -> nat -> nat
 The command has indeed failed with message:
-=> Error: All arguments lists must declare the same names.
+Error: All arguments lists must declare the same names.
 The command has indeed failed with message:
-=> Error: The following arguments are not declared: x.
+Error: The following arguments are not declared: x.
 The command has indeed failed with message:
-=> Error: Arguments names must be distinct.
+Error: Arguments names must be distinct.
 The command has indeed failed with message:
-=> Error: Argument z cannot be declared implicit.
+Error: Argument z cannot be declared implicit.
 The command has indeed failed with message:
-=> Error: Extra argument y.
+Error: Extra argument y.
 The command has indeed failed with message:
-=> Error: To rename arguments the "rename" flag must be specified.
+Error: To rename arguments the "rename" flag must be specified.
 Argument A renamed to R.
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index d5903483..09f032d4 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -6,8 +6,6 @@ fix F (t : t) : P t :=
   end
      : forall P : t -> Type,
        (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
-
-t_rect is not universe polymorphic
      = fun d : TT => match d with
                      | @CTT _ _ b => b
                      end
@@ -26,7 +24,6 @@ match Nat.eq_dec x y with
 end
      : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
 
-proj is not universe polymorphic
 Argument scopes are [nat_scope nat_scope _ _ _]
 foo = 
 fix foo (A : Type) (l : list A) {struct l} : option A :=
@@ -37,7 +34,6 @@ fix foo (A : Type) (l : list A) {struct l} : option A :=
   end
      : forall A : Type, list A -> option A
 
-foo is not universe polymorphic
 Argument scopes are [type_scope list_scope]
 uncast = 
 fun (A : Type) (x : I A) => match x with
@@ -45,12 +41,9 @@ fun (A : Type) (x : I A) => match x with
                             end
      : forall A : Type, I A -> A
 
-uncast is not universe polymorphic
 Argument scopes are [type_scope _]
 foo' = if A 0 then true else false
      : bool
-
-foo' is not universe polymorphic
 f = 
 fun H : B =>
 match H with
@@ -61,5 +54,3 @@ match H with
      else fun _ : P false => Logic.I) x
 end
      : B -> True
-
-f is not universe polymorphic
diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index bcc37b63..6354ad46 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -1,7 +1,7 @@
 The command has indeed failed with message:
-=> Error: The field t is missing in Top.M.
+The field t is missing in Top.M.
 The command has indeed failed with message:
-=> Error: Unable to unify "nat" with "True".
+Unable to unify "nat" with "True".
 The command has indeed failed with message:
-=> In nested Ltac calls to "f" and "apply x", last call failed.
-Error: Unable to unify "nat" with "True".
+In nested Ltac calls to "f" and "apply x", last call failed.
+Unable to unify "nat" with "True".
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index 0b0f501f..3b65003c 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -5,7 +5,6 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I
 d2 = fun x : nat => d1 (y:=x)
      : forall x x0 : nat, x0 = x -> x0 = x
 
-d2 is not universe polymorphic
 Arguments x, x0 are implicit
 Argument scopes are [nat_scope nat_scope _]
 map id (1 :: nil)
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 60ee72b3..6efd671a 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -41,29 +41,29 @@ fun x : nat => ifn x is succ n then n else 0
 -4
      : Z
 The command has indeed failed with message:
-=> Error: x should not be bound in a recursive pattern of the right-hand side.
+Error: x should not be bound in a recursive pattern of the right-hand side.
 The command has indeed failed with message:
-=> Error: in the right-hand side, y and z should appear in
+Error: in the right-hand side, y and z should appear in
 term position as part of a recursive pattern.
 The command has indeed failed with message:
-=> Error: The reference w was not found in the current environment.
+The reference w was not found in the current environment.
 The command has indeed failed with message:
-=> Error: in the right-hand side, y and z should appear in
+Error: in the right-hand side, y and z should appear in
 term position as part of a recursive pattern.
 The command has indeed failed with message:
-=> Error: z is expected to occur in binding position in the right-hand side.
+Error: z is expected to occur in binding position in the right-hand side.
 The command has indeed failed with message:
-=> Error: as y is a non-closed binder, no such "," is allowed to occur.
+Error: as y is a non-closed binder, no such "," is allowed to occur.
 The command has indeed failed with message:
-=> Error: Cannot find where the recursive pattern starts.
+Error: Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-=> Error: Cannot find where the recursive pattern starts.
+Error: Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-=> Error: Cannot find where the recursive pattern starts.
+Error: Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-=> Error: Cannot find where the recursive pattern starts.
+Error: Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-=> Error: Both ends of the recursive pattern are the same.
+Error: Both ends of the recursive pattern are the same.
 SUM (nat * nat) nat
      : Set
 FST (0; 1)
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index 0457c860..ba076f05 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -25,7 +25,6 @@ For eq: Argument scopes are [type_scope _ _]
 For eq_refl: Argument scopes are [type_scope _]
 eq_refl : forall (A : Type) (x : A), x = x
 
-eq_refl is not universe polymorphic
 When applied to no arguments:
   Arguments A, x are implicit and maximally inserted
 When applied to 1 argument:
@@ -46,11 +45,9 @@ fix add (n m : nat) {struct n} : nat :=
   end
      : nat -> nat -> nat
 
-Nat.add is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 Nat.add : nat -> nat -> nat
 
-Nat.add is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 Nat.add is transparent
 Expands to: Constant Coq.Init.Nat.add
@@ -58,7 +55,6 @@ Nat.add : nat -> nat -> nat
 
 plus_n_O : forall n : nat, n = n + 0
 
-plus_n_O is not universe polymorphic
 Argument scope is [nat_scope]
 plus_n_O is opaque
 Expands to: Constant Coq.Init.Peano.plus_n_O
@@ -80,13 +76,11 @@ For le_n: Argument scope is [nat_scope]
 For le_S: Argument scopes are [nat_scope nat_scope _]
 comparison : Set
 
-comparison is not universe polymorphic
 Expands to: Inductive Coq.Init.Datatypes.comparison
 Inductive comparison : Set :=
     Eq : comparison | Lt : comparison | Gt : comparison
 bar : foo
 
-bar is not universe polymorphic
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
@@ -94,14 +88,12 @@ Argument x is implicit and maximally inserted
 Expands to: Constant Top.bar
 *** [ bar : foo ]
 
-bar is not universe polymorphic
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
 Argument x is implicit and maximally inserted
 bar : foo
 
-bar is not universe polymorphic
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
@@ -109,7 +101,6 @@ Argument x is implicit and maximally inserted
 Expands to: Constant Top.bar
 *** [ bar : foo ]
 
-bar is not universe polymorphic
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out
index 67b65d4b..f94ed642 100644
--- a/test-suite/output/TranspModtype.out
+++ b/test-suite/output/TranspModtype.out
@@ -1,15 +1,7 @@
 TrM.A = M.A
      : Set
-
-TrM.A is not universe polymorphic
 OpM.A = M.A
      : Set
-
-OpM.A is not universe polymorphic
 TrM.B = M.B
      : Set
-
-TrM.B is not universe polymorphic
 *** [ OpM.B : Set ]
-
-OpM.B is not universe polymorphic
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index d69baaec..b1952aec 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -4,8 +4,6 @@ fun e : option L => match e with
                     | None => None
                     end
      : option L -> option L
-
-P is not universe polymorphic
 fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
      : forall m n p : nat, S m <= S n + p -> m <= n + p
 fun n : nat => let x := A n in ?y ?y0:T n
diff --git a/test-suite/output/names.out b/test-suite/output/names.out
index 2892dfd5..9471b892 100644
--- a/test-suite/output/names.out
+++ b/test-suite/output/names.out
@@ -1,5 +1,4 @@
 The command has indeed failed with message:
-=> Error:
 In environment
 y : nat
 The term "a y" has type "{y0 : nat | y = y0}"
diff --git a/test-suite/output/rewrite-2172.out b/test-suite/output/rewrite-2172.out
index 30385072..27b0dc1b 100644
--- a/test-suite/output/rewrite-2172.out
+++ b/test-suite/output/rewrite-2172.out
@@ -1,2 +1,2 @@
 The command has indeed failed with message:
-=> Error: Unable to find an instance for the variable E.
+Unable to find an instance for the variable E.
diff --git a/test-suite/output/simpl.v b/test-suite/output/simpl.v
index 89638eed..5f1926f1 100644
--- a/test-suite/output/simpl.v
+++ b/test-suite/output/simpl.v
@@ -4,10 +4,10 @@ Goal forall x, 0+x = 1+x.
 intro x.
 simpl (_ + x).
 Show.
-Undo 2.
+Undo.
 simpl (_ + x) at 2.
 Show.
-Undo 2.
+Undo.
 simpl (0 + _).
 Show.
-Undo 2.
+Undo.
diff --git a/test-suite/prerequisite/admit.v b/test-suite/prerequisite/admit.v
new file mode 100644
index 00000000..fb327663
--- /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 d819dc47..56333973 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/Case22.v b/test-suite/success/Case22.v
index 4eb2dbe9..ce9050d4 100644
--- a/test-suite/success/Case22.v
+++ b/test-suite/success/Case22.v
@@ -5,3 +5,15 @@ Lemma a : forall x:I eq_refl, match x in I a b c return b = b with C => eq_refl
 intro.
 match goal with |- ?c => let x := eval cbv in c in change x end.
 Abort.
+
+Check forall x:I eq_refl, match x in I x return x = x with C => eq_refl end = eq_refl.
+
+(* This is bug #3210 *)
+
+Inductive I' : let X := Set in X :=
+| C' : I'.
+
+Definition foo (x : I') : bool :=
+  match x with
+  C' => true
+  end.
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 3d425754..9661b3bf 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -121,3 +121,44 @@ Inductive foo1 : forall p, Prop := cc1 : foo1 0.
 (* Check cross inference of evars from constructors *)
 
 Inductive foo2 : forall p, Prop := cc2 : forall q, foo2 q | cc3 : foo2 0.
+
+(* An example with reduction removing an occurrence of the inductive type in one of its argument *)
+
+Inductive IND1 (A:Type) := CONS1 : IND1 ((fun x => A) IND1).
+
+(* These types were considered as ill-formed before March 2015, while they
+   could be accepted considering that the type IND1 above was accepted *)
+
+Inductive IND2 (A:Type) (T:=fun _ : Type->Type => A) := CONS2 : IND2 A -> IND2 (T IND2).
+
+Inductive IND3 (A:Type) (T:=fun _ : Type->Type => A) := CONS3 : IND3 (T IND3) -> IND3 A.
+
+Inductive IND4 (A:Type) := CONS4 : IND4 ((fun x => A) IND4) -> IND4 A.
+
+(* This type was ok before March 2015 *)
+
+Inductive IND5 (A : Type) (T := A) : Type := CONS5 : IND5 ((fun _ => A) 0) -> IND5 A.
+
+(* An example of nested positivity which was rejected by the kernel
+   before 24 March 2015 (even with Unset Elimination Schemes to avoid
+   the _rect bug) due to the wrong computation of non-recursively
+   uniform parameters in list' *)
+
+Inductive list' (A:Type) (B:=A) :=
+| nil' : list' A
+| cons' : A -> list' B -> list' A.
+
+Inductive tree := node : list' tree -> tree.
+
+(* This type was raising an anomaly when building the _rect scheme,
+   because of a bug in Inductiveops.get_arity in the presence of
+   let-ins and recursively non-uniform parameters. *)
+
+Inductive L (A:Type) (T:=A) : Type := C : L nat -> L A.
+
+(* This type was raising an anomaly when building the _rect scheme,
+   because of a wrong computation of the number of non-recursively
+   uniform parameters when conversion is needed, leading the example to
+   hit the Inductiveops.get_arity bug mentioned above (see #3491) *)
+
+Inductive IND6 (A:Type) (T:=A) := CONS6 : IND6 T -> IND6 A.
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index 6a488244..25e464d6 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -1,3 +1,5 @@
+Require Eqdep_dec.
+
 (* Check the behaviour of Injection *)
 
 (* Check that Injection tries Intro until *)
diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v
index d316e4a0..e38affd7 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/TacticNotation1.v b/test-suite/success/TacticNotation1.v
new file mode 100644
index 00000000..289f2816
--- /dev/null
+++ b/test-suite/success/TacticNotation1.v
@@ -0,0 +1,20 @@
+Module Type S.
+End S.
+
+Module F (E : S).
+
+  Tactic Notation "foo" := idtac.
+
+  Ltac bar := foo.
+
+End F.
+
+Module G (E : S).
+  Module M := F E.
+
+  Lemma Foo : True.
+  Proof.
+  M.bar.
+  Abort.
+
+End G.
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 21b829aa..a4ed76c5 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -536,3 +536,13 @@ Goal forall f:nat->nat, (forall P x, P (f x)) -> let x:=f 0 in x = 0.
 intros f H x.
 apply H.
 Qed.
+
+(* Test that occur-check is not too restrictive (see comments of #3141) *)
+Lemma bar (X: nat -> nat -> Prop) (foo:forall x, X x x) (a: unit) (H: tt = a):
+  exists x, exists y, X x y.
+Proof.
+intros; eexists; eexists; case H.
+apply (foo ?y).
+Grab Existential Variables.
+exact 0.
+Qed.
diff --git a/test-suite/success/coindprim.v b/test-suite/success/coindprim.v
new file mode 100644
index 00000000..4e0b7bf5
--- /dev/null
+++ b/test-suite/success/coindprim.v
@@ -0,0 +1,52 @@
+Set Primitive Projections.
+
+CoInductive stream A := { hd : A; tl : stream A }.
+
+CoFixpoint ticks : stream unit :=
+  {| hd := tt; tl := ticks |}.
+
+Arguments hd [ A ] s.
+Arguments tl [ A ] s.
+
+CoInductive bisim {A} : stream A -> stream A -> Prop :=
+  | bisims s s' : hd s = hd s' -> bisim (tl s) (tl s') -> bisim s s'.
+
+Lemma bisim_refl {A} (s : stream A) : bisim s s.
+Proof.
+  revert s.
+  cofix aux. intros. constructor. reflexivity. apply aux.
+Defined.
+
+Lemma constr : forall (A : Type) (s : stream A),
+    bisim s (Build_stream _ s.(hd) s.(tl)).
+Proof.
+  intros. constructor. reflexivity. simpl. apply bisim_refl.
+Defined.
+
+Lemma constr' : forall (A : Type) (s : stream A),
+  s = Build_stream _ s.(hd) s.(tl).
+Proof.
+  intros. 
+  Fail destruct s. 
+Abort.
+
+Eval compute in constr _ ticks.
+
+Notation convertible x y := (eq_refl x : x = y).
+
+Fail Check convertible ticks {| hd := hd ticks; tl := tl ticks |}.
+
+CoInductive U := inU
+ { outU : U }.
+
+CoFixpoint u : U :=
+  inU u.
+
+CoFixpoint force (u : U) : U :=
+  inU (outU u).
+
+Lemma eq (x : U) : x = force x.
+Proof.
+  Fail destruct x.
+Abort.
+  (* Impossible *)
\ No newline at end of file
diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v
index dbbd57ae..61e73f85 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/qed_export.v b/test-suite/success/qed_export.v
new file mode 100644
index 00000000..b3e41ab1
--- /dev/null
+++ b/test-suite/success/qed_export.v
@@ -0,0 +1,18 @@
+Lemma a : True.
+Proof.
+assert True as H.
+  abstract (trivial) using exported_seff.
+exact H.
+Fail Qed exporting a_subproof.
+Qed exporting exported_seff.
+Check ( exported_seff : True ).
+
+Lemma b : True.
+Proof.
+assert True as H.
+  abstract (trivial) using exported_seff2.
+exact H.
+Qed.
+
+Fail Check ( exported_seff2 : True ).
+
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index 6dcd6592..62249666 100644
--- a/test-suite/success/rewrite.v
+++ b/test-suite/success/rewrite.v
@@ -148,3 +148,13 @@ eexists. intro H.
 rewrite H.
 reflexivity.
 Abort.
+
+(* Check that rewriting within evars still work (was broken in 8.5beta1) *)
+
+
+Goal forall (a: unit) (H: a = tt), exists x y:nat, x = y.
+intros; eexists; eexists.
+rewrite H.
+Undo.
+subst.
+Abort.
diff --git a/test-suite/success/rewrite_dep.v b/test-suite/success/rewrite_dep.v
index fe250ae8..d0aafd38 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 be0d49e0..0465c4b3 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 b5330779..e540ae5f 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) *)
 
diff --git a/test-suite/success/tryif.v b/test-suite/success/tryif.v
new file mode 100644
index 00000000..4394bddb
--- /dev/null
+++ b/test-suite/success/tryif.v
@@ -0,0 +1,50 @@
+Require Import TestSuite.admit.
+
+(** [not tac] is equivalent to [fail tac "succeeds"] if [tac] succeeds, and is equivalent to [idtac] if [tac] fails *)
+Tactic Notation "not" tactic3(tac) :=
+  (tryif tac then fail 0 tac "succeeds" else idtac); (* error if the tactic solved all goals *) [].
+
+(** Test if a tactic succeeds, but always roll-back the results *)
+Tactic Notation "test" tactic3(tac) := tryif not tac then fail 0 tac "fails" else idtac.
+
+Goal Set.
+Proof.
+  not fail.
+  not not idtac.
+  not fail 0.
+  (** Would be nice if we could get [not fail 1] to pass, maybe *)
+  not not admit.
+  not not test admit.
+  not progress test admit.
+  (* test grouping *)
+  not (not idtac; fail).
+  assert True.
+  all:not fail.
+  2:not fail.
+  all:admit.
+Defined.
+
+Goal Set.
+Proof.
+  test idtac.
+  test try fail.
+  test admit.
+  test match goal with |- Set => idtac end.
+  test (idtac; match goal with |- Set => idtac end).
+  (* test grouping *)
+  first [ (test idtac; fail); fail 1 | idtac ].
+  try test fail.
+  try test test fail.
+  test test idtac.
+  test test admit.
+  Fail test fail.
+  test (idtac; []).
+  test (assert True; [|]).
+  (* would be nice, perhaps, if we could catch [fail 1] and not just [fail 0] this *)
+  try ((test fail); fail 1).
+  assert True.
+  all:test idtac.
+  all:test admit.
+  2:test admit.
+  all:admit.
+Defined.