Merge remote-tracking branch 'upstream/trunk' into trunk

44 files changed, 1006 insertions, 184 deletions

diff --git a/test-suite/bugs/closed/2141.v b/test-suite/bugs/closed/2141.v
index 941ae530fd..098a7e9e72 100644
--- a/test-suite/bugs/closed/2141.v
+++ b/test-suite/bugs/closed/2141.v
@@ -1,3 +1,4 @@
+Require Coq.extraction.Extraction.
 Require Import FSetList.
 Require Import OrderedTypeEx.
 
diff --git a/test-suite/bugs/closed/3036.v b/test-suite/bugs/closed/3036.v
index 451bec9b20..3b57310d6e 100644
--- a/test-suite/bugs/closed/3036.v
+++ b/test-suite/bugs/closed/3036.v
@@ -15,11 +15,11 @@ Definition perm := Qc.
 Locate Qle_bool.
 
 Definition compatibleb (p1 p2 : perm) : bool :=
-let p1pos := Qle_bool 00 p1 in
-  let p2pos := Qle_bool 00 p2 in
+let p1pos := Qle_bool 0 p1 in
+  let p2pos := Qle_bool 0 p2 in
     negb (
          (p1pos && p2pos)
-      || ((p1pos || p2pos) && (negb (Qle_bool 00 ((p1 + p2)%Qc)))))%Qc.
+      || ((p1pos || p2pos) && (negb (Qle_bool 0 ((p1 + p2)%Qc)))))%Qc.
 
 Definition compatible (p1 p2 : perm) := compatibleb p1 p2 = true.
 
diff --git a/test-suite/bugs/closed/3287.v b/test-suite/bugs/closed/3287.v
index 7c78131252..1b758acd73 100644
--- a/test-suite/bugs/closed/3287.v
+++ b/test-suite/bugs/closed/3287.v
@@ -1,3 +1,5 @@
+Require Coq.extraction.Extraction.
+
 Module Foo.
 (* Definition foo := (I,I). *)
 Definition bar := true.
diff --git a/test-suite/bugs/closed/3330.v b/test-suite/bugs/closed/3330.v
index e3b5e94356..672fb3f131 100644
--- a/test-suite/bugs/closed/3330.v
+++ b/test-suite/bugs/closed/3330.v
@@ -41,6 +41,8 @@ Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function
 
 Open Scope function_scope.
 
+Set Printing Universes. Set Printing All.
+
 Inductive paths {A : Type} (a : A) : A -> Type :=
   idpath : paths a a.
 
@@ -156,7 +158,8 @@ Delimit Scope morphism_scope with morphism.
 
 Delimit Scope category_scope with category.
 Delimit Scope object_scope with object.
-
+Set Printing Universes.
+Set Printing All.
 Record PreCategory :=
   Build_PreCategory' {
       object :> Type;
@@ -1069,7 +1072,7 @@ Section Adjunction.
   Variable F : Functor C D.
   Variable G : Functor D C.
 
-  Let Adjunction_Type := 
+ Let Adjunction_Type := 
     Eval simpl in (hom_functor D) o (F^op, 1) <~=~> (hom_functor C) o (1, G).
 
   Record AdjunctionHom :=
diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v
index 73709268a4..33e5d532ad 100644
--- a/test-suite/bugs/closed/3612.v
+++ b/test-suite/bugs/closed/3612.v
@@ -39,7 +39,6 @@ Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P)
 p = q.
 
 Declare ML Module "ltac_plugin".
-Declare ML Module "coretactics".
 
 Set Default Proof Mode "Classic".
 
diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v
index 179f81e668..a664a1ef1d 100644
--- a/test-suite/bugs/closed/3649.v
+++ b/test-suite/bugs/closed/3649.v
@@ -3,7 +3,6 @@
 (* 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) *)
 Declare ML Module "ltac_plugin".
-Declare ML Module "coretactics".
 Set Default Proof Mode "Classic".
 Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
 Reserved Notation "x = y" (at level 70, no associativity).
@@ -14,7 +13,6 @@ 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 :=
diff --git a/test-suite/bugs/closed/3923.v b/test-suite/bugs/closed/3923.v
index 0aa029e73d..2fb0a5439a 100644
--- a/test-suite/bugs/closed/3923.v
+++ b/test-suite/bugs/closed/3923.v
@@ -1,3 +1,5 @@
+Require Coq.extraction.Extraction.
+
 Module Type TRIVIAL.
 Parameter t:Type.
 End TRIVIAL.
diff --git a/test-suite/bugs/closed/3943.v b/test-suite/bugs/closed/3943.v
new file mode 100644
index 0000000000..5e5ba816f9
--- /dev/null
+++ b/test-suite/bugs/closed/3943.v
@@ -0,0 +1,50 @@
+(* File reduced by coq-bug-finder from original input, then from 9492 lines to 119 lines *)
+(* coqc version 8.5beta1 (January 2015) compiled on Jan 18 2015 7:27:36 with OCaml 3.12.1
+   coqtop version 8.5beta1 (January 2015) *)
+
+Set Typeclasses Dependency Order.
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+Notation "x = y" := (@paths _ x y) : type_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.
+
+Set Implicit Arguments.
+Delimit Scope morphism_scope with morphism.
+Delimit Scope category_scope with category.
+Delimit Scope object_scope with object.
+
+Record PreCategory := Build_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' }.
+Arguments identity {!C%category} / x%object : rename.
+Arguments compose {!C%category} / {s d d'}%object (m1 m2)%morphism : rename.
+
+Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) := {
+    morphism_inverse : morphism C d s;
+    left_inverse : compose morphism_inverse m = identity _;
+    right_inverse : compose m morphism_inverse = identity _ }.
+Arguments morphism_inverse {C s d} m {_}.
+Local Notation "m ^-1" := (morphism_inverse m) (at level 3, format "m '^-1'") : morphism_scope.
+
+Class Isomorphic {C : PreCategory} s d := {
+    morphism_isomorphic :> morphism C s d;
+    isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic }.
+Coercion morphism_isomorphic : Isomorphic >-> morphism.
+
+Variable C : PreCategory.
+Variables s d : C.
+
+Definition path_isomorphic (i j : Isomorphic s d)
+: @morphism_isomorphic _ _ _ i = @morphism_isomorphic _ _ _ j -> i = j.
+Admitted.
+
+Definition ap_morphism_inverse_path_isomorphic (i j : Isomorphic s d) p q
+: ap (fun e : Isomorphic s d => e^-1)%morphism (path_isomorphic i j p) = q.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4250.v b/test-suite/bugs/closed/4250.v
new file mode 100644
index 0000000000..74cacf559a
--- /dev/null
+++ b/test-suite/bugs/closed/4250.v
@@ -0,0 +1,11 @@
+Require Import FunInd.
+Require  Vector.
+Generalizable All Variables.
+
+Definition f `{n:nat , u:Vector.t A n} := n.
+
+Function f2 {A:Type} {n:nat} {v:Vector.t A n} : nat := n.
+
+(* fails with "The reference A was not found in the current environment." *)
+Function f3 `{n:nat , u:Vector.t A n} := u.
+Check R_f3_complete.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4366.v b/test-suite/bugs/closed/4366.v
index 6a5e9a4023..403c2d2026 100644
--- a/test-suite/bugs/closed/4366.v
+++ b/test-suite/bugs/closed/4366.v
@@ -10,6 +10,6 @@ end.
 Goal True.
 Proof.
 pose (v := stupid 24).
