Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh

42 files changed, 1063 insertions, 55 deletions

diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v
index ce9050d421..3c696502cd 100644
--- a/test-suite/success/Case22.v
+++ b/test-suite/success/Case22.v
@@ -17,3 +17,47 @@ Definition foo (x : I') : bool :=
   match x with
   C' => true
   end.
+
+(* Bug found in november 2015: was wrongly failing in 8.5beta2 and 8.5beta3 *)
+
+Inductive I2 (A:Type) : let B:=A in forall C, let D:=(C*B)%type in Type :=
+  E2 : I2 A nat.
+
+Check fun x:I2 nat nat => match x in I2 _ X Y Z return X*Y*Z with
+  E2 _ => (0,0,(0,0))
+  end.
+
+(* This used to succeed in 8.3, 8.4 and 8.5beta1 *)
+
+Inductive IND : forall X:Type, let Y:=X in Type :=
+  CONSTR : IND True.
+
+Definition F (x:IND True) (A:Type) :=
+  (* This failed in 8.5beta2 though it should have been accepted *)
+  match x in IND X Y return Y with
+  CONSTR => Logic.I
+  end.
+
+Theorem paradox : False.
+  (* This succeeded in 8.3, 8.4 and 8.5beta1 because F had wrong type *)
+Fail Proof (F C False).
+
+(* Another bug found in November 2015 (a substitution was wrongly
+   reversed at pretyping level) *)
+
+Inductive Ind (A:Type) :
+  let X:=A in forall Y:Type, let Z:=(X*Y)%type in Type :=
+  Constr : Ind A nat.
+
+Check fun x:Ind bool nat =>
+  match x in Ind _ X Y Z return Z with
+  | Constr _ => (true,0)
+  end.
+
+(* A vm_compute bug (the type of constructors was not supposed to
+   contain local definitions before proper parameters) *)
+
+Inductive Ind2 (b:=1) (c:nat) : Type :=
+  Constr2 : Ind2 c.
+
+Eval vm_compute in Constr2 2.
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index e42663505d..49c465b6c6 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -1861,3 +1861,10 @@ Type (fun n => match n with
 
 Definition transport {A} (P : A->Type) {x y : A} (p : x=y) (u : P x) : P y :=
   match p with eq_refl => u end.
+
+(* Check in-pattern clauses with constant constructors, which were
+   previously interpreted as variables (before 8.5) *)
+
+Check match eq_refl 0 in _=O return O=O with eq_refl => eq_refl end.
+
+Check match niln in listn O return O=O with niln => eq_refl end.
diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v
index 87c38cfa06..e4ee351c3a 100644
--- a/test-suite/success/Check.v
+++ b/test-suite/success/Check.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/Compat84.v b/test-suite/success/Compat84.v
new file mode 100644
index 0000000000..db6348fa17
--- /dev/null
+++ b/test-suite/success/Compat84.v
@@ -0,0 +1,19 @@
+(* -*- coq-prog-args: ("-emacs" "-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/Field.v b/test-suite/success/Field.v
index 8db08b6d78..438e461357 100644
--- a/test-suite/success/Field.v
+++ b/test-suite/success/Field.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index cc8cec4707..f934a5c74a 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -62,3 +62,47 @@ Axiom cast_coalesce :
   ((e :? pf1) :? pf2) = (e :? trans_eq pf1 pf2).
 
 Hint Rewrite cast_coalesce : ltamer.
+
+Require Import Program.
+Module HintCut.
+Class A (f : nat -> nat) := a : True.
+Class B (f : nat -> nat) := b : True.
+Class C (f : nat -> nat) := c : True.
+Class D (f : nat -> nat) := d : True.
+Class E (f : nat -> nat) := e : True.
+
+Instance a_is_b f : A f -> B f.
+Proof. easy. Qed.
+Instance b_is_c f : B f -> C f.
+Proof. easy. Qed.
+Instance c_is_d f : C f -> D f.
+Proof. easy. Qed.
+Instance d_is_e f : D f -> E f.
+Proof. easy. Qed.
+
+Instance a_compose f g : A f -> A g -> A (compose f g).
+Proof. easy. Qed.
+Instance b_compose f g : B f -> B g -> B (compose f g).
+Proof. easy. Qed.
+Instance c_compose f g : C f -> C g -> C (compose f g).
+Proof. easy. Qed.
+Instance d_compose f g : D f -> D g -> D (compose f g).
+Proof. easy. Qed.
+Instance e_compose f g : E f -> E g -> E (compose f g).
+Proof. easy. Qed.
+
+Instance a_id : A id.
+Proof. easy. Qed.
+
+Instance foo f :
+  E (id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘
+     id ∘ id ∘ id ∘ id ∘ id ∘ f ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id).
+Proof.
+  Fail Timeout 1 apply _. (* 3.7s *)
+  
+Hint Cut [!*; (a_is_b | b_is_c | c_is_d | d_is_e) ;
+  (a_compose | b_compose | c_compose | d_compose | e_compose)] : typeclass_instances.
+
+  Timeout 1 Fail apply _. (* 0.06s *)
+Abort.
+End HintCut.
\ No newline at end of file
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index 25e464d677..56ed89ed86 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -68,6 +68,12 @@ einjection (H O).
 instantiate (1:=O).
 Abort.
 
+Goal (forall x y : nat, x = y -> S x = S y) -> True.
+intros.
+einjection (H O ?[y]) as H0.
+instantiate (y:=O).
+Abort.
+
 (* Test the injection intropattern *)
 
 Goal forall (a b:nat) l l', cons a l = cons b l' -> a=b.
diff --git a/test-suite/success/MatchFail.v b/test-suite/success/MatchFail.v
index 7069bba430..8462d36272 100644
--- a/test-suite/success/MatchFail.v
+++ b/test-suite/success/MatchFail.v
@@ -9,14 +9,14 @@ Require Export ZArithRing.
 Ltac compute_POS :=
   match goal with
   |  |- context [(Zpos (xI ?X1))] =>
-      let v := constr:X1 in
-      match constr:v with
+      let v := constr:(X1) in
+      match constr:(v) with
       | 1%positive => fail 1
       | _ =>  rewrite (BinInt.Pos2Z.inj_xI v)
       end
   |  |- context [(Zpos (xO ?X1))] =>
-      let v := constr:X1 in
-      match constr:v with
+      let v := constr:(X1) in
+      match constr:(v) with
       | 1%positive => fail 1
       | _ =>  rewrite (BinInt.Pos2Z.inj_xO v)
       end
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 2371d32cda..b72a067407 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -101,3 +101,9 @@ Fail Check fun x => match x with S (FORALL x, _) => 0 end.
 
 Parameter traverse : (nat -> unit) -> (nat -> unit).
 Notation traverse_var f l := (traverse (fun l => f l) l).
+
+(* Check that when an ident become a keyword, it does not break
+   previous rules relying on the string to be classified as an ident *)
+
+Notation "'intros' x" := (S x) (at level 0).
+Goal True -> True. intros H. exact H. Qed.
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
new file mode 100644
index 0000000000..9505a56e3f
--- /dev/null
+++ b/test-suite/success/Notations2.v
@@ -0,0 +1,92 @@
+(* This file is giving some examples about how implicit arguments and
+   scopes are treated when using abbreviations or notations, in terms
+   or patterns, or when using @ and parentheses in terms and patterns.
+
+The convention is:
+
+Constant foo with implicit arguments and scopes used in a term or a pattern:
+
+       foo      do not deactivate further arguments and scopes
+       @foo     deactivates further arguments and scopes
+       (foo x)  deactivates further arguments and scopes
+       (@foo x) deactivates further arguments and scopes
+
+Notations binding to foo:
+
+#   := foo      do not deactivate further arguments and scopes
+#   := @foo     deactivates further arguments and scopes
+# x := foo x    deactivates further arguments and scopes
+# x := @foo x   deactivates further arguments and scopes
+
+Abbreviations binding to foo:
+
+f   := foo      do not deactivate further arguments and scopes
+f   := @foo     deactivates further arguments and scopes
+f x := foo x    do not deactivate further arguments and scopes
+f x := @foo x   do not deactivate further arguments and scopes
+*)
+
+(* One checks that abbreviations and notations in patterns now behave like in terms *)
+
+Inductive prod' A : Type -> Type :=
+| pair' (a:A) B (b:B) (c:bool) : prod' A B.
+Arguments pair' [A] a%bool_scope [B] b%bool_scope c%bool_scope.
+Notation "0" := true : bool_scope.
+
+(* 1. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *)
+Notation c1 x := (pair' x).
+Check pair' 0 0 0 : prod' bool bool.
+Check (pair' 0) _ 0%bool 0%bool : prod' bool bool. (* parentheses are blocking implicit and scopes *)
+Check c1 0 0 0 : prod' bool bool.
+Check fun x : prod' bool bool => match x with c1 0 y 0 => 2 | _ => 1 end.
+
+(* 2. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *)
+Notation c2 x := (@pair' _ x).
+Check (@pair' _ 0) _ 0%bool 0%bool : prod' bool bool. (* parentheses are blocking implicit and scopes *)
+Check c2 0 0 0 : prod' bool bool.
+Check fun A (x : prod' bool A) => match x with c2 0 y 0 => 2 | _ => 1 end.
+Check fun A (x : prod' bool A) => match x with (@pair' _ 0) _ y 0%bool => 2 | _ => 1 end.
+
+(* 3. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *)
+Notation c3 x := ((@pair') _ x).
+Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool. (* @ is blocking implicit and scopes *)
+Check ((@pair') _ 0%bool) _ 0%bool 0%bool : prod' bool bool. (* parentheses and @ are blocking implicit and scopes *)
+Check c3 0 0 0 : prod' nat bool. (* First scope is blocked but not the last two scopes *)
+Check fun A (x :prod' nat A) => match x with c3 0 y 0 => 2 | _ => 1 end.
+
+(* 4. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *)
+(* unless an atomic @ is given *)
+Notation c4 := (@pair').
+Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool.
+Check c4 _ 0%bool _ 0%bool 0%bool : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with c4 _ 0%bool _ y 0%bool => 2 | _ => 1 end.
+Check fun A (x :prod' bool A) => match x with (@pair') _ 0%bool _ y 0%bool => 2 | _ => 1 end.
+
+(* 5. Notations stop further implicit arguments to be inserted and scopes to be used *)
+Notation "# x" := (pair' x) (at level 0, x at level 1).
+Check pair' 0 0 0 : prod' bool bool.
+Check # 0 _ 0%bool 0%bool : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with # 0 _ y 0%bool => 2 | _ => 1 end.
+
+(* 6. Notations stop further implicit arguments to be inserted and scopes to be used *)
+Notation "## x" := ((@pair') _ x) (at level 0, x at level 1).
+Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool.
+Check ((@pair') _ 0%bool) _ 0%bool 0%bool : prod' bool bool.
+Check ## 0%bool _ 0%bool 0%bool : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with ## 0%bool _ y 0%bool => 2 | _ => 1 end.
+
+(* 7. Notations stop further implicit arguments to be inserted and scopes to be used *)
+Notation "###" := (@pair') (at level 0).
+Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool.
+Check ### _ 0%bool _ 0%bool 0%bool : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with ### _ 0%bool _ y 0%bool => 2 | _ => 1 end.
+
+(* 8. Notations w/o @ preserves implicit arguments and scopes *)
+Notation "####" := pair' (at level 0).
+Check #### 0 0 0 : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with #### 0 y 0 => 2 | _ => 1 end.
+
+(* 9. Notations w/o @ but arguments do not preserve further implicit arguments and scopes *)
+Notation "##### x" := (pair' x) (at level 0, x at level 1).
+Check ##### 0 _ 0%bool 0%bool : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end.
diff --git a/test-suite/success/TacticNotation2.v b/test-suite/success/TacticNotation2.v
new file mode 100644
index 0000000000..cb341b8e10
--- /dev/null
+++ b/test-suite/success/TacticNotation2.v
@@ -0,0 +1,12 @@
+Tactic Notation "complete" tactic(tac) := tac; fail.
+
+Ltac f0 := complete (intuition idtac).
+(** FIXME: This is badly printed because of bug #3079.
+    At least we check that it does not fail anomalously. *)
+Print Ltac f0.
+
+Ltac f1 := complete f1.
+Print Ltac f1.
+
+Ltac f2 := complete intuition.
+Print Ltac f2.
diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v
index 01d9afb426..767f15be72 100644
--- a/test-suite/success/Tauto.v
+++ b/test-suite/success/Tauto.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v
index 3090f40cde..c8a8b862fa 100644
--- a/test-suite/success/TestRefine.v
+++ b/test-suite/success/TestRefine.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 55b666b723..02e043bc36 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -543,7 +543,7 @@ Qed.
 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.
+intros; eexists; eexists ?[y]; case H.
 apply (foo ?y).
 Grab Existential Variables.
 exact 0.
diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v
index db3b19af51..5477c83316 100644
--- a/test-suite/success/auto.v
+++ b/test-suite/success/auto.v
@@ -1,6 +1,6 @@
 (* Wish #2154 by E. van der Weegen *)
 
-(* auto was not using f_equal-style lemmas with metavariables occuring
+(* auto was not using f_equal-style lemmas with metavariables occurring
    only in the type of an evar of the concl, but not directly in the
    concl itself *)
 
@@ -45,3 +45,92 @@ Proof.
   eexists. Fail progress debug eauto with test2. 
   progress eauto with test.
 Qed.
+
+(** Patterns of Extern have a "matching" semantics.
+    It is not so for apply/exact hints *)
+
+Class B (A : Type).
+Class I. 
+Instance i : I.
+  
+Definition flip {A B C : Type} (f : A -> B -> C) := fun y x => f x y.
+Class D (f : nat -> nat -> nat).
+Definition ftest (x y : nat) := x + y.
+Definition flipD (f : nat -> nat -> nat) : D f -> D (flip f).
+  Admitted.
+Module Instnopat.
+  Local Instance: B nat.
+  (* pattern_of_constr -> B nat *)
+  (* exact hint *)
+  Check (_ : B nat).
+  (* map_eauto -> B_instance0 *)
+  (* NO Constr_matching.matches !!! *)
+  Check (_ : B _).
+
+  Goal exists T, B T.
+    eexists.
+    eauto with typeclass_instances.
+  Qed.
+
+  Local Instance: D ftest.
+  Local Hint Resolve flipD | 0 : typeclass_instances.
+  (* pattern: D (flip _) *)
+  Fail Timeout 1 Check (_ : D _). (* loops applying flipD *)  
+  
+End Instnopat.
+
+Module InstnopatApply.
+  Local Instance: I -> B nat.
+  (* pattern_of_constr -> B nat *)
+  (* apply hint  *)
+  Check (_ : B nat).
+  (* map_eauto -> B_instance0 *)
+  (* NO Constr_matching.matches !!! *)
+  Check (_ : B _).
+
+  Goal exists T, B T.
+    eexists.
+    eauto with typeclass_instances.
+  Qed.
+End InstnopatApply.
+  
+Module InstPat.
+  Hint Extern 3 (B nat) => split : typeclass_instances.
+  (* map_eauto -> Extern hint *)
+  (* Constr_matching.matches -> true *)
+  Check (_ : B nat).
+  (* map_eauto -> Extern hint *)
+  (* Constr_matching.matches -> false:
+     Because an inductive in the pattern does not match an evar in the goal *)
+  Check (_ : B _).
+
+  Goal exists T, B T.
+    eexists.
+    (* map_existential -> Extern hint *)
+    (* Constr_matching.matches -> false *)
+    Fail progress eauto with typeclass_instances.
+    (* map_eauto -> Extern hint *)
+    (* Constr_matching.matches -> false *)
+    Fail typeclasses eauto.
+  Abort.
+
+  Hint Extern 0 (D (flip _)) => apply flipD : typeclass_instances.
+  Module withftest.
+    Local Instance: D ftest.
+
+    Check (_ : D _).
+    (* D_instance_0 : D ftest *)
+    Check (_ : D (flip _)).
+    (* ... : D (flip ftest) *)
+  End withftest.
+  Module withoutftest.
+    Hint Extern 0 (D ftest) => split : typeclass_instances.
+    Check (_ : D _).
+    (* ? : D ?, _not_ looping *)
+    Check (_ : D (flip _)).
+    (* ? : D (flip ?), _not_ looping *)
+
+    Check (_ : D (flip ftest)).
+    (* flipD ftest {|  |} : D (flip ftest) *)
+  End withoutftest.
+End InstPat.
diff --git a/test-suite/success/bigQ.v b/test-suite/success/bigQ.v
new file mode 100644
index 0000000000..7fd0cf669d
--- /dev/null
+++ b/test-suite/success/bigQ.v
@@ -0,0 +1,66 @@
+Require Import BigQ.
+Import List.
+
+Definition pi_4_approx_low' := 
+(5066193963420194617885108698600649932059391557720145469382602092416947640628637390992675949693715109726079394291478795603894419483819297806310615866892414925850691415582239745615128821983865262221858109336884967754871321668348027076234335167119885298878199925731495390387858629042311908406056230882123787019283378509712244687397013657159455607193734144010901984756727174636853404278421831024545476850410085042498464474261035780891759930905778986584183710930670670301831474144997069400304290351567959717683444430666444319233768399342338059169002790777424962570605618705584660815518973602995097110557181643034682308210782171804373210646804613922337450953858508244032293753591878060539465788294318856859293281629951093130167801471787011911886414492513677892193100809508943832528344473873460853362957387889412799458784754514139679847887887544849825173792522272708046699681079289358082661375778523609867456540595586031625044964543428047238934233579184772793670436643502740076366994465457847106782560289782615794595755672643440040123002018908935362541166831619056664637901929131328502017686713274283777724453661234225382109584471950444925886358166551424008707439387934109226545596919797083495958300914344992836193126080289565652575543234385558967555959267746932292860747199382633363026440008828134867747920263181610216905129926037611247017868033961426567047355301676870662406173724238530061264149506666345040372864118731705584795947926329181826992456072045382170981478151356381437136818835196834068650217794381425547036331194595892801393225038235274901050364737353586927051766717037643833477566087835266968086513005761986678747515870298138062157791066648217784877968385924845017637219384732843791052551854695220023477365706464590594542001161575677402761543188277502092362285265847964496740584911576627239093631932307473445797386335961743298553548881544486940399236133577915988716682746485564575640818803540680574730591500432326858763829791848612343662539095316357052823005419355719381626599487868023399182174939253393897549026675976384326749445831606130546375395770778462506203752920470130305293966478109733954117063941901686840180727195741528561335809865193566993349413786715403053579411364371500063193205131503024022217701373077790337150298315820556080596579100618643147698304927957576213733526923182742441048553793831725592624850721293495085399785588171300815789795594858916409701139277050529011775828846362873246196866089783324522718656445008090114701320562608474099248873638488023114015981013142490827777895317580810590743940417298263300561876701828404744082864248409230009391001735746615476377303707782123483770118391136826609366946585715225248587168403619476143657107412319421501162805102723455593551478028055839072686207007765300258935153546418515706362733656094770289090398825190320430416955807878686642673124733998295439657633866090085982598765253268688814792672416195730086607425842181518560588819896560847103627615434844684536463752986969865794019299978956052589825441828842338163389851892617560591840546654410705167593310272272965900821031821380595084783691324416454359888103920904935692840264474003367023256964191100139001239923263691779167792867186165635514824889759796850863175082506408142175595463676408992027105356481220754473245821534527625758942093801142305560662681150069082553674495761075895588095760081401141419460482860852822686860785424514171214889677926763812031823537071721974799922995763666175738785000806081164280471363125324839717808977470218218571800106898347366938927189989988149888641129263448064762730769285877330997355234347773807099829665997515649429224335217107760728789764718885665291038706425454675746218345291274054088843647602239258308472486102933167465443294268551209015027897159307743987020521392788721231001835675584104894174434637260464035122611721657641428625505184886116917149318963070896162119215386541876236027342810162765609201440423207771441367926085768438143507025739041041240810056881304230519058117534418374553879198061289605354335880794397478047346975609179199801003098836622253165101961484972165230151495472006888128587168049198312469715081555662345452800468933420359802645393289853553618279788400476187713990872203669487294118461245455333004125835663010526985716431187034663870796866708678078952110615910196519835267441831874676895301527286826106517027821074816850326548617513767142627360001181210946100011774672126943957522004190414960909074050454565964857276407084991922274068961845339154089866785707764290964299529444616711194034827611771558783466230353209661849406004241580029437779784290315347968833708422223285859451369907260780956405036020581705441364379616715041818815829810906212826084485200785283123265202151252852134381195424724503189247411069117189489985791487434549080447866370484866697404176437230771558469231403088139693477706784802801265075586678597768511791952562627345622499328
+        # 100788726492580594349650258277496659410917619472657560321971265983799894639441017438166498752997098978003489632843381325240982516059309714013145358125224597827602157516585886911710102182473475545864474089191789296685473601331678556438310133356793199956062857423397512495293688453655805536015029176541424005214818033707522950635262669828538132795615008381824067071229426026518897202246241637377064076189277685257166926338187911595052586669184297526234794666364657344206795357967279911782849686515024121916258300642000317525374433525235296287037535618423661645124459323811792936193272341688261801253469089129439519903538495370298752436267926761998785090092411372633429302950606054074205533246665546979112178855223925266166034953000200646676762301817000435641690517142795144469005596172113586738287118865058604922865654348297975054956781513943444060257230946224520058527667925776273088622386666860662470481606622952298649177217986593047495967209669116410592230626047083795555559776477430548946990993890380787911273437967786556742804566652408275798339221179283430482118140020742719695900657696142739101628984271513292954605191778803974738871043737934546460016184719168074062912083778327025499841998124431899131874519812228674255796948879306477894924710085384116453080236862135706628989104070747737689294987000148388110561753028594988959655591699155508380909698460304884908709246116411180876105681720036833487450945730831039969246996849503525429840196651386469599438064049723005123629385485140945945416764414133189625489032807860400751723995946290581976152580477047961138617997133510128194027510895265424780627975864980749945631413855375897945293107842908479797077570371447220506451229526132919408351287454305932886749170523056147842439813407002950370505941417426433452282518739345666494683448699945734453214481915512562995906034771246088038719298959180199052759295868161570318718927430655393250250811804905393113074074574608255523847592006804881016594060188745212933427473833239777228852952217878690668413947367586040297784502192683200664398064682201012931468052982448022330449955215606614483165425935154496289535573901139223034819824408001205784146243892228030383941863746839845526558421740316887532141893650230936137269356278754487130882868595412163277284772124736531380334814212708066069618080153747333573454834500999083737284449542481264971030785043701582134343596645346132964567391370300568578875509971483039720438955919863275044932311289587494336123538202079503922025306586828117649623642521324286648529829664567232756108169459356549144779085080036654897525078792273443307070502103724611233768453196294899770515940520895908289018412144327894912660060761908970811602375085884115384049610753387776858733798341463052471017393165656926510611173543365663267563198760597092606598728110197523695339144204179424646442294307593146446562536865057987897899655645968129515654148044008249646703504419478535298270862753806142083172190778193001810574370442181909146645889199829207284871551220439225371051511970054965951914399901815408791418836185742573331879114400013259342896515702942707292473805188905427717363630137869116872433627556880809120353079342030725196065815470427569172350436988386579444534375353968759750750178342190349607711313840613843718547859929387259163285524671855725511880656411741012446023392964655239624520090988149679656514996202498334816938716757663800773997302639681907686195671083505910700098597156238624351157219093280177066146218516478636356056420098245995113668018177690728654922707281126889313941750547830163078886329630807850633273613622550216189245162735650139455042125252043274668279981753287687674520319519360593091620297805736177366738063651905396783336064579717230286821545930579779462534206093794040878198825916141099864730374109311705285661056855668930671948265232862757146615431791375559792290479316263924560826544387396762768331402198937951439504767950821089741987629257538953417586416459087855138539304027013800937360598578194413362672871055543854633921502486683911956250444582746421552178164852341035733290405311280719066037175324627429434912416361334254696649419037348733709488576582107382055914938194078813926926742828297826939120316120573453588052056773875836843924877773978390546387248009519202370375478981843515393806263037580338009594022254079586380520797699651840576286033587273591899639699077044271208886940540056794360292760863657703246410020854088849880453524038877935317875884698324859548991680533307680053872403383516589028793015681082435908524045497475001609824047204954932626536311826911363867426654549346914317405110707189532251727848751560224936842128628673253616256326013555922159336370177663785738170802777550686079119049748734352584409583136667752555307842739679930698964098088960000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%bigQ
+.
+
+Definition pi_4_approx_high' := 
+(5066193963420194617885108698600649932059391557720145469382602092416947640628637390992675949693715109726079394291478795603894419483819297806310615866892414925850691415582239745615128821983865262221858109336884967754871321668348027076234335167119885298878199925731495390387858629042311908406056230882123787019283378509712244687397013657159455607193734144010901984756727174636853404278421831024545476850410085042498464474261035780891759930905778986584183710930670670301831474144997069400304290351567959717683444430666444319233768399342338059169002790777424962570605618705584660815518973602995097110557181643034682308210788409308322071457087096445676662503017187903223859814905546579050729173916234740628466315449085686468204847296426235788544874405450791749423436215032927889914519102361378633666267941326393265376660400091389373564825046526561381561278586121772300141564909333667988204680492088607706214346458601842899721615765319505314310192693665547163360402786722105590252780194994950097926184146718893770363322073641336811404180286358079915338791029818581497746089864894356686643882883410392601500048021013346713450539807687779704798018559373507951388092945938366448668853081682176581336156031434604604833692503597621519809826880683536141897075567053733515342478008373282599947520770191238802249392773327261328133194484586433840861730959791563023761306622956165536481335792721379318928171897265310054788931201902441066997927781894934061720760080768154565282051604447333036111267534150649674590201404453202347064545359869105856798745664471694795576801148562495225166002814304124970965817043547048503388910163287916513427409193998045119986267987892522931703487420953769290650229176116308194977201080691718825944370436642709192983358059711255925052564016519597530235976618244111239816418652282585432539731271068892992142956810775762851238126881225206289553948196520384709574383566733478326330112084307565420647201107231840508040019131253750047046446929758911912155202166566751947087545292626353331520202690130850009389387290465497377022080531269511355734944672010542204118978272180881335465227900174033380001851066811103401787656367819132934758616060307366679580043123632565656840669377840733018248707250548277181001911990237151790533341326223932843775840498222236867608395855700891719880219904948672458645420169533565809609056209006342663841718949396996175294237942265325043426430990062217643279654512512640557763489491751115437780462208361129433667449740743123546232162409802316714286708788831227582498585478334315076725145986771341647015244092760289407649044493584479944044779273447198382196766547779885914425854375158084417582279211000449529495605127376707776277159376010648950025135061284601443461110447113346277147728593420397807946636800365109579479211273476195727270004743568492888900356505584731622538401071221591141889158461271000051210318027818802379539544396973228585821742794928813630781709195703717312953337431290682263448669168179857644544116657440168099166467471736180072984407514757289757495435699300593165669101965987430482600019222913485092771346963058673132443387835726110205958057187517487684058179749952286341120230051432903482992282688283815697442898155194928723360957436110770317998431272108100149791425689283090777721270428030993332057319821685391144252815655146410678839177846108260765981523812232294638190350688210999605869296307711846463311346627138400477211801219366400312514793356564308532012682051019030257269068628100171220662165246389309014292764479226570049772046255291379151017129899157296574099437276707879597755725339406865738613810979022640265737120949077721294633786520294559343155148383011293584240192753971366644780434237846862975993387453786681995831719537733846579480995517357440575781962659282856696638992709756358478461648462532279323701121386551383509193782388241965285971965887701816406255233933761008649762854363984142178331798953040874526844255758512982810004271235810681505829473926495256537353108899526434200682024946218302499640511518360332022463196599199779172637638655415918976955930735312156870786600023896830267884391447789311101069654521354446521135407720085038662159974712373018912537116964809382149581004863115431780452188813210275393919111435118030412595133958954313836191108258769640843644195537185904547405641078708492098917460393911427237155683288565433183738513871595286090814836422982384810033331519971102974091067660369548406192526284519976668985518575216481570167748402860759832933071281814538397923687510782620605409323050353840034866296214149657376249634795555007199540807313397329050410326609108411299737760271566308288500400587417017113933243099961248847368789383209110747378488312550109911605079801570534271874115018095746872468910162721975463388518648962869080447866370484866697404176437230771558469231403088139693477706784802801265075586678597768511791952562627345622499328
+        # 100788726492580594349650258277496659410917619472657560321971265983799894639441017438166498752997098978003489632843381325240982516059309714013145358125224597827602157516585886911710102182473475545864474089191789296685473601331678556438310133356793199956062857423397512495293688453655805536015029176541424005214818033707522950635262669828538132795615008381824067071229426026518897202246241637377064076189277685257166926338187911595052586669184297526234794666364657344206795357967279911782849686515024121916258300642000317525374433525235296287037535618423661645124459323811792936193272341688261801253469089129439519903538495370298752436267926761998785090092411372633429302950606054074205533246665546979112178855223925266166034953000200646676762301817000435641690517142795144469005596172113586738287118865058604922865654348297975054956781513943444060257230946224520058527667925776273088622386666860662470481606622952298649177217986593047495967209669116410592230626047083795555559776477430548946990993890380787911273437967786556742804566652408275798339221179283430482118140020742719695900657696142739101628984271513292954605191778803974738871043737934546460016184719168074062912083778327025499841998124431899131874519812228674255796948879306477894924710085384116453080236862135706628989104070747737689294987000148388110561753028594988959655591699155508380909698460304884908709246116411180876105681720036833487450945730831039969246996849503525429840196651386469599438064049723005123629385485140945945416764414133189625489032807860400751723995946290581976152580477047961138617997133510128194027510895265424780627975864980749945631413855375897945293107842908479797077570371447220506451229526132919408351287454305932886749170523056147842439813407002950370505941417426433452282518739345666494683448699945734453214481915512562995906034771246088038719298959180199052759295868161570318718927430655393250250811804905393113074074574608255523847592006804881016594060188745212933427473833239777228852952217878690668413947367586040297784502192683200664398064682201012931468052982448022330449955215606614483165425935154496289535573901139223034819824408001205784146243892228030383941863746839845526558421740316887532141893650230936137269356278754487130882868595412163277284772124736531380334814212708066069618080153747333573454834500999083737284449542481264971030785043701582134343596645346132964567391370300568578875509971483039720438955919863275044932311289587494336123538202079503922025306586828117649623642521324286648529829664567232756108169459356549144779085080036654897525078792273443307070502103724611233768453196294899770515940520895908289018412144327894912660060761908970811602375085884115384049610753387776858733798341463052471017393165656926510611173543365663267563198760597092606598728110197523695339144204179424646442294307593146446562536865057987897899655645968129515654148044008249646703504419478535298270862753806142083172190778193001810574370442181909146645889199829207284871551220439225371051511970054965951914399901815408791418836185742573331879114400013259342896515702942707292473805188905427717363630137869116872433627556880809120353079342030725196065815470427569172350436988386579444534375353968759750750178342190349607711313840613843718547859929387259163285524671855725511880656411741012446023392964655239624520090988149679656514996202498334816938716757663800773997302639681907686195671083505910700098597156238624351157219093280177066146218516478636356056420098245995113668018177690728654922707281126889313941750547830163078886329630807850633273613622550216189245162735650139455042125252043274668279981753287687674520319519360593091620297805736177366738063651905396783336064579717230286821545930579779462534206093794040878198825916141099864730374109311705285661056855668930671948265232862757146615431791375559792290479316263924560826544387396762768331402198937951439504767950821089741987629257538953417586416459087855138539304027013800937360598578194413362672871055543854633921502486683911956250444582746421552178164852341035733290405311280719066037175324627429434912416361334254696649419037348733709488576582107382055914938194078813926926742828297826939120316120573453588052056773875836843924877773978390546387248009519202370375478981843515393806263037580338009594022254079586380520797699651840576286033587273591899639699077044271208886940540056794360292760863657703246410020854088849880453524038877935317875884698324859548991680533307680053872403383516589028793015681082435908524045497475001609824047204954932626536311826911363867426654549346914317405110707189532251727848751560224936842128628673253616256326013555922159336370177663785738170802777550686079119049748734352584409583136667752555307842739679930698964098088960000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%bigQ
+.
+
+Fixpoint numden_Rcontfrac_tailrecB (accu: list bigZ) (n1 d1: bigZ) (n2 d2: bigZ) (fuel: nat) {struct fuel}:
+  (list bigZ * bigQ * bigQ) :=
+  let default := (rev_append accu nil, BigQ.div (BigQ.Qz n1) (BigQ.Qz d1), BigQ.div (BigQ.Qz n2) (BigQ.Qz d2)) in
+  match fuel with
+  | O => default
+  | S fuel' =>
+    let '(q1, r1) := BigZ.div_eucl n1 d1 in
+    let '(q2, r2) := BigZ.div_eucl n2 d2 in
+    match BigZ.eqb q1 q2 with
+    | false => default
+    | true =>
+      let r1_is_zero := BigZ.eqb r1 0 in
+      let r2_is_zero := BigZ.eqb r2 0 in
+      match Bool.eqb r1_is_zero r2_is_zero with
+      | false => default
+      | true =>
+        match r1_is_zero with
+          | true =>
+            match BigZ.eqb q1 1 with
+              | true => (rev_append accu nil, 1%bigQ, 1%bigQ)
+              | false => (rev_append ((q1 - 1)%bigZ :: accu) nil, 1%bigQ, 1%bigQ)
+            end
+          | false => numden_Rcontfrac_tailrecB (q1 :: accu) d1 r1 d2 r2 fuel'
+        end
+      end
+    end
+  end.
+
+Definition Bnum b :=
+  match b with
+  | BigQ.Qz t => t
+  | BigQ.Qq n d =>
+    if (d =? BigN.zero)%bigN then 0%bigZ else n
+  end.
+
+Definition Bden b :=
+  match b with
+  | BigQ.Qz _ => 1%bigN
+  | BigQ.Qq _ d => if (d =? BigN.zero)%bigN then 1%bigN else d 
+  end.
+
+Definition rat_Rcontfrac_tailrecB q1 q2 :=
+  numden_Rcontfrac_tailrecB nil (Bnum q1) (BigZ.Pos (Bden q1)) (Bnum q2) (BigZ.Pos (Bden q2)).
+
+Definition pi_4_contfrac :=
+  rat_Rcontfrac_tailrecB pi_4_approx_low' pi_4_approx_high' 3000.
+
+(* The following used to fail because of a non canonical representation of 0 in
+the bytecode interpreter. Bug reported privately by Tahina Ramananandro. *)
+Goal pi_4_contfrac = pi_4_contfrac.
+vm_compute.
+reflexivity.
+Qed.
diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v
index a70d919635..dc0527d826 100644
--- a/test-suite/success/cc.v
+++ b/test-suite/success/cc.v
@@ -129,5 +129,10 @@ Qed.
 
 End bug_2447.
 
+(* congruence was supposed to do discriminate but it was bugged for
+   types with indices *)
 
-
+Inductive I : nat -> Type := C : I 0 | D : I 0.
+Goal ~C=D.
+congruence.
+Qed.
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 83a33f75dc..90a60daa66 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -96,19 +96,21 @@ Abort.
 (* Check that subterm selection does not solve existing evars *)
 
 Goal exists x, S x = S 0.
-eexists.
+eexists ?[x].
+Show x.  (* Incidentally test Show on a named goal *)
 destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *)
 change (0 = S 0).
 Abort.
 
 Goal exists x, S 0 = S x.
-eexists.
+eexists ?[x].
 destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *)
 change (0 = S ?x).
+[x]: exact 0. (* Incidentally test applying a tactic to a goal on the shelve *)
 Abort.
 
 Goal exists n p:nat, (S n,S n) = (S p,S p) /\ p = n.
-do 2 eexists.
+eexists ?[n]; eexists ?[p].
 destruct (_, S _). (* Was unifying at some time in trunk, now takes the first occurrence *)
 change ((n, n0) = (S ?p, S ?p) /\ ?p = ?n).
 Abort.
@@ -387,7 +389,7 @@ Abort.
 
 Goal forall b:bool, True.
 intro b.
-destruct !b.
+destruct (b).
 clear b. (* b has to be here *)
 Abort.
 
@@ -424,7 +426,7 @@ destruct b eqn:H.
 (* Check natural instantiation behavior when the goal has already an evar *)
 
 Goal exists x, S x = x.
-eexists.
+eexists ?[x].
 destruct (S _).
 change (0 = ?x).
 Abort.
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index 9e57801e06..773dd321eb 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v
index 1b5c7f183e..1f6af0dc44 100644
--- a/test-suite/success/eqdecide.v
+++ b/test-suite/success/eqdecide.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v
index 57f3775d7e..0086e090bd 100644
--- a/test-suite/success/extraction.v
+++ b/test-suite/success/extraction.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/extraction_impl.v b/test-suite/success/extraction_impl.v
new file mode 100644
index 0000000000..dfdeff82ff
--- /dev/null
+++ b/test-suite/success/extraction_impl.v
@@ -0,0 +1,82 @@
+
+(** Examples of extraction with manually-declared implicit arguments *)
+
+(** NB: we should someday check the produced code instead of
+    simply running the commands. *)
+
+(** Bug #4243, part 1 *)
+
+Inductive dnat : nat -> Type :=
+| d0 : dnat 0
+| ds : forall n m, n = m -> dnat n ->  dnat (S n).
+
+Extraction Implicit ds [m].
+
+Lemma dnat_nat: forall n, dnat n -> nat.
+Proof.
+  intros n d.
+  induction d as [| n m Heq d IHn].
+  exact 0. exact (S IHn).
+Defined.
+
+Recursive Extraction dnat_nat.
+
+Extraction Implicit dnat_nat [n].
+Recursive Extraction dnat_nat.
+
+(** Same, with a Fixpoint *)
+
+Fixpoint dnat_nat' n (d:dnat n) :=
+ match d with
+ | d0 => 0
+ | ds n m _ d => S (dnat_nat' n d)
+ end.
+
+Recursive Extraction dnat_nat'.
+
+Extraction Implicit dnat_nat' [n].
+Recursive Extraction dnat_nat'.
+
+(** Bug #4243, part 2 *)
+
+Inductive enat: nat -> Type :=
+  e0: enat 0
+| es: forall n, enat n -> enat (S n).
+
+Lemma enat_nat: forall n, enat n -> nat.
+Proof.
+  intros n e.
+  induction e as [| n e IHe].
+  exact (O).
+  exact (S IHe).
+Defined.
+
+Extraction Implicit es [n].
+Extraction Implicit enat_nat [n].
+Recursive Extraction enat_nat.
+
+(** Same, with a Fixpoint *)
+
+Fixpoint enat_nat' n (e:enat n) : nat :=
+ match e with
+ | e0 => 0
+ | es n e => S (enat_nat' n e)
+ end.
+
+Extraction Implicit enat_nat' [n].
+Recursive Extraction enat_nat'.
+
+(** Bug #4228 *)
+
+Module Food.
+Inductive Course :=
+| main:    nat -> Course
+| dessert: nat -> Course.
+
+Inductive Meal : Course -> Type :=
+| one_course : forall n:nat, Meal (main n)
+| two_course : forall n m, Meal (main n) -> Meal (dessert m).
+Extraction Implicit two_course [n].
+End Food.
+
+Recursive Extraction Food.Meal.
diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v
index b733aef6db..c729b23ce7 100644
--- a/test-suite/success/inds_type_sec.v
+++ b/test-suite/success/inds_type_sec.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index 7ae60d9892..1ed731f50f 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -151,3 +151,46 @@ intros x H1 H.
 induction H.
 change (0 = z -> True) in IHrepr''.
 Abort.
+
+(* Test double induction *)
+
+(* This was failing in 8.5 and before because of a bug in the order of
+   hypotheses *)
+
+Inductive I2 : Type :=
+  C2 : forall x:nat, x=x -> I2.
+Goal forall a b:I2, a = b.
+double induction a b.
+Abort.
+
+(* This was leaving useless hypotheses in 8.5 and before because of
+   the same bug. This is a change of compatibility. *)
+
+Inductive I3 : Prop :=
+  C3 : forall x:nat, x=x -> I3.
+Goal forall a b:I3, a = b.
+double induction a b.
+Fail clear H. (* H should have been erased *)
+Abort.
+
+(* This one had quantification in reverse order in 8.5 and before *)
+(* This is a change of compatibility. *)
+
+Goal forall m n, le m n -> le n m -> n=m.
+intros m n. double induction 1 2.
+3:destruct 1. (* Should be "S m0 <= m0" *)
+Abort.
+
+(* Idem *)
+
+Goal forall m n p q, le m n -> le p q -> n+p=m+q.
+intros *. double induction 1 2.
+3:clear H2. (* H2 should have been erased *)
+Abort.
+
+(* This is unchanged *)
+
+Goal forall m n:nat, n=m.
+double induction m n.
+Abort.
+
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index ae1694c58c..ee69df9774 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -34,30 +34,97 @@ intros _ ?.
 exact H.
 Qed.
 
-(* A short test about introduction pattern pat/c *)
+(* A short test about introduction pattern pat%c *)
 Goal (True -> 0=0) -> True /\ False -> 0=0.
-intros H (H1/H,_).
+intros H (H1%H,_).
 exact H1.
 Qed.
 
 (* A test about bugs in 8.5beta2 *)
 Goal (True -> 0=0) -> True /\ False -> False -> 0=0.
 intros H H0 H1.
-destruct H0 as (a/H,_).
+destruct H0 as (a%H,_).
 (* Check that H0 is removed (was bugged in 8.5beta2) *)
 Fail clear H0.
-(* Check position of newly created hypotheses when using pat/c (was
+(* Check position of newly created hypotheses when using pat%c (was
    left at top in 8.5beta2) *)
 match goal with H:_ |- _ => clear H end. (* clear H1:False *)
 match goal with H:_ |- _ => exact H end. (* check that next hyp shows 0=0 *)
 Qed.
 
 Goal (True -> 0=0) -> True -> 0=0.
-intros H H1/H.
+intros H H1%H.
 exact H1.
 Qed.
 
 Goal forall n, n = S n -> 0=0.
-intros n H/n_Sn.
+intros n H%n_Sn.
 destruct H.
 Qed.
+
+(* Another check about generated names and cleared hypotheses with
+   pat%c patterns *)
+Goal (True -> 0=0 /\ 1=1) -> True -> 0=0.
+intros H (H1,?)%H.
+change (1=1) in H0.
+exact H1.
+Qed.
+
+(* Checking iterated pat%c1...%cn introduction patterns and side conditions *)
+
+Goal forall A B C D:Prop, (A -> B -> C) -> (C -> D) -> B -> A -> D.
+intros * H H0 H1.
+intros H2%H%H0.
+- exact H2.
+- exact H1.
+Qed.
+
+(* Bug found by Enrico *)
+
+Goal forall x : nat, True.
+intros y%(fun x => x).
+Abort.
+
+(* Fixing a bug in the order of side conditions of a "->" step *)
+
+Goal (True -> 1=0) -> 1=1.
+intros ->.
+- reflexivity.
+- exact I.
+Qed.
+
+Goal forall x, (True -> x=0) -> 0=x.
+intros x ->.
+- reflexivity.
+- exact I.
+Qed.
+
+(* Fixing a bug when destructing a type with let-ins in the constructor *)
+
+Inductive I := C : let x:=1 in x=1 -> I.
+Goal I -> True.
+intros [x H]. (* Was failing in 8.5 *)
+Abort.
+
+(* Ensuring that the (pat1,...,patn) intropatterns has the expected size, up
+   to skipping let-ins *)
+
+Goal I -> 1=1.
+intros (H).  (* This skips x *)
+exact H.
+Qed.
+
+Goal I -> 1=1.
+Fail intros (x,H,H').
+Fail intros [|].
+intros (x,H).
+exact H.
+Qed.
+
+Goal Acc le 0 -> True.
+Fail induction 1 as (n,H). (* Induction hypothesis is missing *)
+induction 1 as (n,H,IH).
+exact Logic.I.
+Qed.
+
+
diff --git a/test-suite/success/keyedrewrite.v b/test-suite/success/keyedrewrite.v
index bbe9d4bfff..b88c142be1 100644
--- a/test-suite/success/keyedrewrite.v
+++ b/test-suite/success/keyedrewrite.v
@@ -22,3 +22,41 @@ Qed.
 
 Print Equivalent Keys.
 End foo.
+
+Require Import Arith List Omega.
+
+Definition G {A} (f : A -> A -> A) (x : A) := f x x.
+
+Lemma list_foo A (l : list A) : G (@app A) (l ++ nil) = G (@app A) l.
+Proof. unfold G; rewrite app_nil_r; reflexivity. Qed.
+
+(* Bundled version of a magma *)
+Structure magma := Magma { b_car :> Type; op : b_car -> b_car -> b_car }.
+Arguments op {_} _ _.
+
+(* Instance for lists *)
+Canonical Structure list_magma A := Magma (list A) (@app A).
+
+(* Basically like list_foo, but now uses the op projection instead of app for
+the argument of G *)
+Lemma test1 A (l : list A) : G op (l ++ nil) = G op l.
+
+(* Ensure that conversion of terms with evars is allowed once a keyed candidate unifier is found *)
+rewrite -> list_foo.
+reflexivity.
+Qed.
+
+(* Basically like list_foo, but now uses the op projection for everything *)
+Lemma test2 A (l : list A) : G op (op l nil) = G op l.
+Proof.
+rewrite ->list_foo.
+reflexivity.
+Qed.
+
+ Require Import Bool.
+   Set Keyed Unification.
+
+   Lemma test b : b && true = b.
+    Fail rewrite andb_true_l.
+   Admitted.
+   
\ No newline at end of file
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index f9df021dc2..ce90990594 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -15,7 +15,7 @@ Ltac F x := idtac; G x
  with G y := idtac; F y.
 
 (* Check that Match Context keeps a closure *)
-Ltac U := let a := constr:I in
+Ltac U := let a := constr:(I) in
           match goal with
           |  |- _ => apply a
           end.
@@ -75,7 +75,7 @@ Qed.
 
 (* Check context binding *)
 Ltac sym t :=
-  match constr:t with
+  match constr:(t) with
   | context C[(?X1 = ?X2)] => context C [X1 = X2]
   end.
 
@@ -143,7 +143,7 @@ Qed.
 
 Ltac check_binding y := cut ((fun y => y) = S).
 Goal True.
-check_binding ipattern:H.
+check_binding ipattern:(H).
 Abort.
 
 (* Check that variables explicitly parsed as ltac variables are not
@@ -151,7 +151,7 @@ Abort.
 
 Ltac afi tac := intros; tac.
 Goal 1 = 2.
-afi ltac:auto.
+afi ltac:(auto).
 Abort.
 
 (* Tactic Notation avec listes *)
@@ -174,7 +174,7 @@ Abort.
    empty args *)
 
 Goal True.
-match constr:@None with @None => exact I end.
+match constr:(@None) with @None => exact I end.
 Abort.
 
 (* Check second-order pattern unification *)
@@ -218,7 +218,7 @@ Ltac Z1 t := set (x:=t).
 Ltac Z2 t := t.
 Goal True -> True.
 Z1 O.
-Z2 ltac:O.
+Z2 ltac:(O).
 exact I.
 Qed.
 
@@ -302,7 +302,18 @@ Abort.
 (* Check instantiation of binders using ltac names *)
 
 Goal True.
-let x := ipattern:y in assert (forall x y, x = y + 0).
+let x := ipattern:(y) in assert (forall x y, x = y + 0).
 intro.
 destruct y. (* Check that the name is y here *)
 Abort.
+
+(* An example suggested by Jason (see #4317) showing the intended semantics *)
+(* Order of binders is reverted because y is just told to depend on x *)
+
+Goal 1=1.
+let T := constr:(fun a b : nat => a) in
+  lazymatch T with
+  | (fun x z => ?y) => pose ((fun x x => y) 2 1)
+  end.
+exact (eq_refl n).
+Qed.
diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v
index 54cfa658c8..45c1a5e584 100644
--- a/test-suite/success/mutual_ind.v
+++ b/test-suite/success/mutual_ind.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/namedunivs.v b/test-suite/success/namedunivs.v
index 059462fac3..f9154ef576 100644
--- a/test-suite/success/namedunivs.v
+++ b/test-suite/success/namedunivs.v
@@ -4,6 +4,8 @@
 (* Fail  exact H. *)
 (* Section . *)
 
+Unset Strict Universe Declaration.
+
 Section lift_strict.
 Polymorphic Definition liftlt := 
   let t := Type@{i} : Type@{k} in
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 957612ef1d..878875bd92 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -1,3 +1,5 @@
+Unset Strict Universe Declaration.
+
 Module withoutpoly.
 
 Inductive empty :=. 
@@ -240,7 +242,7 @@ Fail Check (Prop : Set).
 Fail Check (Set : Set).
 Check (Set : Type).
 Check (Prop : Type).
-Definition setType := $(let t := type of Set in exact t)$.
+Definition setType := ltac:(let t := type of Set in exact t).
 
 Definition foo (A : Prop) := A.
 
@@ -301,7 +303,7 @@ Set Printing Universes.
 Axiom admit : forall A, A.
 Record R := {O : Type}.
 
-Definition RL (x : R@{i}) : $(let u := constr:(Type@{i}:Type@{j}) in exact (R@{j}) )$ := {|O := @O x|}.
+Definition RL (x : R@{i}) : ltac:(let u := constr:(Type@{i}:Type@{j}) in exact (R@{j}) ) := {|O := @O x|}.
 Definition RLRL : forall x : R, RL x = RL (RL x) := fun x => eq_refl.
 Definition RLRL' : forall x : R, RL x = RL (RL x).
   intros. apply eq_refl.
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 125615c535..b5e6ccd618 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -35,10 +35,6 @@ Set Implicit Arguments.
 
 Check nat.
 
-(* Inductive X (U:Type) := Foo (k : nat) (x : X U).  *)
-(* Parameter x : X nat. *)
-(* Check x.(k). *)
-
 Inductive X (U:Type) := { k : nat; a: k = k -> X U; b : let x := a eq_refl in X U }.
 
 Parameter x:X nat.
@@ -49,18 +45,8 @@ Inductive Y := { next : option Y }.
 
 Check _.(next) : option Y.
 Lemma eta_ind (y : Y) : y = Build_Y y.(next).
-Proof. reflexivity. Defined.
-
-Variable t : Y.
+Proof. Fail reflexivity. Abort.
 
-Fixpoint yn (n : nat) (y : Y) : Y := 
-  match n with
-    | 0 => t
-    | S n => {| next := Some (yn n y) |}
-  end.
-
-Lemma eta_ind'  (y: Y) : Some (yn 100 y) = Some {| next := (yn 100 y).(next) |}.
-Proof. reflexivity. Defined.
 
 
 (* 
@@ -194,4 +180,17 @@ 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.
 Recursive Extraction term term'.
-(*Unset Printing Primitive Projection Parameters.*)
\ No newline at end of file
+(*Unset Printing Primitive Projection Parameters.*)
+
+(* Primitive projections in the presence of let-ins (was not failing in beta3)*)
+
+Set Primitive Projections.
+Record s (x:nat) (y:=S x) := {c:=x; d:x=c}.
+Lemma f : 0=1.
+Proof.
+Fail apply d.
+(*
+split.
+reflexivity.
+Qed.
+*)
diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v
index 61e73f8587..adaa05ad06 100644
--- a/test-suite/success/proof_using.v
+++ b/test-suite/success/proof_using.v
@@ -117,5 +117,82 @@ End T1.
 
 Check (bla 7 : 2 = 8).
 
+Section A.
+Variable a : nat.
+Variable b : nat.
+Variable c : nat.
+Variable H1 : a = 3.
+Variable H2 : a = 3 -> b = 7.
+Variable H3 : c = 3.
+
+Lemma foo : a = a.
+Proof using Type*.
+pose H1 as e1.
+pose H2 as e2.
+reflexivity.
+Qed.
+
+Lemma bar : a = 3 -> b = 7.
+Proof using b*.
+exact H2.
+Qed.
+
+Lemma baz : c=3.
+Proof using c*.
+exact H3.
+Qed.
+
+Lemma baz2 : c=3.
+Proof using c* a.
+exact H3.
+Qed.
+
+End A.
+
+Check (foo 3 7 (refl_equal 3)
+               (fun _ => refl_equal 7)).
+Check (bar 3 7 (refl_equal 3)
+               (fun _ => refl_equal 7)).
+Check (baz2 99 3 (refl_equal 3)).
+Check (baz 3 (refl_equal 3)).
+
+Section Let.
+
+Variables a b : nat.
+Let pa : a = a. Proof. reflexivity. Qed.
+Unset Default Proof Using.
+Set Suggest Proof Using.
+Lemma test_let : a = a.
+Proof using a.
+exact pa.
+Qed.
+
+Let ppa : pa = pa. Proof. reflexivity. Qed.
+
+Lemma test_let2 : pa = pa.
+Proof using Type.
+exact ppa.
+Qed.
+
+End Let.
+
+Check (test_let 3).
+
+(* Disabled
+Section Clear.
+
+Variable a: nat.
+Hypotheses H : a = 4.
+
+Set Proof Using Clear Unused.
+
+Lemma test_clear : a = a.
+Proof using a.
+Fail rewrite H.
+trivial.
+Qed.
+
+End Clear.
+*)
 
 
diff --git a/test-suite/success/record_syntax.v b/test-suite/success/record_syntax.v
new file mode 100644
index 0000000000..db2bbb0dc7
--- /dev/null
+++ b/test-suite/success/record_syntax.v
@@ -0,0 +1,47 @@
+Module A.
+
+Record Foo := { foo : unit; bar : unit }.
+
+Definition foo_ := {|
+  foo := tt;
+  bar := tt
+|}.
+
+Definition foo0 (p : Foo) := match p with {| |} => tt end.
+Definition foo1 (p : Foo) := match p with {| foo := f |} => f end.
+Definition foo2 (p : Foo) := match p with {| foo := f; |} => f end.
+Definition foo3 (p : Foo) := match p with {| foo := f; bar := g |} => (f, g) end.
+Definition foo4 (p : Foo) := match p with {| foo := f; bar := g; |} => (f, g) end.
+
+End A.
+
+Module B.
+
+Record Foo := { }.
+
+End B.
+
+Module C.
+
+Record Foo := { foo : unit; bar : unit; }.
+
+Definition foo_ := {|
+  foo := tt;
+  bar := tt;
+|}.
+
+End C.
+
+Module D.
+
+Record Foo := { foo : unit }.
+Definition foo_ := {| foo := tt |}.
+
+End D.
+
+Module E.
+
+Record Foo := { foo : unit; }.
+Definition foo_ := {| foo := tt; |}.
+
+End E.
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v
index 1e667884b8..352abb2af5 100644
--- a/test-suite/success/refine.v
+++ b/test-suite/success/refine.v
@@ -62,7 +62,7 @@ Abort.
 Goal (forall n : nat, n = 0 -> Prop) -> Prop.
 intro P.
  refine (P _ _).
-2:reflexivity.
+reflexivity.
 Abort.
 
 (* Submitted by Jacek Chrzaszcz (bug #1102) *)
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
index 0465c4b3fb..1f24ef2a6b 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -166,3 +166,16 @@ Proof. intros. setoid_rewrite <- foo_prf. change (beq_nat x 0 = y). Abort.
 Goal forall (x : nat) (y : bool), beq_nat (foo_neg x) 0 = foo_neg y.
 Proof. intros. setoid_rewrite <- @foo_prf at 1. change (beq_nat x 0 = foo_neg y). Abort.
 
+(* This should not raise an anomaly as it did for some time in early 2016 *)
+
+Definition t := nat -> bool.
+Definition h (a b : t) := forall n, a n = b n.
+
+Instance subrelh : subrelation h (Morphisms.pointwise_relation nat eq).
+Proof. intros x y H; assumption. Qed.
+
+Goal forall a b, h a b -> a 0 = b 0.
+intros.
+setoid_rewrite H. (* Fallback on ordinary rewrite without anomaly *)
+reflexivity.
+Qed.
diff --git a/test-suite/success/sideff.v b/test-suite/success/sideff.v
new file mode 100644
index 0000000000..3c0b81568a
--- /dev/null
+++ b/test-suite/success/sideff.v
@@ -0,0 +1,12 @@
+Definition idw (A : Type) := A.
+Lemma foobar : unit.
+Proof.
+  Require Import Program.
+  apply (const tt tt).
+Qed.
+
+Lemma foobar' : unit.
+  Lemma aux : forall A : Type, A -> unit.
+  Proof. intros. pose (foo := idw A). exact tt. Show Universes. Qed.
+  apply (@aux unit tt).
+Qed.
diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v
index 2954e25562..d595cbc2b8 100644
--- a/test-suite/success/unfold.v
+++ b/test-suite/success/unfold.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v
index e00701fb68..269359ae62 100644
--- a/test-suite/success/univers.v
+++ b/test-suite/success/univers.v
@@ -60,3 +60,20 @@ Qed.
 (* Submitted by Danko Ilik (bug report #1507); related to LetIn *)
 
 Record U : Type := { A:=Type; a:A }.
+
+(** Check assignement of sorts to inductives and records. *)
+
+Variable sh : list nat.
+
+Definition is_box_in_shape (b :nat * nat) := True.
+Definition myType := Type.
+
+Module Ind.
+Inductive box_in : myType :=
+  myBox (coord : nat * nat) (_ : is_box_in_shape coord) : box_in.
+End Ind.
+
+Module Rec.
+Record box_in : myType :=
+  BoxIn { coord :> nat * nat; _ : is_box_in_shape coord }.
+End Rec.
\ No newline at end of file
diff --git a/test-suite/success/univnames.v b/test-suite/success/univnames.v
new file mode 100644
index 0000000000..048b53d26c
--- /dev/null
+++ b/test-suite/success/univnames.v
@@ -0,0 +1,26 @@
+Set Universe Polymorphism.
+
+Definition foo@{i j} (A : Type@{i}) (B : Type@{j}) := A.
+
+Set Printing Universes.
+
+Fail Definition bar@{i} (A : Type@{i}) (B : Type) := A.
+
+Definition baz@{i j} (A : Type@{i}) (B : Type@{j}) := (A * B)%type.
+
+Fail Definition bad@{i j} (A : Type@{i}) (B : Type@{j}) : Type := (A * B)%type.
+
+Fail Definition bad@{i} (A : Type@{i}) (B : Type@{j}) : Type := (A * B)%type.
+
+Definition shuffle@{i j} (A : Type@{j}) (B : Type@{i}) := (A * B)%type.
+
+Definition nothing (A : Type) := A.
+
+Inductive bla@{l k} : Type@{k} := blaI : Type@{l} -> bla.
+
+Inductive blacopy@{k l} : Type@{k} := blacopyI : Type@{l} -> blacopy.
+
+
+Monomorphic Universe g.
+
+Inductive blacopy'@{l} : Type@{g} := blacopy'I : Type@{l} -> blacopy'.
\ No newline at end of file
diff --git a/test-suite/success/unshelve.v b/test-suite/success/unshelve.v
new file mode 100644
index 0000000000..672222bdd6
--- /dev/null
+++ b/test-suite/success/unshelve.v
@@ -0,0 +1,11 @@
+Axiom F : forall (b : bool), b = true ->
+  forall (i : unit), i = i -> True.
+
+Goal True.
+Proof.
+unshelve (refine (F _ _ _ _)).
++ exact true.
++ exact tt.
++ exact (@eq_refl bool true).
++ exact (@eq_refl unit tt).
+Qed.
diff --git a/test-suite/success/vm_univ_poly.v b/test-suite/success/vm_univ_poly.v
new file mode 100644
index 0000000000..58fa39743d
--- /dev/null
+++ b/test-suite/success/vm_univ_poly.v
@@ -0,0 +1,141 @@
+(* Basic tests *)
+Polymorphic Definition pid {T : Type} (x : T) : T := x.
+(*
+Definition _1 : pid true = true :=
+  @eq_refl _ true <: pid true = true.
+
+Polymorphic Definition a_type := Type.
+
+Definition _2 : a_type@{i} = Type@{i} :=
+  @eq_refl _ Type@{i} <: a_type@{i} = Type@{i}.
+
+Polymorphic Definition FORALL (T : Type) (P : T -> Prop) : Prop :=
+  forall x : T, P x.
+
+Polymorphic Axiom todo : forall {T:Type}, T -> T.
+
+Polymorphic Definition todo' (T : Type) := @todo T.
+
+Definition _3 : @todo'@{Set} = @todo@{Set} :=
+  @eq_refl _ (@todo@{Set}) <: @todo'@{Set} = @todo@{Set}.
+*)
+
+(* Inductive Types *)
+Inductive sumbool (A B : Prop) : Set :=
+| left : A -> sumbool A B
+| right : B -> sumbool A B.
+
+Definition x : sumbool True False := left _ _ I.
+
+Definition sumbool_copy {A B : Prop} (H : sumbool A B) : sumbool A B :=
+  match H with
+  | left _ _ x => left _ _ x
+  | right _ _ x => right _ _ x
+  end.
+
+Definition _4 : sumbool_copy x = x :=
+  @eq_refl _ x <: sumbool_copy x = x.
+
+(* Polymorphic Inductive Types *)
+Polymorphic Inductive poption@{i} (T : Type@{i}) : Type@{i} :=
+| PSome : T -> poption@{i} T
+| PNone : poption@{i} T.
+
+Polymorphic Definition poption_default@{i} {T : Type@{i}} (p : poption@{i} T) (x : T) : T :=
+  match p with
+  | @PSome _ y => y
+  | @PNone _ => x
+  end.
+
+Polymorphic Inductive plist@{i} (T : Type@{i}) : Type@{i} :=
+| pnil
+| pcons : T -> plist@{i} T -> plist@{i} T.
+
+Arguments pnil {_}.
+Arguments pcons {_} _ _.
+
+Polymorphic Definition pmap@{i j}
+            {T : Type@{i}} {U : Type@{j}} (f : T -> U) :=
+  fix pmap (ls : plist@{i} T) : plist@{j} U :=
+    match ls with
+    | @pnil _ => @pnil _
+    | @pcons _ l ls => @pcons@{j} U (f l) (pmap@{i j} ls)
+    end.
+
+Universe Ubool.
+Inductive tbool : Type@{Ubool} := ttrue | tfalse.
+
+
+Eval vm_compute in pmap pid (pcons true (pcons false pnil)).
+Eval vm_compute in pmap (fun x => match x with
+                                  | pnil => true
+                                  | pcons _ _ => false
+                                  end) (pcons pnil (pcons (pcons false pnil) pnil)).
+Eval vm_compute in pmap (fun x => x -> Type) (pcons tbool (pcons (plist tbool) pnil)).
+
+Polymorphic Inductive Tree@{i} (T : Type@{i}) : Type@{i} :=
+| Empty
+| Branch : plist@{i} (Tree@{i} T) -> Tree@{i} T.
+
+Polymorphic Definition pfold@{i u}
+            {T : Type@{i}} {U : Type@{u}} (f : T -> U -> U) :=
+  fix pfold (acc : U) (ls : plist@{i} T) : U :=
+    match ls with
+    | pnil => acc
+    | pcons a b => pfold (f a acc) b
+    end.
+
+Polymorphic Inductive nat@{i} : Type@{i} :=
+| O
+| S : nat -> nat.
+
+Polymorphic Fixpoint nat_max@{i} (a b : nat@{i}) : nat@{i} :=
+  match a , b with
+  | O , b => b
+  | a , O => a
+  | S a , S b => S (nat_max a b)
+  end.
+
+Polymorphic Fixpoint height@{i} {T : Type@{i}} (t : Tree@{i} T) : nat@{i} :=
+  match t return nat@{i} with
+  | Empty _ => O
+  | Branch _ ls => S@{i} (pfold@{i i} nat_max O (pmap height ls))
+  end.
+
+Polymorphic Fixpoint repeat@{i} {T : Type@{i}} (n : nat@{i}) (v : T) : plist@{i} T :=
+  match n return plist@{i} T with
+  | O => pnil
+  | S n => pcons@{i} v (repeat n v)
+  end.
+
+Polymorphic Fixpoint big_tree@{i} (n : nat@{i}) : Tree@{i} nat@{i} :=
+  match n with
+  | O => @Empty nat@{i}
+  | S n' => Branch@{i} nat@{i} (repeat@{i} n' (big_tree@{i} n'))
+  end.
+
+Eval compute in height (big_tree (S (S (S O)))).
+
+Let big := S (S (S (S (S O)))).
+Polymorphic Definition really_big@{i} := (S@{i} (S (S (S (S (S (S (S (S (S O)))))))))).
+
+Time Definition _5 : height (@Empty nat) = O :=
+  @eq_refl nat O <: height (@Empty nat) = O.
+
+Time Definition _6 : height@{Set} (@Branch nat pnil) = S O :=
+  @eq_refl nat@{Set} (S@{Set} O@{Set}) <: @eq nat@{Set} (height@{Set} (@Branch@{Set} nat@{Set} (@pnil@{Set} (Tree@{Set} nat@{Set})))) (S@{Set} O@{Set}).
+
+Time Definition _7 : height (big_tree big) = big :=
+  @eq_refl nat big <: height (big_tree big) = big.
+
+Time Definition _8 : height (big_tree really_big) = really_big :=
+ @eq_refl nat@{Set} (S@{Set}
+        (S@{Set}
+           (S@{Set}
+              (S@{Set}
+                 (S@{Set}
+                    (S@{Set} (S@{Set} (S@{Set} (S@{Set} (S@{Set} O@{Set}))))))))))
+ <:
+ @eq nat@{Set}
+   (@height nat@{Set} (big_tree really_big@{Set}))
+   really_big@{Set}.
diff --git a/test-suite/success/vm_univ_poly_match.v b/test-suite/success/vm_univ_poly_match.v
new file mode 100644
index 0000000000..abe6d0fe07
--- /dev/null
+++ b/test-suite/success/vm_univ_poly_match.v
@@ -0,0 +1,28 @@
+Set Dump Bytecode.
+Set Printing Universes.
+Set Printing All.
+
+Polymorphic Class Applicative@{d c} (T : Type@{d} -> Type@{c}) :=
+{ pure : forall {A : Type@{d}}, A -> T A
+ ; ap : forall {A B : Type@{d}}, T (A -> B) -> T A -> T B
+}.
+
+Universes Uo Ua.
+
+Eval compute in @pure@{Uo Ua}.
+
+Global Instance Applicative_option : Applicative@{Uo Ua} option :=
+{| pure := @Some
+ ; ap := fun _ _ f x =>
+           match f , x with
+             | Some f , Some x => Some (f x)
+             | _ , _ => None
+           end
+|}.
+
+Definition foo := ap (ap (pure plus) (pure 1)) (pure 1).
+
+Print foo.
+
+
+Eval vm_compute in foo.