-Timeout 2 vm_compute in v.
+Timeout 4 vm_compute in v.
 exact I.
 Qed.
diff --git a/test-suite/bugs/closed/4394.v b/test-suite/bugs/closed/4394.v
deleted file mode 100644
index 1ad81345db..0000000000
--- a/test-suite/bugs/closed/4394.v
+++ /dev/null
@@ -1,19 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
-
-Require Import Equality List.
-Inductive Foo (I : Type -> Type) (A : Type) : Type :=
-| foo (B : Type) : A -> I B -> Foo I A.
-Definition Family := Type -> Type.
-Definition FooToo : Family -> Family := Foo.
-Definition optionize (I : Type -> Type) (A : Type) := option (I A).
-Definition bar (I : Type -> Type) (A : Type) : A -> option (I A) -> Foo (optionize I) A := foo (optionize I) A A.
-Record Rec (I : Type -> Type) := { rec : forall A : Type, A -> I A -> Foo I A }.
-Definition barRec : Rec (optionize id) := {| rec := bar id |}.
-Inductive Empty {T} : T -> Prop := .
-Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family) nil)) (b : unit) :
-  Empty (a, b) -> False.
-Proof.
-  intro e.
-  dependent induction e.
-Qed.
-
diff --git a/test-suite/bugs/closed/4400.v b/test-suite/bugs/closed/4400.v
deleted file mode 100644
index a89cf0cbc3..0000000000
--- a/test-suite/bugs/closed/4400.v
+++ /dev/null
@@ -1,19 +0,0 @@
-(* -*- coq-prog-args: ("-require" "Coq.Compat.Coq84" "-compat" "8.4") -*- *)
-Require Import Coq.Lists.List Coq.Logic.JMeq Program.Equality.
-Set Printing Universes.
-Inductive Foo (I : Type -> Type) (A : Type) : Type :=
-| foo (B : Type) : A -> I B -> Foo I A.
-Definition Family := Type -> Type.
-Definition FooToo : Family -> Family := Foo.
-Definition optionize (I : Type -> Type) (A : Type) := option (I A).
-Definition bar (I : Type -> Type) (A : Type) : A -> option (I A) -> Foo(optionize I) A := foo (optionize I) A A.
-Record Rec (I : Type -> Type) := { rec : forall A : Type, A -> I A -> Foo I A }.
-Definition barRec : Rec (optionize id) := {| rec := bar id |}.
-Inductive Empty {T} : T -> Prop := .
-Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family)
-nil)) (b : unit) :
-  Empty (a, b) -> False.
-Proof.
-  intro e.
-  dependent induction e.
-Qed.
diff --git a/test-suite/bugs/closed/4616.v b/test-suite/bugs/closed/4616.v
index c862f82067..a59975dbcf 100644
--- a/test-suite/bugs/closed/4616.v
+++ b/test-suite/bugs/closed/4616.v
@@ -1,3 +1,5 @@
+Require Coq.extraction.Extraction.
+
 Set Primitive Projections.
 Record Foo' := Foo { foo : Type }.
 Axiom f : forall t : Foo', foo t.
diff --git a/test-suite/bugs/closed/4656.v b/test-suite/bugs/closed/4656.v
deleted file mode 100644
index a59eed2c86..0000000000
--- a/test-suite/bugs/closed/4656.v
+++ /dev/null
@@ -1,4 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
-Goal True.
-  constructor 1.
-Qed.
diff --git a/test-suite/bugs/closed/4710.v b/test-suite/bugs/closed/4710.v
index fdc8501099..5d8ca330ac 100644
--- a/test-suite/bugs/closed/4710.v
+++ b/test-suite/bugs/closed/4710.v
@@ -1,3 +1,5 @@
+Require Coq.extraction.Extraction.
+
 Set Primitive Projections.
 Record Foo' := Foo { foo : nat }.
 Extraction foo.
diff --git a/test-suite/bugs/closed/4727.v b/test-suite/bugs/closed/4727.v
deleted file mode 100644
index cfb4548d2c..0000000000
--- a/test-suite/bugs/closed/4727.v
+++ /dev/null
@@ -1,10 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
-Goal forall (P : Set) (l : P) (P0 : Set) (w w0 : P0) (T : Type) (a : P * T) (o : P -> option P0),
-    (forall (l1 l2 : P) (w1 : P0), o l1 = Some w1 -> o l2 = Some w1 -> l1 = l2) ->
-    o l = Some w -> o (fst a) = Some w0 -> {w = w0} + {w <> w0} -> False.
-Proof.
-  clear; intros ???????? inj H0 H1 H2.
-  destruct H2; intuition subst.
-  eapply inj in H1; [ | eauto ].
-  progress subst. (* should succeed, used to not succeed *)
-Abort.
diff --git a/test-suite/bugs/closed/4733.v b/test-suite/bugs/closed/4733.v
deleted file mode 100644
index a90abd71cf..0000000000
--- a/test-suite/bugs/closed/4733.v
+++ /dev/null
@@ -1,52 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
-(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5.  If they use*)
-Require Import Coq.Lists.List.
-Require Import Coq.Vectors.Vector.
-Import ListNotations.
-Import VectorNotations.
-Set Implicit Arguments.
-Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T).
-Arguments mynil {_}, _.
-
-Delimit Scope mylist_scope with mylist.
-Bind Scope mylist_scope with mylist.
-Delimit Scope vector_scope with vector.
-
-Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
-Notation " [ x ] " := (mycons x mynil) : mylist_scope.
-Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope.
-
-(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4.  There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *)
-Check [ ]%mylist : mylist _.
-Check [ ]%list : list _.
-Check []%vector : Vector.t _ _.
-Check [ _ ]%mylist : mylist _.
-Check [ _ ]%list : list _.
-Check [ _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%list : list _.
-Check [ _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ; _ ]%mylist : mylist _.
-
-Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z mynil) ..)) : mylist_scope.
-(* Now these all work, but not so in 8.4.  If we get the ability to remove notations, this section can also just be removed. *)
-Check [ ]%mylist : mylist _.
-Check [ ]%list : list _.
-Check []%vector : Vector.t _ _.
-Check [ _ ]%mylist : mylist _.
-Check [ _ ]%list : list _.
-Check [ _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%list : list _.
-Check [ _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ; _ ]%mylist : mylist _.
diff --git a/test-suite/bugs/closed/5372.v b/test-suite/bugs/closed/5372.v
index 2dc78d4c7f..e60244cd1d 100644
--- a/test-suite/bugs/closed/5372.v
+++ b/test-suite/bugs/closed/5372.v
@@ -1,4 +1,5 @@
 (* coq bug 5372: https://coq.inria.fr/bugs/show_bug.cgi?id=5372 *)
+Require Import FunInd.
 Function odd (n:nat) :=
   match n with
   | 0 => false
diff --git a/test-suite/bugs/closed/5414.v b/test-suite/bugs/closed/5414.v
new file mode 100644
index 0000000000..2522a274fb
--- /dev/null
+++ b/test-suite/bugs/closed/5414.v
@@ -0,0 +1,12 @@
+(* Use of idents bound to ltac names in a "match" *)
+
+Definition foo : Type.
+Proof.
+  let x := fresh "a" in
+  refine (forall k : nat * nat, let '(x, _) := k in (_ : Type)).
+  exact (a = a).
+Defined.
+Goal foo.
+intros k. elim k. (* elim because elim keeps names *)
+intros.
+Check a. (* We check that the name is "a" *)
diff --git a/test-suite/bugs/closed/5578.v b/test-suite/bugs/closed/5578.v
new file mode 100644
index 0000000000..5bcdaa2f18
--- /dev/null
+++ b/test-suite/bugs/closed/5578.v
@@ -0,0 +1,57 @@
+(* File reduced by coq-bug-finder from original input, then from 1549 lines to  298 lines, then from 277 lines to 133 lines, then from 985 lines to 138 lines,  then from 206 lines to 139 lines, then from 203 lines to 142 lines, then from  262 lines to 152 lines, then from 567 lines to 151 lines, then from 3746 lines  to 151 lines, then from 577 lines to 151 lines, then from 187 lines to 151  lines, thenfrom 981 lines to 940 lines, then from 938 lines to 175 lines, then  from 589 lines to 205 lines, then from 3797 lines to 205 lines, then from 628  lines to 206 lines, then from 238 lines to 205 lines, then from 1346 lines to  213 lines, then from 633 lines to 214 lines, then from 243 lines to 213 lines,  then from 5656 lines to 245 lines, then from 661 lines to 272 lines, then from  3856 lines to 352 lines, then from 1266 lines to 407 lines, then from 421 lines  to 406 lines, then from 424 lines to 91 lines, then from 105 lines to 91 lines,  then from 85 lines to 55 lines, then from 69 lines to 55 lines *)
+(* coqc version trunk (May 2017) compiled on May 30 2017 13:28:59 with OCaml 
+4.02.3
+   coqtop version jgross-Leopard-WS:/home/jgross/Downloads/coq/coq-trunk,trunk  (fd36c0451c26e44b1b7e93299d3367ad2d35fee3) *)
+
+Class Proper {A} (R : A -> A -> Prop) (m : A) := mkp : R m m.
+Definition respectful {A B} (R : A -> A -> Prop) (R' : B -> B -> Prop) (f g : A  -> B) := forall x y, R x y -> R' (f x) (g y).
+Set Implicit Arguments.
+
+Class EqDec (A : Set) := {
+  eqb : A -> A -> bool ;
+  eqb_leibniz : forall x y, eqb x y = true <-> x = y
+}.
+
+Infix "?=" := eqb (at level 70) : eq_scope.
+
+Inductive Comp : Set -> Type :=
+| Bind : forall (A B : Set), Comp B -> (B -> Comp A) -> Comp A.
+
+Open Scope eq_scope.
+
+Goal forall (Rat : Set) (PositiveMap_t : Set -> Set)
+            type (t : type) (interp_type_list_message interp_type_rand  interp_type_message : nat -> Set),
+    (forall eta : nat, PositiveMap_t (interp_type_rand eta) ->  interp_type_list_message eta -> interp_type_message eta) ->
+    ((nat -> Rat) -> Prop) ->
+    forall (interp_type_sbool : nat -> Set) (interp_type0 : type -> nat -> Set),
+      (forall eta : nat,
+          (interp_type_list_message eta -> interp_type_message eta) ->  PositiveMap_t (interp_type_rand eta) -> interp_type0 t eta)
+      -> (forall (t0 : type) (eta : nat), EqDec (interp_type0 t0 eta))
+      -> (bool -> Comp bool) -> False.
+  clear.
+  intros Rat PositiveMap_t type t interp_type_list_message interp_type_rand  interp_type_message adv negligible interp_type_sbool
+         interp_type interp_term_fixed_t_x
+         EqDec_interp_type ret_bool.
+  assert (forall f adv' k
+                 (lem : forall (eta : nat) (evil_rands rands : PositiveMap_t 
+(interp_type_rand eta)),
+                     (interp_term_fixed_t_x eta (adv eta evil_rands) rands
+                                            ?= interp_term_fixed_t_x eta (adv  eta evil_rands) rands) = true),
+             (forall (eta : nat), Proper (respectful eq eq) (f eta))
+             -> negligible
+                  (fun eta : nat =>
+                     f eta (
+                         (Bind (k eta) (fun rands =>
+                          ret_bool (interp_term_fixed_t_x eta (adv' eta) rands  ?= interp_term_fixed_t_x eta (adv' eta) rands)))))).
+  Undo.
+  assert (forall f adv' k
+                 (lem : forall (eta : nat) (rands : PositiveMap_t 
+(interp_type_rand eta)),
+                     (interp_term_fixed_t_x eta (adv' eta) rands ?=  interp_term_fixed_t_x eta (adv' eta) rands) = true),
+             (forall (eta : nat), Proper (respectful eq eq) (f eta))
+             -> negligible
+                  (fun eta : nat =>
+                     f eta (
+                         (Bind (k eta) (fun rands =>
+                          ret_bool (interp_term_fixed_t_x eta (adv' eta) rands  ?= interp_term_fixed_t_x eta (adv' eta) rands)))))).
+ (* Error: Anomaly "Signature and its instance do not match." Please report at http://coq.inria.fr/bugs/. *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/5618.v b/test-suite/bugs/closed/5618.v
new file mode 100644
index 0000000000..ab88a88f44
--- /dev/null
+++ b/test-suite/bugs/closed/5618.v
@@ -0,0 +1,9 @@
+Require Import FunInd.
+
+Function test {T} (v : T) (x : nat) : nat :=
+  match x with
+  | 0 => 0
+  | S x' => test v x'
+  end.
+
+Check R_test_complete.
\ No newline at end of file
diff --git a/test-suite/bugs/opened/4803.v b/test-suite/bugs/opened/4803.v
deleted file mode 100644
index 4541f13d01..0000000000
--- a/test-suite/bugs/opened/4803.v
+++ /dev/null
@@ -1,48 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
-(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5.  If they use*)
-Require Import Coq.Lists.List.
-Require Import Coq.Vectors.Vector.
-Import ListNotations.
-Import VectorNotations.
-Set Implicit Arguments.
-Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T).
-Arguments mynil {_}, _.
-
-Delimit Scope mylist_scope with mylist.
-Bind Scope mylist_scope with mylist.
-Delimit Scope vector_scope with vector.
-
-Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
-Notation " [ x ] " := (mycons x mynil) : mylist_scope.
-Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope.
-
-(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4.  There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *)
-Check [ ]%mylist : mylist _.
-Check [ ]%list : list _.
-Check []%vector : Vector.t _ _.
-Check [ _ ]%mylist : mylist _.
-Check [ _ ]%list : list _.
-Check [ _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%list : list _.
-Check [ _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ; _ ]%mylist : mylist _.
-
-(** Now check that we can add and then remove notations from the parser *)
-(* We should be able to stick some vernacular here to remove [] from the parser *)
-Fail Remove Notation "[]".
-Goal True.
-  (* This should not be a syntax error; before moving this file to closed, uncomment this line. *)
-  (* idtac; []. *)
-  constructor.
-Qed.
-
-Check { _ : _ & _ }.
-Reserved Infix "&" (at level 0).
-Fail Remove Infix "&".
-(* Check { _ : _ & _ }. *)
diff --git a/test-suite/coq-makefile/arg/_CoqProject b/test-suite/coq-makefile/arg/_CoqProject
index afdb32e7cf..53dc963997 100644
--- a/test-suite/coq-makefile/arg/_CoqProject
+++ b/test-suite/coq-makefile/arg/_CoqProject
@@ -1,7 +1,7 @@
 -R theories test
 -R src test
 -I src
--arg "-compat 8.4"
+-arg "-w default"
 
 src/test_plugin.mlpack
 src/test.ml4
diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v
new file mode 100644
index 0000000000..a978f6b901
--- /dev/null
+++ b/test-suite/coqchk/cumulativity.v
@@ -0,0 +1,67 @@
+Set Universe Polymorphism.
+Set Inductive Cumulativity.
+Set Printing Universes.
+
+Inductive List (A: Type) := nil | cons : A -> List A -> List A.
+
+Section ListLift.
+  Universe i j.
+
+  Constraint i < j.
+
+  Definition LiftL {A} : List@{i} A -> List@{j} A := fun x => x.
+
+End ListLift.
+
+Lemma LiftL_Lem A (l : List A) : l = LiftL l.
+Proof. reflexivity. Qed.
+
+Section ListLower.
+  Universe i j.
+
+  Constraint i < j.
+
+  Definition LowerL {A : Type@{i}} : List@{j} A -> List@{i} A := fun x => x.
+
+End ListLower.
+
+Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l.
+Proof. reflexivity. Qed.
+(*
+I disable these tests because cqochk can't process them when compiled with
+   ocaml-4.02.3+32bit and camlp5-4.16 which is the case for Travis!
+
+   I have added this file (including the commented parts below) in
+   test-suite/success/cumulativity.v which doesn't run coqchk on them.
+*)
+(* Inductive Tp := tp : Type -> Tp. *)
+
+(* Section TpLift. *)
+(*   Universe i j. *)
+
+(*   Constraint i < j. *)
+
+(*   Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x. *)
+
+(* End TpLift. *)
+
+(* Lemma LiftC_Lem (t : Tp) : LiftTp t = t. *)
+(* Proof. reflexivity. Qed. *)
+
+(* Section TpLower. *)
+(*   Universe i j. *)
+
+(*   Constraint i < j. *)
+
+(*   Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x. *)
+
+(* End TpLower. *)
+
+
+(* Section subtyping_test. *)
+(*   Universe i j. *)
+(*   Constraint i < j. *)
+
+(*   Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2. *)
+
+(* End subtyping_test. *)
\ No newline at end of file
diff --git a/test-suite/ide/blocking-futures.fake b/test-suite/ide/blocking-futures.fake
index b63f09bcfc..541fb798c0 100644
--- a/test-suite/ide/blocking-futures.fake
+++ b/test-suite/ide/blocking-futures.fake
@@ -4,6 +4,7 @@
 # Extraction will force the future computation, assert it is blocking
 # Example courtesy of Jonathan (jonikelee)
 #
+ADD { Require Coq.extraction.Extraction. }
 ADD { Require Import List. }
 ADD { Import ListNotations. }
 ADD { Definition myrev{A}(l : list A) : {rl : list A | rl = rev l}. }
diff --git a/test-suite/misc/deps-checksum.sh b/test-suite/misc/deps-checksum.sh
index 1e2afb7540..e07612b84c 100755
--- a/test-suite/misc/deps-checksum.sh
+++ b/test-suite/misc/deps-checksum.sh
@@ -1,4 +1,4 @@
-rm -f misc/deps/*/*.vo
+rm -f misc/deps/A/*.vo misc/deps/B/*.vo
 $coqc -R misc/deps/A A misc/deps/A/A.v
 $coqc -R misc/deps/B A misc/deps/B/A.v
 $coqc -R misc/deps/B A misc/deps/B/B.v
diff --git a/test-suite/misc/deps-order.sh b/test-suite/misc/deps-order.sh
index 375b706f0a..00c5eb1bd5 100755
--- a/test-suite/misc/deps-order.sh
+++ b/test-suite/misc/deps-order.sh
@@ -1,7 +1,7 @@
 # Check that both coqdep and coqtop/coqc supports -R
 # Check that both coqdep and coqtop/coqc takes the later -R
 # See bugs 2242, 2337, 2339
-rm -f misc/deps/*/*.vo
+rm -f misc/deps/lib/*.vo misc/deps/client/*.vo
 tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`
 $coqdep -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 | head -n 1 > $tmpoutput
 diff -u misc/deps/deps.out $tmpoutput 2>&1
diff --git a/test-suite/misc/printers.sh b/test-suite/misc/printers.sh
index c822d0eb37..28e7dc362f 100755
--- a/test-suite/misc/printers.sh
+++ b/test-suite/misc/printers.sh
@@ -1,3 +1,3 @@
-printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | grep Unbound
+printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | egrep "Error|Unbound"
 if [ $? = 0 ]; then exit 1; else exit 0; fi
 
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index f064dfe763..97fa8e2542 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -80,3 +80,49 @@ fun '(D n m p q) => n + m + p + q
      : J -> nat
 The command has indeed failed with message:
 The constructor D (in type J) expects 3 arguments.
+lem1 = 
+fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
+     : forall k : nat * nat, k = k
+lem2 = 
+fun dd : bool => if dd as aa return (aa = aa) then eq_refl else eq_refl
+     : forall k : bool, k = k
+
+Argument scope is [bool_scope]
+lem3 = 
+fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
+     : forall k : nat * nat, k = k
+1 subgoal
+  
+  x : nat
+  n, n0 := match x + 0 with
+           | 0 => 0
+           | S _ => 0
+           end : nat
+  e,
+  e0 := match x + 0 as y return (y = y) with
+        | 0 => eq_refl
+        | S n => eq_refl
+        end : x + 0 = x + 0
+  n1, n2 := match x with
+            | 0 => 0
+            | S _ => 0
+            end : nat
+  e1, e2 := match x return (x = x) with
+            | 0 => eq_refl
+            | S n => eq_refl
+            end : x = x
+  ============================
+  x + 0 = 0
+1 subgoal
+  
+  p : nat
+  a,
+  a0 := match eq_refl as y in (_ = e) return (y = y /\ e = e) with
+        | eq_refl => conj eq_refl eq_refl
+        end : eq_refl = eq_refl /\ p = p
+  a1,
+  a2 := match eq_refl in (_ = e) return (p = p /\ e = e) with
+        | eq_refl => conj eq_refl eq_refl
+        end : p = p /\ p = p
+  ============================
+  eq_refl = eq_refl
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 6a4fd007df..17fee3303d 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -121,3 +121,66 @@ Check fun x => let '(D n m p q) := x in n+m+p+q.
 (* This used to succeed, being interpreted as "let '{{n, m, p}} := ..." *)
 
 Fail Check fun x : J => let '{{n, m, _}} p := x in n + m + p.
+
+(* Test use of idents bound to ltac names in a "match" *)
+
+Lemma lem1 : forall k, k=k :>nat * nat.
+let x := fresh "aa" in
+let y := fresh "bb" in
+let z := fresh "cc" in
+let k := fresh "dd" in
+refine (fun k : nat * nat => match k as x return x = x with (y,z) => eq_refl end).
+Qed.
+Print lem1.
+
+Lemma lem2 : forall k, k=k :> bool.
+let x := fresh "aa" in
+let y := fresh "bb" in
+let z := fresh "cc" in
+let k := fresh "dd" in
+refine (fun k => if k as x return x = x then eq_refl else eq_refl).
+Qed.
+Print lem2.
+
+Lemma lem3 : forall k, k=k :>nat * nat.
+let x := fresh "aa" in
+let y := fresh "bb" in
+let z := fresh "cc" in
+let k := fresh "dd" in
+refine (fun k : nat * nat => let (y,z) as x return x = x := k in eq_refl).
+Qed.
+Print lem3.
+
+Lemma lem4 x : x+0=0.
+match goal with |- ?y = _ => pose (match y with 0 => 0 | S n => 0 end) end.
+match goal with |- ?y = _ => pose (match y as y with 0 => 0 | S n => 0 end) end.
+match goal with |- ?y = _ => pose (match y as y return y=y with 0 => eq_refl | S n => eq_refl end) end.
+match goal with |- ?y = _ => pose (match y return y=y with 0 => eq_refl | S n => eq_refl end) end.
+match goal with |- ?y + _ = _ => pose (match y with 0 => 0 | S n => 0 end) end.
+match goal with |- ?y + _ = _ => pose (match y as y with 0 => 0 | S n => 0 end) end.
+match goal with |- ?y + _ = _ => pose (match y as y return y=y with 0 => eq_refl | S n => eq_refl end) end.
+match goal with |- ?y + _ = _ => pose (match y return y=y with 0 => eq_refl | S n => eq_refl end) end.
+Show.
+
+Lemma lem5 (p:nat) : eq_refl p = eq_refl p.
+let y := fresh "n" in (* Checking that y is hidden *)
+  let z := fresh "e" in (* Checking that z is hidden *)
+  match goal with
+  |- ?y = _ => pose (match y as y in _ = z return y=y /\ z=z with eq_refl => conj eq_refl eq_refl end)
+  end.
+let y := fresh "n" in
+  let z := fresh "e" in
+  match goal with
+  |- ?y = _ => pose (match y in _ = z return y=y /\ z=z with eq_refl => conj eq_refl eq_refl end)
+  end.
+let y := fresh "n" in
+  let z := fresh "e" in
+  match goal with
+  |- eq_refl ?y = _ => pose (match eq_refl y in _ = z return y=y /\ z=z with eq_refl => conj eq_refl eq_refl end)
+  end.
+let p := fresh "p" in
+  let z := fresh "e" in
+  match goal with
+  |- eq_refl ?p = _ => pose (match eq_refl p in _ = z return p=p /\ z=z with eq_refl => conj eq_refl eq_refl end)
+  end.
+Show.
diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v
index 6c514b16ee..1ecd9771eb 100644
--- a/test-suite/output/Extraction_matchs_2413.v
+++ b/test-suite/output/Extraction_matchs_2413.v
@@ -1,5 +1,7 @@
 (** Extraction : tests of optimizations of pattern matching *)
 
+Require Coq.extraction.Extraction.
+
 (** First, a few basic tests *)
 
 Definition test1 b :=
diff --git a/test-suite/success/Case19.v b/test-suite/success/Case19.v
index e59828defe..ce98879a5f 100644
--- a/test-suite/success/Case19.v
+++ b/test-suite/success/Case19.v
@@ -17,3 +17,22 @@ Fail exists (fun x =>
         with
         | eq_refl => eq_refl
         end).
+Abort.
+
+(* Some tests with ltac matching on building "if" and "let" *)
+
+Goal forall b c d, (if negb b then c else d) = 0.
+intros.
+match goal with
+|- (if ?b then ?c else ?d) = 0 => transitivity (if b then d else c)
+end.
+Abort.
+
+Definition swap {A} {B} '((x,y):A*B) := (y,x).
+
+Goal forall p, (let '(x,y) := swap p in x + y) = 0.
+intros.
+match goal with
+|- (let '(x,y) := ?p in x + y) = 0 => transitivity (let (x,y) := p in x+y)
+end.
+Abort.
diff --git a/test-suite/success/Compat84.v b/test-suite/success/Compat84.v
deleted file mode 100644
index 732a024fc1..0000000000
--- a/test-suite/success/Compat84.v
+++ /dev/null
@@ -1,19 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
-
-Goal True.
-  solve [ constructor 1 ]. Undo.
-  solve [ econstructor 1 ]. Undo.
-  solve [ constructor ]. Undo.
-  solve [ econstructor ]. Undo.
-  solve [ constructor (fail) ]. Undo.
-  solve [ econstructor (fail) ]. Undo.
-  split.
-Qed.
-
-Goal False \/ True.
-  solve [ constructor (constructor) ]. Undo.
-  solve [ econstructor (econstructor) ]. Undo.
-  solve [ constructor 2; constructor ]. Undo.
-  solve [ econstructor 2; econstructor ]. Undo.
-  right; esplit.
-Qed.
diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v
index 3bf97c1312..f87f2e2a9d 100644
--- a/test-suite/success/Funind.v
+++ b/test-suite/success/Funind.v
@@ -1,4 +1,6 @@
 
+Require Import Coq.funind.FunInd.
+
 Definition iszero (n : nat) : bool :=
   match n with
   | O => true
diff --git a/test-suite/success/FunindExtraction_compat86.v b/test-suite/success/FunindExtraction_compat86.v
new file mode 100644
index 0000000000..8912197d2f
--- /dev/null
+++ b/test-suite/success/FunindExtraction_compat86.v
@@ -0,0 +1,506 @@
+(* -*- coq-prog-args: ("-compat" "8.6") -*- *)
+
+Definition iszero (n : nat) : bool :=
+  match n with
+  | O => true
+  | _ => false
+  end.
+
+Functional Scheme iszero_ind := Induction for iszero Sort Prop.
+
+Lemma toto : forall n : nat, n = 0 -> iszero n = true.
+intros x eg.
+ functional induction iszero x; simpl.
+trivial.
+inversion eg.
+Qed.
+
+
+Function ftest (n m : nat) : nat :=
+  match n with
+  | O => match m with
+         | O => 0
+         | _ => 1
+         end
+  | S p => 0
+  end.
+(* MS: FIXME: apparently can't define R_ftest_complete. Rest of the file goes through. *)
+
+Lemma test1 : forall n m : nat, ftest n m <= 2.
+intros n m.
+ functional induction ftest n m; auto.
+Qed.
+
+Lemma test2 : forall m n, ~ 2 = ftest n m.
+Proof.
+intros n m;intro H.
+functional inversion H ftest.
+Qed.
+
+Lemma test3 : forall n m, ftest n m = 0 -> (n = 0 /\ m = 0)  \/ n <> 0.
+Proof.
+functional inversion 1 ftest;auto.
+Qed.
+
+
+Require Import Arith.
+Lemma test11 : forall m : nat, ftest 0 m <= 2.
+intros m.
+ functional induction ftest 0 m.
+auto.
+auto.
+auto with *.
+Qed.
+
+Function lamfix (m n : nat) {struct n } : nat :=
+  match n with
+    | O => m
+    | S p => lamfix m p
+  end.
+
+(* Parameter v1 v2 : nat. *)
+
+Lemma lamfix_lem : forall v1 v2 : nat, lamfix v1 v2 = v1.
+intros v1 v2.
+ functional induction lamfix v1 v2.
+trivial.
+assumption.
+Defined.
+
+
+
+(* polymorphic function *)
+Require Import List.
+
+Functional Scheme app_ind := Induction for app Sort Prop.
+
+Lemma appnil : forall (A : Set) (l l' : list A), l' = nil -> l = l ++ l'.
+intros A l l'.
+ functional induction app A l l';  intuition.
+ rewrite <- H0; trivial.
+Qed.
+
+
+
+
+
+Require Export Arith.
+
+
+Function trivfun (n : nat) : nat :=
+  match n with
+  | O => 0
+  | S m => trivfun m
+  end.
+
+
+(* essaie de parametre variables non locaux:*)
+
+Parameter varessai : nat.
+
+Lemma first_try : trivfun varessai = 0.
+ functional induction trivfun varessai.
+trivial.
+assumption.
+Defined.
+
+
+ Functional Scheme triv_ind := Induction for trivfun Sort Prop.
+
+Lemma bisrepetita : forall n' : nat, trivfun n' = 0.
+intros n'.
+ functional induction trivfun n'.
+trivial.
+assumption.
+Qed.
+
+
+
+
+
+
+
+Function iseven (n : nat) : bool :=
+  match n with
+  | O => true
+  | S (S m) => iseven m
+  | _ => false
+  end.
+
+
+Function funex (n : nat) : nat :=
+  match iseven n with
+  | true => n
+  | false => match n with
+             | O => 0
+             | S r => funex r
+             end
+  end.
+
+
+Function nat_equal_bool (n m : nat) {struct n} : bool :=
+  match n with
+  | O => match m with
+         | O => true
+         | _ => false
+         end
+  | S p => match m with
+           | O => false
+           | S q => nat_equal_bool p q
+           end
+  end.
+
+
+Require Export Div2.
+Require Import Nat.
+Functional Scheme div2_ind := Induction for div2 Sort Prop.
+Lemma div2_inf : forall n : nat, div2 n <= n.
+intros n.
+ functional induction div2 n.
+auto.
+auto.
+
+apply le_S.
+apply le_n_S.
+exact IHn0.
+Qed.
+
+(* reuse this lemma as a scheme:*)
+
+Function nested_lam (n : nat) : nat -> nat :=
+  match n with
+  | O => fun m : nat => 0
+  | S n' => fun m : nat => m + nested_lam n' m
+  end.
+
+
+Lemma nest : forall n m : nat, nested_lam n m = n * m.
+intros n m.
+ functional induction nested_lam n m; simpl;auto.
+Qed.
+
+
+Function essai (x : nat) (p : nat * nat) {struct x} : nat :=
+  let (n, m) := (p: nat*nat) in
+  match n with
+  | O => 0
+  | S q => match x with
+           | O => 1
+           | S r => S (essai r (q, m))
+           end
+  end.
+
+Lemma essai_essai :
+ forall (x : nat) (p : nat * nat), let (n, m) := p in 0 < n -> 0 < essai x p.
+intros x p.
+ functional induction essai x p; intros.
+inversion H.
+auto with arith.
+ auto with arith.
+Qed.
+
+Function plus_x_not_five'' (n m : nat) {struct n} : nat :=
+  let x := nat_equal_bool m 5 in
+  let y := 0 in
+  match n with
+  | O => y
+  | S q =>
+      let recapp := plus_x_not_five'' q m in
+      match x with
+      | true => S recapp
+      | false => S recapp
+      end
+  end.
+
+Lemma notplusfive'' : forall x y : nat, y = 5 -> plus_x_not_five'' x y = x.
+intros a b.
+ functional induction plus_x_not_five'' a b; intros hyp; simpl; auto.
+Qed.
+
+Lemma iseq_eq : forall n m : nat, n = m -> nat_equal_bool n m = true.
+intros n m.
+ functional induction nat_equal_bool n m; simpl; intros hyp; auto.
+rewrite <- hyp in y; simpl in y;tauto.
+inversion hyp.
+Qed.
+
+Lemma iseq_eq' : forall n m : nat, nat_equal_bool n m = true -> n = m.
+intros n m.
+ functional induction nat_equal_bool n m; simpl; intros eg; auto.
+inversion eg.
+inversion eg.
+Qed.
+
+
+Inductive istrue : bool -> Prop :=
+    istrue0 : istrue true.
+
+Functional Scheme add_ind := Induction for add Sort Prop.
+
+Lemma inf_x_plusxy' : forall x y : nat, x <= x + y.
+intros n m.
+ functional induction add n m; intros.
+auto with arith.
+auto with arith.
+Qed.
+
+
+Lemma inf_x_plusxy'' : forall x : nat, x <= x + 0.
+intros n.
+unfold plus.
+ functional induction plus n 0; intros.
+auto with arith.
+apply le_n_S.
+assumption.
+Qed.
+
+Lemma inf_x_plusxy''' : forall x : nat, x <= 0 + x.
+intros n.
+ functional induction plus 0 n; intros; auto with arith.
+Qed.
+
+Function mod2 (n : nat) : nat :=
+  match n with
+  | O => 0
+  | S (S m) => S (mod2 m)
+  | _ => 0
+  end.
+
+Lemma princ_mod2 : forall n : nat, mod2 n <= n.
+intros n.
+ functional induction mod2 n; simpl; auto with arith.
+Qed.
+
+Function isfour (n : nat) : bool :=
+  match n with
+  | S (S (S (S O))) => true
+  | _ => false
+  end.
+
+Function isononeorfour (n : nat) : bool :=
+  match n with
+  | S O => true
+  | S (S (S (S O))) => true
+  | _ => false
+  end.
+
+Lemma toto'' : forall n : nat, istrue (isfour n) -> istrue (isononeorfour n).
+intros n.
+ functional induction isononeorfour n; intros istr; simpl;
+ inversion istr.
+apply istrue0.
+destruct n. inversion istr.
+destruct n. tauto.
+destruct n. inversion istr.
+destruct n. inversion istr.
+destruct n. tauto.
+simpl in *. inversion H0.
+Qed.
+
+Lemma toto' : forall n m : nat, n = 4 -> istrue (isononeorfour n).
+intros n.
+ functional induction isononeorfour n; intros m istr; inversion istr.
+apply istrue0.
+rewrite H in y; simpl in y;tauto.
+Qed.
+
+Function ftest4 (n m : nat) : nat :=
+  match n with
+  | O => match m with
+         | O => 0
+         | S q => 1
+         end
+  | S p => match m with
+           | O => 0
+           | S r => 1
+           end
+  end.
+
+Lemma test4 : forall n m : nat, ftest n m <= 2.
+intros n m.
+ functional induction ftest n m; auto with arith.
+Qed.
+
+Lemma test4' : forall n m : nat, ftest4 (S n) m <= 2.
+intros n m.
+assert ({n0 | n0 = S n}).
+exists (S n);reflexivity.
+destruct H as [n0 H1].
+rewrite <- H1;revert H1.
+ functional induction ftest4 n0 m.
+inversion 1.
+inversion 1.
+
+auto with arith.
+auto with arith.
+Qed.
+
+Function ftest44 (x : nat * nat) (n m : nat) : nat :=
+  let (p, q) := (x: nat*nat) in
+  match n with
+  | O => match m with
+         | O => 0
+         | S q => 1
+         end
+  | S p => match m with
+           | O => 0
+           | S r => 1
+           end
+  end.
+
+Lemma test44 :
+ forall (pq : nat * nat) (n m o r s : nat), ftest44 pq n (S m) <= 2.
+intros pq n m o r s.
+ functional induction ftest44 pq n (S m).
+auto with arith.
+auto with arith.
+auto with arith.
+auto with arith.
+Qed.
+
+Function ftest2 (n m : nat) {struct n} : nat :=
+  match n with
+  | O => match m with
+         | O => 0
+         | S q => 0
+         end
+  | S p => ftest2 p m
+  end.
+
+Lemma test2' : forall n m : nat, ftest2 n m <= 2.
+intros n m.
+ functional induction ftest2 n m; simpl; intros; auto.
+Qed.
+
+Function ftest3 (n m : nat) {struct n} : nat :=
+  match n with
+  | O => 0
+  | S p => match m with
+           | O => ftest3 p 0
+           | S r => 0
+           end
+  end.
+
+Lemma test3' : forall n m : nat, ftest3 n m <= 2.
+intros n m.
+ functional induction ftest3 n m.
+intros.
+auto.
+intros.
+auto.
+intros.
+simpl.
+auto.
+Qed.
+
+Function ftest5 (n m : nat) {struct n} : nat :=
+  match n with
+  | O => 0
+  | S p => match m with
+           | O => ftest5 p 0
+           | S r => ftest5 p r
+           end
+  end.
+
+Lemma test5 : forall n m : nat, ftest5 n m <= 2.
+intros n m.
+ functional induction ftest5 n m.
+intros.
+auto.
+intros.
+auto.
+intros.
+simpl.
+auto.
+Qed.
+
+Function ftest7 (n : nat) : nat :=
+  match ftest5 n 0 with
+  | O => 0
+  | S r => 0
+  end.
+
+Lemma essai7 :
+ forall (Hrec : forall n : nat, ftest5 n 0 = 0 -> ftest7 n <= 2)
+   (Hrec0 : forall n r : nat, ftest5 n 0 = S r -> ftest7 n <= 2)
+   (n : nat), ftest7 n <= 2.
+intros hyp1 hyp2 n.
+ functional induction ftest7 n; auto.
+Qed.
+
+Function ftest6 (n m : nat) {struct n} : nat :=
+  match n with
+  | O => 0
+  | S p => match ftest5 p 0 with
+           | O => ftest6 p 0
+           | S r => ftest6 p r
+           end
+  end.
+
+
+Lemma princ6 :
+ (forall n m : nat, n = 0 -> ftest6 0 m <= 2) ->
+ (forall n m p : nat,
+  ftest6 p 0 <= 2 -> ftest5 p 0 = 0 -> n = S p -> ftest6 (S p) m <= 2) ->
+ (forall n m p r : nat,
+  ftest6 p r <= 2 -> ftest5 p 0 = S r -> n = S p -> ftest6 (S p) m <= 2) ->
+ forall x y : nat, ftest6 x y <= 2.
+intros hyp1 hyp2 hyp3 n m.
+generalize hyp1 hyp2 hyp3.
+clear hyp1 hyp2 hyp3.
+ functional induction ftest6 n m; auto.
+Qed.
+
+Lemma essai6 : forall n m : nat, ftest6 n m <= 2.
+intros n m.
+ functional induction ftest6 n m; simpl; auto.
+Qed.
+
+(* Some tests with modules *)
+Module M.
+Function test_m (n:nat) : nat :=
+  match n with
+    | 0 => 0
+    | S n =>  S (S (test_m n))
+  end.
+
+Lemma test_m_is_double :  forall n, div2 (test_m n) = n.
+Proof.
+intros n.
+functional induction (test_m n).
+reflexivity.
+simpl;rewrite IHn0;reflexivity.
+Qed.
+End M.
+(* We redefine a new Function with the same name *)
+Function test_m (n:nat) : nat :=
+  pred n.
+
+Lemma test_m_is_pred : forall n, test_m n = pred n.
+Proof.
+intro n.
+functional induction (test_m n). (* the test_m_ind to use is the last defined  saying that test_m = pred*)
+reflexivity.
+Qed.
+
+(* Checks if the dot notation are correctly treated in infos *)
+Lemma M_test_m_is_double : forall n, div2 (M.test_m n) = n.
+intro n.
+(* here we should apply M.test_m_ind *)
+functional induction (M.test_m n).
+reflexivity.
+simpl;rewrite IHn0;reflexivity.
+Qed.
+
+Import M.
+(* Now test_m is the one which defines double *)
+
+Lemma test_m_is_double : forall n, div2 (M.test_m n) = n.
+intro n.
+(* here we should apply M.test_m_ind *)
+functional induction (test_m n).
+reflexivity.
+simpl;rewrite IHn0;reflexivity.
+Qed.
+
+Extraction iszero.
diff --git a/test-suite/success/ROmega3.v b/test-suite/success/ROmega3.v
new file mode 100644
index 0000000000..fd4ff260b5
--- /dev/null
+++ b/test-suite/success/ROmega3.v
@@ -0,0 +1,31 @@
+
+Require Import ZArith ROmega.
+Local Open Scope Z_scope.
+
+(** Benchmark provided by Chantal Keller, that romega used to
+    solve far too slowly (compared to omega or lia). *)
+
+Parameter v4 : Z.
+Parameter v3 : Z.
+Parameter o4 : Z.
+Parameter s5 : Z.
+Parameter v2 : Z.
+Parameter o5 : Z.
+Parameter s6 : Z.
+Parameter v1 : Z.
+Parameter o6 : Z.
+Parameter s7 : Z.
+Parameter v0 : Z.
+Parameter o7 : Z.
+
+Lemma lemma_5833 :
+ ~ 16 * v4 + (8 * v3 + (-8192 * o4 + (-4096 * s5 + (4 * v2 +
+      (-4096 * o5 + (-2048 * s6 + (2 * v1 + (-2048 * o6 +
+         (-1024 * s7 + (v0 + -1024 * o7)))))))))) >= 8192
+\/
+  16 * v4 + (8 * v3 + (-8192 * o4 + (-4096 * s5 + (4 * v2 +
+      (-4096 * o5 + (-2048 * s6 + (2 * v1 + (-2048 * o6 +
+         (-1024 * s7 + (v0 + -1024 * o7)))))))))) >= 1024.
+Proof.
+Timeout 1 romega. (* should take a few milliseconds, not seconds *)
+Timeout 1 Qed. (* ditto *)
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index d8f8042465..8419404925 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -147,6 +147,7 @@ Proof.
  intros; absurd (p < p); eauto with arith.
 Qed.
 
+Require Coq.extraction.Extraction.
 Extraction max.
 
 
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
new file mode 100644
index 0000000000..ebf817cfc5
--- /dev/null
+++ b/test-suite/success/cumulativity.v
@@ -0,0 +1,65 @@
+Set Universe Polymorphism.
+Set Inductive Cumulativity.
+Set Printing Universes.
+
+Inductive List (A: Type) := nil | cons : A -> List A -> List A.
+
+Section ListLift.
+  Universe i j.
+
+  Constraint i < j.
+
+  Definition LiftL {A} : List@{i} A -> List@{j} A := fun x => x.
+
+End ListLift.
+
+Lemma LiftL_Lem A (l : List A) : l = LiftL l.
+Proof. reflexivity. Qed.
+
+Section ListLower.
+  Universe i j.
+
+  Constraint i < j.
+
+  Definition LowerL {A : Type@{i}} : List@{j} A -> List@{i} A := fun x => x.
+
+End ListLower.
+
+Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l.
+Proof. reflexivity. Qed.
+
+Inductive Tp := tp : Type -> Tp.
+
+Section TpLift.
+  Universe i j.
+
+  Constraint i < j.
+
+  Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x.
+
+End TpLift.
+
+Lemma LiftC_Lem (t : Tp) : LiftTp t = t.
+Proof. reflexivity. Qed.
+
+Section TpLower.
+  Universe i j.
+
+  Constraint i < j.
+
+  Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x.
+
+End TpLower.
+
+
+Section subtyping_test.
+  Universe i j.
+  Constraint i < j.
+
+  Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2.
+
+End subtyping_test.
+
+Record A : Type := { a :> Type; }.
+
+Record B (X : A) : Type := { b : X; }.
\ No newline at end of file
diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v
index 0086e090bd..89be144152 100644
--- a/test-suite/success/extraction.v
+++ b/test-suite/success/extraction.v
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+Require Coq.extraction.Extraction.
 Require Import Arith.
 Require Import List.
 
diff --git a/test-suite/success/extraction_dep.v b/test-suite/success/extraction_dep.v
index 11bb25fda0..e770cf779a 100644
--- a/test-suite/success/extraction_dep.v
+++ b/test-suite/success/extraction_dep.v
@@ -1,6 +1,8 @@
 
 (** Examples of code elimination inside modules during extraction *)
 
+Require Coq.extraction.Extraction.
+
 (** NB: we should someday check the produced code instead of
     simply running the commands. *)
 
diff --git a/test-suite/success/extraction_impl.v b/test-suite/success/extraction_impl.v
index dfdeff82ff..5bf807b1c6 100644
--- a/test-suite/success/extraction_impl.v
+++ b/test-suite/success/extraction_impl.v
@@ -4,6 +4,8 @@
 (** NB: we should someday check the produced code instead of
     simply running the commands. *)
 
+Require Coq.extraction.Extraction.
+
 (** Bug #4243, part 1 *)
 
 Inductive dnat : nat -> Type :=
diff --git a/test-suite/success/extraction_polyprop.v b/test-suite/success/extraction_polyprop.v
index 7215bd9905..936d838c50 100644
--- a/test-suite/success/extraction_polyprop.v
+++ b/test-suite/success/extraction_polyprop.v
@@ -3,6 +3,8 @@
    code that segfaults. See Table.error_singleton_become_prop
    or S. Glondu's thesis for more details. *)
 
+Require Coq.extraction.Extraction.
+
 Definition f {X} (p : (nat -> X) * True) : X * nat :=
   (fst p 0, 0).
 
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 66ff55edcb..ecc988507c 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -352,3 +352,35 @@ Module Anonymous.
   Check collapsethemiddle@{_ _}.
 
 End Anonymous.
+
+Module F.
+  Context {A B : Type}.
+  Definition foo : Type := B.
+End F.
+
+Set Universe Polymorphism.
+
+Cumulative Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }.
+
+Section test_letin_subtyping.
+  Universe i j k i' j' k'.
+  Constraint j < j'.
+
+  Context (W : Type) (X : box@{i j k} W).
+  Definition Y := X : box@{i' j' k'} W.
+
+  Universe i1 j1 k1 i2 j2 k2.
+  Constraint i1 < i2.
+  Constraint k2 < k1.
+  Context (V : Type).
+
+  Definition Z : box@{i1 j1 k1} V := {| unwrap := V |}.
+  Definition Z' : box@{i2 j2 k2} V := {| unwrap := V |}.
+  Lemma ZZ' : @eq (box@{i2 j2 k2} V) Z Z'.
+  Proof.
+    Set Printing All. Set Printing Universes.
+    cbv.
+    reflexivity.
+  Qed.
+
+End test_letin_subtyping.
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 2fa7704941..789854b2d6 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -181,6 +181,8 @@ Record wrap (A : Type) := { unwrap : A; unwrap2 : A }.
 
 Definition term (x : wrap nat) := x.(unwrap).
 Definition term' (x : wrap nat) := let f := (@unwrap2 nat) in f x.
+
+Require Coq.extraction.Extraction.
 Recursive Extraction term term'.
 (*Unset Printing Primitive Projection Parameters.*)