From 379c2403b1cd031091a2271353f26ab24afeb1e5 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 22 Oct 2016 10:17:39 +0200
Subject: Port fix for bugs 4763, 5149, previously 0b417c12e

Adds a compatibility flag so that the behavior of 8.5 can be obtained too.

Original commit:
   unification.ml: fix for bug #4763, unif regression

    Do not force all remaining conversions problems to be solved after
    the _first_ solution of an evar. This was hell to track down, thanks
    for the help of Maxime. contribs pass and HoTT too.
---
 test-suite/bugs/closed/4763.v         | 13 +++++++++++++
 test-suite/bugs/closed/HoTT_coq_117.v | 21 ++++++++++++++++++++-
 2 files changed, 33 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4763.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4763.v b/test-suite/bugs/closed/4763.v
new file mode 100644
index 0000000000..ae8ed0e6e8
--- /dev/null
+++ b/test-suite/bugs/closed/4763.v
@@ -0,0 +1,13 @@
+Require Import Coq.Arith.Arith Coq.Classes.Morphisms Coq.Classes.RelationClasses.
+Coercion is_true : bool >-> Sortclass.
+Global Instance: Transitive leb.
+Admitted.
+
+Goal forall x y z, leb x y -> leb y z -> True.
+  intros ??? H H'.
+  lazymatch goal with
+  | [ H : is_true (?R ?x ?y), H' : is_true (?R ?y ?z) |- _ ]
+    => pose proof (transitivity H H' : is_true (R x z))
+  end.
+  exact I.
+Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/HoTT_coq_117.v b/test-suite/bugs/closed/HoTT_coq_117.v
index 5fbcfef4e0..de60fd0ae4 100644
--- a/test-suite/bugs/closed/HoTT_coq_117.v
+++ b/test-suite/bugs/closed/HoTT_coq_117.v
@@ -16,10 +16,29 @@ Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A,
 Admitted.
 
 Inductive Empty : Set := .
-Instance contr_from_Empty {_ : Funext} (A : Type) :
+Fail Instance contr_from_Empty {_ : Funext} (A : Type) :
+  Contr_internal (Empty -> A) :=
+  BuildContr _
+             (Empty_rect (fun _ => A))
+             (fun f => path_forall _ f (fun x => Empty_rect _ x)).
+
+Fail Instance contr_from_Empty {F : Funext} (A : Type) :
   Contr_internal (Empty -> A) :=
   BuildContr _
              (Empty_rect (fun _ => A))
              (fun f => path_forall _ f (fun x => Empty_rect _ x)).
+
+(** This could be disallowed, this uses the Funext argument *)
+Instance contr_from_Empty {_ : Funext} (A : Type) :
+  Contr_internal (Empty -> A) :=
+  BuildContr _
+             (Empty_rect (fun _ => A))
+             (fun f => path_forall _ f (fun x => Empty_rect (fun _ => _ x = f x) x)).
+
+Instance contr_from_Empty' {_ : Funext} (A : Type) :
+  Contr_internal (Empty -> A) :=
+  BuildContr _
+             (Empty_rect (fun _ => A))
+             (fun f => path_forall _ f (fun x => Empty_rect (fun _ => _ x = f x) x)).
 (* Toplevel input, characters 15-220:
 Anomaly: unknown meta ?190. Please report. *)
-- 
cgit v1.2.3


From ccb173a440fa2eb7105a692c979253edbfe475ee Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 19 Oct 2016 13:33:28 +0200
Subject: Unification constraint handling (#4763, #5149)

Refine fix for bug #4763, fixing #5149

Tactic [Refine.solve_constraints] and global option

Adds a new multi-goal tactic [Refine.solve_constraints] that forces solving of
unification constraints and evar candidates to be solved. run_tactic now calls
[solve_constraints] at every [.], preserving (mostly) the 8.4/8.5 behavior of tactics.
The option allows to unset the forced solving unification constraints at
each ".", letting the user control the places where the use of
heuristics is done.

Fix test-suite files too.
---
 test-suite/bugs/closed/2310.v       |  6 ++++-
 test-suite/bugs/closed/3647.v       |  3 ++-
 test-suite/bugs/closed/4416.v       |  1 +
 test-suite/bugs/closed/5149.v       | 47 +++++++++++++++++++++++++++++++++++++
 test-suite/output/unifconstraints.v |  1 +
 5 files changed, 56 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/bugs/closed/5149.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/2310.v b/test-suite/bugs/closed/2310.v
index 0be859eddf..9fddede7e9 100644
--- a/test-suite/bugs/closed/2310.v
+++ b/test-suite/bugs/closed/2310.v
@@ -14,4 +14,8 @@ Definition replace a (y:Nest (prod a a)) : a = a -> Nest a.
    (P:=\a.Nest (prod a a) and P:=\_.Nest (prod a a)) and refine should either
    leave P as subgoal or choose itself one solution *)
 
-intros. refine (Cons (cast H _ y)).
\ No newline at end of file
+  intros. Fail refine (Cons (cast H _ y)).
+  Unset Use Unification Heuristics. (* Keep the unification constraint around *)
+  refine (Cons (cast H _ y)).
+  intros.
+  refine (Nest (prod X X)). Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3647.v b/test-suite/bugs/closed/3647.v
index 495e67e09e..f2cd41203c 100644
--- a/test-suite/bugs/closed/3647.v
+++ b/test-suite/bugs/closed/3647.v
@@ -650,4 +650,5 @@ Goal    forall (ptest : program) (cond : Condition) (value : bool)
 
   Grab Existential Variables.
   subst_body; simpl.
-  refine (all_behead (projT2 _)).
+  Fail refine (all_behead (projT2 _)).
+  Unset Use Unification Heuristics. refine (all_behead (projT2 _)).
diff --git a/test-suite/bugs/closed/4416.v b/test-suite/bugs/closed/4416.v
index b97a8ce640..afe8c62ed0 100644
--- a/test-suite/bugs/closed/4416.v
+++ b/test-suite/bugs/closed/4416.v
@@ -1,3 +1,4 @@
 Goal exists x, x.
+Unset Use Unification Heuristics.
 unshelve refine (ex_intro _ _ _); match goal with _ => refine (_ _) end.
 (* Error: Incorrect number of goals (expected 2 tactics). *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/5149.v b/test-suite/bugs/closed/5149.v
new file mode 100644
index 0000000000..01b9d158fe
--- /dev/null
+++ b/test-suite/bugs/closed/5149.v
@@ -0,0 +1,47 @@
+Goal forall x x' : nat, x = x' -> S x = S x -> exists y, S y = S x.
+intros.
+eexists.
+rewrite <- H.
+eassumption.
+Qed.
+
+Goal forall (base_type_code : Type) (t : base_type_code) (flat_type : Type) 
+            (t' : flat_type) (exprf interp_flat_type0 interp_flat_type1 : 
+flat_type -> Type)
+            (v v' : interp_flat_type1 t'),
+    v = v' ->
+    forall (interpf : forall t0 : flat_type, exprf t0 -> interp_flat_type1 t0)
+           (SmartVarVar : forall t0 : flat_type, interp_flat_type1 t0 -> 
+interp_flat_type0 t0)
+           (Tbase : base_type_code -> flat_type) (x : exprf (Tbase t))
+           (x' : interp_flat_type1 (Tbase t)) (T : Type)
+           (flatten_binding_list : forall t0 : flat_type,
+               interp_flat_type0 t0 -> interp_flat_type1 t0 -> list T)
+           (P : T -> list T -> Prop) (prod : Type -> Type -> Type)
+           (s : forall x0 : base_type_code, prod (exprf (Tbase x0)) 
+(interp_flat_type1 (Tbase x0)) -> T)
+           (pair : forall A B : Type, A -> B -> prod A B),
+      P (s t (pair (exprf (Tbase t)) (interp_flat_type1 (Tbase t)) x x'))
+        (flatten_binding_list t' (SmartVarVar t' v') v) ->
+      (forall (t0 : base_type_code) (t'0 : flat_type) (v0 : interp_flat_type1 
+t'0)
+              (x0 : exprf (Tbase t0)) (x'0 : interp_flat_type1 (Tbase t0)),
+          P (s t0 (pair (exprf (Tbase t0)) (interp_flat_type1 (Tbase t0)) x0 
+x'0))
+            (flatten_binding_list t'0 (SmartVarVar t'0 v0) v0) -> interpf 
+(Tbase t0) x0 = x'0) ->
+      interpf (Tbase t) x = x'.
+Proof.
+  intros ?????????????????????? interpf_SmartVarVar.
+  solve [ unshelve (subst; eapply interpf_SmartVarVar; eassumption) ] || fail 
+"too early".
+  Undo.
+  (** Implicitely at the dot. The first fails because unshelve adds a goal, and solve hence fails. The second has an ambiant unification problem that is solved after solve *)
+  Fail solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption) ].
+  solve [eapply interpf_SmartVarVar; subst; eassumption].
+  Undo.
+  Unset Use Unification Heuristics.
+  (* User control of when constraints are solved *)
+  solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption); solve_constraints ].
+Qed.
+
diff --git a/test-suite/output/unifconstraints.v b/test-suite/output/unifconstraints.v
index c76fc74a0c..c7fb82adac 100644
--- a/test-suite/output/unifconstraints.v
+++ b/test-suite/output/unifconstraints.v
@@ -1,4 +1,5 @@
 (* Set Printing Existential Instances. *)
+Unset Use Unification Heuristics.
 Axiom veeryyyyyyyyyyyyloooooooooooooonggidentifier : nat.
 Goal True /\ True /\ True \/
              veeryyyyyyyyyyyyloooooooooooooonggidentifier =
-- 
cgit v1.2.3


From d6fe6773c959493ed97108e1032b1bd8c1e78081 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 24 Oct 2016 18:18:33 +0200
Subject: Lets Hints/Instances take an optional pattern

In addition to a priority, cleanup the interfaces for passing this
information as well. The pattern, if given, takes priority over the
inferred one.
We only allow Existing Instances gr ... gr | pri. for now, without
pattern, as before.
Make the API compatible to 8.5 as well.
---
 test-suite/success/Hints.v | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index 89b8bd7ac1..91edc06bfa 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -8,6 +8,10 @@ Hint Unfold eq_sym: core.
 Hint Constructors eq: foo bar.
 Hint Extern 3 (_ = _) => apply eq_refl: foo bar.
 
+Hint Resolve eq_refl | 4 (_ = _) : baz.
+Hint Resolve eq_sym eq_trans : baz.
+Hint Extern 3 (_ = _) => apply eq_sym : baz.
+
 (* Old-style syntax *)
 Hint Resolve eq_refl eq_sym.
 Hint Resolve eq_refl eq_sym: foo.
@@ -105,4 +109,4 @@ Hint Cut [_* (a_is_b | b_is_c | c_is_d | d_is_e)
 
   Timeout 1 Fail apply _. (* 0.06s *)
 Abort.
-End HintCut.
\ No newline at end of file
+End HintCut.
-- 
cgit v1.2.3


From c5802966f23b9a8dc34f55961d4861997a3df01f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 26 Oct 2016 18:34:13 +0200
Subject: Test new syntax for hints and typeclass options

---
 test-suite/success/Hints.v       | 81 ++++++++++++++++++++++++++++++++++++----
 test-suite/success/Typeclasses.v | 47 +++++++++++++++++++++++
 2 files changed, 121 insertions(+), 7 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index 91edc06bfa..1abe14774c 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -1,4 +1,12 @@
 (* Checks syntax of Hints commands *)
+(* Old-style syntax *)
+Hint Resolve eq_refl eq_sym.
+Hint Resolve eq_refl eq_sym: foo.
+Hint Immediate eq_refl eq_sym.
+Hint Immediate eq_refl eq_sym: foo.
+Hint Unfold fst eq_sym.
+Hint Unfold fst eq_sym: foo.
+
 (* Checks that qualified names are accepted *)
 
 (* New-style syntax *)
@@ -8,17 +16,76 @@ Hint Unfold eq_sym: core.
 Hint Constructors eq: foo bar.
 Hint Extern 3 (_ = _) => apply eq_refl: foo bar.
 
+(* Extended new syntax with patterns *)
 Hint Resolve eq_refl | 4 (_ = _) : baz.
 Hint Resolve eq_sym eq_trans : baz.
 Hint Extern 3 (_ = _) => apply eq_sym : baz.
 
-(* Old-style syntax *)
-Hint Resolve eq_refl eq_sym.
-Hint Resolve eq_refl eq_sym: foo.
-Hint Immediate eq_refl eq_sym.
-Hint Immediate eq_refl eq_sym: foo.
-Hint Unfold fst eq_sym.
-Hint Unfold fst eq_sym: foo.
+Parameter pred : nat -> Prop.
+Parameter pred0 : pred 0.
+Parameter f : nat -> nat.
+Parameter predf : forall n, pred n -> pred (f n).
+
+(* No conversion on let-bound variables and constants in pred (the default) *)
+Hint Resolve pred0 | 1 (pred _) : pred.
+Hint Resolve predf | 0 : pred.
+
+(* Allow full conversion on let-bound variables and constants *)
+Create HintDb predconv discriminated.
+Hint Resolve pred0 | 1 (pred _) : predconv.
+Hint Resolve predf | 0 : predconv.
+
+Goal exists n, pred n.
+  eexists.
+  Fail Timeout 1 typeclasses eauto with pred.
+  Set Typeclasses Filtered Unification.
+  Set Typeclasses Debug Verbosity 2.
+  (* predf is not tried as it doesn't match the goal *)
+  typeclasses eauto with pred.
+Qed.
+
+Parameter predconv : forall n, pred n -> pred (0 + S n).
+
+(* The inferred pattern contains 0 + ?n, syntactic match will fail to see convertible
+ terms *)
+Hint Resolve pred0 : pred2.
+Hint Resolve predconv : pred2.
+
+(** In this database we allow predconv to apply to pred (S _) goals, more generally
+  than the inferred pattern (pred (0 + S _)). *)
+Create HintDb pred2conv discriminated.
+Hint Resolve pred0 : pred2conv.
+Hint Resolve predconv | 1 (pred (S _)) : pred2conv.
+
+Goal pred 3.
+  Fail typeclasses eauto with pred2.
+  typeclasses eauto with pred2conv.
+Abort.
+
+Set Typeclasses Filtered Unification.
+Set Typeclasses Debug Verbosity 2.
+Hint Resolve predconv | 1 (pred _) : pred.
+Hint Resolve predconv | 1 (pred (S _)) : predconv.
+Test Typeclasses Limit Intros.
+Goal pred 3.
+  (* predf is not tried as it doesn't match the goal *)
+  (* predconv is tried but fails as the transparent state doesn't allow
+     unfolding + *)
+  Fail typeclasses eauto with pred.
+  (* Here predconv succeeds as it matches (pred (S _)) and then
+     full unification is allowed *)
+  typeclasses eauto with predconv.
+Qed.
+
+(** The other way around: goal contains redexes instead of instances *)
+Goal exists n, pred (0 + n).
+  eexists.
+  (* predf is applied indefinitely *)
+  Fail Timeout 1 typeclasses eauto with pred.
+  (* pred0 (pred _) matches the goal *)
+  typeclasses eauto with predconv.
+Qed.
+
 
 (* Checks that local names are accepted *)
 Section A.
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 3eaa04144f..651bbf7d28 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -1,3 +1,16 @@
+Module onlyclasses.
+
+  Variable Foo : Type.
+  Variable foo : Foo.
+  Hint Extern 0 Foo => exact foo : typeclass_instances.
+  Goal Foo * Foo.
+    split. shelve.
+    Fail typeclasses eauto.
+    typeclasses eauto with typeclass_instances.
+    Unshelve. typeclasses eauto with typeclass_instances.
+  Abort.
+End onlyclasses.
+
 Module bt.
 Require Import Equivalence.
 
@@ -104,6 +117,40 @@ Section sec.
  Check U (fun x => e x) _.
 End sec.
 
+Module UniqueSolutions.
+  Set Typeclasses Unique Solutions.
+  Class Eq (A : Type) : Set.
+    Instance eqa : Eq nat := {}.
+    Instance eqb : Eq nat := {}.
+
+    Goal Eq nat.
+      try apply _.
+      Fail exactly_once typeclasses eauto.
+    Abort.
+End UniqueSolutions.
+
+
+Module UniqueInstances.
+  (** Optimize proof search on this class by never backtracking on (closed) goals
+      for it. *)
+  Set Typeclasses Unique Instances.
+  Class Eq (A : Type) : Set.
+    Instance eqa : Eq nat := _. constructor. Qed.
+    Instance eqb : Eq nat := {}.
+    Class Foo (A : Type) (e : Eq A) : Set.
+    Instance fooa : Foo _ eqa := {}.
+
+    Tactic Notation "refineu" open_constr(c) := unshelve refine c.
+
+    Set Typeclasses Debug.
+    Goal { e : Eq nat & Foo nat e }.
+      unshelve refineu (existT _ _ _).
+      all:simpl.
+      (** Does not backtrack on the (wrong) solution eqb *)
+      Fail all:typeclasses eauto.
+    Abort.
+End UniqueInstances.
+
 Module IterativeDeepening.
 
   Class A.
-- 
cgit v1.2.3


From a477dca64bb71a98fb92875df438d44d1fe54400 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 26 Oct 2016 19:20:08 +0200
Subject: Fix handling of only_classes at toplevel

---
 test-suite/bugs/closed/3513.v    |  31 +++++++--
 test-suite/success/Typeclasses.v |  30 ++++++++-
 test-suite/success/eauto.v       | 135 +++++++++++++++++++++++++++------------
 3 files changed, 148 insertions(+), 48 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v
index fcdfa0057b..ff515038ec 100644
--- a/test-suite/bugs/closed/3513.v
+++ b/test-suite/bugs/closed/3513.v
@@ -1,4 +1,3 @@
-Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 5752 lines to 3828 lines, then from 2707 lines to 558 lines, then from 472 lines to 168 lines, then from 110 lines to 101 lines, then from 96 lines to 77 lines, then from 80 lines to 64 lines *)
 Require Coq.Setoids.Setoid.
 Import Coq.Setoids.Setoid.
@@ -35,7 +34,7 @@ Local Existing Instance ILFun_Ops.
 Local Existing Instance ILFun_ILogic.
 Definition catOP (P Q: OPred) : OPred := admit.
 Add Parametric Morphism : catOP with signature lentails ==> lentails ==> lentails as catOP_entails_m.
-admit.
+apply admit.
 Defined.
 Definition catOPA (P Q R : OPred) : catOP (catOP P Q) R -|- catOP P (catOP Q R) := admit.
 Class IsPointed (T : Type) := point : T.
@@ -69,8 +68,26 @@ Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred)
     pose P;
     refine (P _ _)
   end; unfold Basics.flip.
-  2: solve [ apply reflexivity ].
-  Undo.
-  2: reflexivity. (* Toplevel input, characters 18-29:
-Error:
-Tactic failure: The relation lentails is not a declared reflexive relation. Maybe you need to require the Setoid library. *)
\ No newline at end of file
+  Focus 2.
+  Set Typeclasses Debug.
+  Set Typeclasses Legacy Resolution.
+  apply reflexivity.
+  (* Debug: 1.1: apply @IsPointed_catOP on
+(IsPointed (exists x0 : Actions, (catOP ?Goal O2 : OPred) x0))
+Debug: 1.1.1.1: apply OPred_inhabited on (IsPointed (exists x0 : Actions, ?Goal x0))
+Debug: 1.1.2.1: apply OPred_inhabited on (IsPointed (exists x : Actions, O2 x))
+Debug: 2.1: apply @Equivalence_Reflexive on (Reflexive lentails)
+Debug: 2.1.1: no match for (Equivalence lentails) , 5 possibilities
+Debug: Backtracking after apply @Equivalence_Reflexive
+Debug: 2.2: apply @PreOrder_Reflexive on (Reflexive lentails)
+Debug: 2.2.1.1: apply @lentailsPre on (PreOrder lentails)
+Debug: 2.2.1.1.1.1: apply ILFun_ILogic on (ILogic OPred)
+*)
+  Undo. Unset Typeclasses Legacy Resolution.
+  Test Typeclasses Unique Solutions.
+  Test Typeclasses Unique Instances.
+  Show Existentials.
+  Set Typeclasses Debug Verbosity 2.
+  Set Printing All.
+  Fail apply reflexivity.
+  
\ No newline at end of file
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 651bbf7d28..4581a7ce40 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -5,12 +5,40 @@ Module onlyclasses.
   Hint Extern 0 Foo => exact foo : typeclass_instances.
   Goal Foo * Foo.
     split. shelve.
-    Fail typeclasses eauto.
+    Set Typeclasses Debug.
+    typeclasses eauto.
     typeclasses eauto with typeclass_instances.
     Unshelve. typeclasses eauto with typeclass_instances.
   Abort.
 End onlyclasses.
 
+Module shelve_non_class_subgoals.
+  Variable Foo : Type.
+  Variable foo : Foo.
+  Hint Extern 0 Foo => exact foo : typeclass_instances.
+  Class Bar := {}.
+  Instance bar1 (f:Foo) : Bar.
+
+  Typeclasses eauto := debug.
+  Set Typeclasses Debug Verbosity 2.
+  Goal Bar.
+    (* Solution has shelved subgoals *)
+    Fail typeclasses eauto.
+  Abort.
+End shelve_non_class_subgoals.
+
+Module shelve_non_class_subgoals2.
+  Class Bar := {}.
+
+  Instance bar1 (t:Type) : Bar.
+  Hint Extern 0 => exact True : typeclass_instances.
+  Typeclasses eauto := debug.
+  Goal Bar.
+    Fail typeclasses eauto.
+    debug eauto with typeclass_instances.
+  Qed.  
+End shelve_non_class_subgoals2.
+
 Module bt.
 Require Import Equivalence.
 
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index 4db547f4e4..9bcecfe1f3 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -5,7 +5,6 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-Require Import List.
 
 Class A (A : Type).
   Instance an: A nat.
@@ -31,6 +30,8 @@ Defined.
 
 Hint Extern 0 (_ /\ _) => constructor : typeclass_instances.
 
+Existing Class and.
+
 Goal exists (T : Type) (t : T), A T /\ B T t.
 Proof.
   eexists. eexists. typeclasses eauto.
@@ -46,7 +47,7 @@ Class C {T} `(a : A T) (t : T).
 Require Import Classes.Init.
 Hint Extern 0 { x : ?A & _ } =>
   unshelve class_apply @existT : typeclass_instances.
-
+Existing Class sigT.
 Set Typeclasses Debug.
 Instance can: C an 0.
 (* Backtrack on instance implementation *)
@@ -63,41 +64,6 @@ Proof.
 Defined.
   
 
-Parameter in_list : list (nat * nat) -> nat -> Prop.
-Definition not_in_list (l : list (nat * nat)) (n : nat) : Prop :=
-  ~ in_list l n.
-
-(* Hints Unfold not_in_list. *)
-
-Axiom
-  lem1 :
-    forall (l1 l2 : list (nat * nat)) (n : nat),
-    not_in_list (l1 ++ l2) n -> not_in_list l1 n.
-
-Axiom
-  lem2 :
-    forall (l1 l2 : list (nat * nat)) (n : nat),
-    not_in_list (l1 ++ l2) n -> not_in_list l2 n.
-
-Axiom
-  lem3 :
-    forall (l : list (nat * nat)) (n p q : nat),
-    not_in_list ((p, q) :: l) n -> not_in_list l n.
-
-Axiom
-  lem4 :
-    forall (l1 l2 : list (nat * nat)) (n : nat),
-    not_in_list l1 n -> not_in_list l2 n -> not_in_list (l1 ++ l2) n.
-
-Hint Resolve lem1 lem2 lem3 lem4: essai.
-
-Goal
-forall (l : list (nat * nat)) (n p q : nat),
-not_in_list ((p, q) :: l) n -> not_in_list l n.
-  intros.
-  eauto with essai.
-Qed.
-
 (* Example from Nicolas Magaud on coq-club - Jul 2000 *)
 
 Definition Nat : Set := nat.
@@ -126,6 +92,9 @@ Qed.
   Full backtracking on dependent subgoals.
  *)
 Require Import Coq.Classes.Init.
+
+Module NTabareau.
+
 Set Typeclasses Dependency Order.
 Unset Typeclasses Iterative Deepening.
 Notation "x .1" := (projT1 x) (at level 3).
@@ -149,7 +118,8 @@ Hint Extern 5 (Bar ?D.1) =>
 Hint Extern 5 (Qux ?D.1) =>
     destruct D; simpl : typeclass_instances.
 
-Hint Extern 1 myType => unshelve refine (fooTobar _ _).1 : typeclass_instances.
+Hint Extern 1 myType =>
+  unshelve refine (fooTobar _ _).1 : typeclass_instances.
 
 Hint Extern 1 myType => unshelve refine (barToqux _ _).1 : typeclass_instances.
 
@@ -158,8 +128,93 @@ Hint Extern 0 { x : _ & _ } => simple refine (existT _ _ _) : typeclass_instance
 Unset Typeclasses Debug.
 Definition trivial a (H : Foo a) : {b : myType & Qux b}. 
 Proof.
-  Time typeclasses eauto 10.
+  Time typeclasses eauto 10 with typeclass_instances.
   Undo. Set Typeclasses Iterative Deepening.
-  Time typeclasses eauto.
+  Time typeclasses eauto with typeclass_instances.
 Defined.
 
+End NTabareau.
+
+Module NTabareauClasses.
+
+Set Typeclasses Dependency Order.
+Unset Typeclasses Iterative Deepening.
+Notation "x .1" := (projT1 x) (at level 3).
+Notation "x .2" := (projT2 x) (at level 3).
+
+Parameter myType: Type. 
+Existing Class myType.
+
+Class Foo (a:myType) := {}.
+
+Class Bar (a:myType) := {}.
+
+Class Qux (a:myType) := {}.
+
+Parameter fooTobar : forall a (H : Foo a), {b: myType & Bar b}.
+
+Parameter barToqux : forall a (H : Bar a), {b: myType & Qux b}.
+
+Hint Extern 5 (Bar ?D.1) =>
+    destruct D; simpl : typeclass_instances.
+
+Hint Extern 5 (Qux ?D.1) =>
+    destruct D; simpl : typeclass_instances.
+
+Hint Extern 1 myType =>
+  unshelve notypeclasses refine (fooTobar _ _).1 : typeclass_instances.
+
+Hint Extern 1 myType =>
+  unshelve notypeclasses refine (barToqux _ _).1 : typeclass_instances.
+
+Hint Extern 0 { x : _ & _ } =>
+  unshelve notypeclasses refine (existT _ _ _) : typeclass_instances.
+
+Unset Typeclasses Debug.
+
+Definition trivial a (H : Foo a) : {b : myType & Qux b}. 
+Proof.
+  Time typeclasses eauto 10 with typeclass_instances.
+  Undo. Set Typeclasses Iterative Deepening.
+  Time typeclasses eauto with typeclass_instances.
+Defined.
+
+End NTabareauClasses.
+
+
+Require Import List.
+
+Parameter in_list : list (nat * nat) -> nat -> Prop.
+Definition not_in_list (l : list (nat * nat)) (n : nat) : Prop :=
+  ~ in_list l n.
+
+(* Hints Unfold not_in_list. *)
+
+Axiom
+  lem1 :
+    forall (l1 l2 : list (nat * nat)) (n : nat),
+    not_in_list (l1 ++ l2) n -> not_in_list l1 n.
+
+Axiom
+  lem2 :
+    forall (l1 l2 : list (nat * nat)) (n : nat),
+    not_in_list (l1 ++ l2) n -> not_in_list l2 n.
+
+Axiom
+  lem3 :
+    forall (l : list (nat * nat)) (n p q : nat),
+    not_in_list ((p, q) :: l) n -> not_in_list l n.
+
+Axiom
+  lem4 :
+    forall (l1 l2 : list (nat * nat)) (n : nat),
+    not_in_list l1 n -> not_in_list l2 n -> not_in_list (l1 ++ l2) n.
+
+Hint Resolve lem1 lem2 lem3 lem4: essai.
+
+Goal
+forall (l : list (nat * nat)) (n p q : nat),
+not_in_list ((p, q) :: l) n -> not_in_list l n.
+  intros.
+  eauto with essai.
+Qed.
-- 
cgit v1.2.3


From 98305374e2fdec4b64d7d086ddca0c4e812b178e Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 29 Oct 2016 11:51:38 +0200
Subject: typeclasses eauto Implem/doc of shelving strategy

Now [typeclasses eauto] mimicks what happens during resolution
faithfully, and the shelving behavior/requirements for a successful
proof-search are documented.
---
 test-suite/success/Typeclasses.v | 17 +++++++++--------
 test-suite/success/bteauto.v     | 10 +++++++---
 test-suite/success/eauto.v       |  1 +
 3 files changed, 17 insertions(+), 11 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 4581a7ce40..6885717ec5 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -6,10 +6,10 @@ Module onlyclasses.
   Goal Foo * Foo.
     split. shelve.
     Set Typeclasses Debug.
-    typeclasses eauto.
+    Fail typeclasses eauto.
     typeclasses eauto with typeclass_instances.
     Unshelve. typeclasses eauto with typeclass_instances.
-  Abort.
+  Qed.
 End onlyclasses.
 
 Module shelve_non_class_subgoals.
@@ -22,22 +22,23 @@ Module shelve_non_class_subgoals.
   Typeclasses eauto := debug.
   Set Typeclasses Debug Verbosity 2.
   Goal Bar.
-    (* Solution has shelved subgoals *)
+    (* Solution has shelved subgoals (of non typeclass type) *)
     Fail typeclasses eauto.
   Abort.
 End shelve_non_class_subgoals.
 
-Module shelve_non_class_subgoals2.
+Module Leivantex2PR339.
+  (** Was a bug preventing to find hints associated with no pattern *)
   Class Bar := {}.
-
   Instance bar1 (t:Type) : Bar.
   Hint Extern 0 => exact True : typeclass_instances.
   Typeclasses eauto := debug.
   Goal Bar.
     Fail typeclasses eauto.
-    debug eauto with typeclass_instances.
-  Qed.  
-End shelve_non_class_subgoals2.
+    Set Typeclasses Debug Verbosity 2.
+    typeclasses eauto with typeclass_instances.
+  Qed.
+End Leivantex2PR339.
 
 Module bt.
 Require Import Equivalence.
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index bb1cf06541..f97f764b4d 100644
--- a/test-suite/success/bteauto.v
+++ b/test-suite/success/bteauto.v
@@ -8,7 +8,7 @@ Module Backtracking.
   Qed.
   
   Arguments foo A : clear implicits.
-  
+  Require Import Program.Tactics.
   Example find42 : exists n, n = 42.
   Proof.
     eexists.
@@ -20,9 +20,13 @@ Module Backtracking.
     Fail reflexivity. 
     Undo 2.
     (* Without multiple successes it fails *)
-    Fail all:((once typeclasses eauto) + apply eq_refl).
+    Set Typeclasses Debug Verbosity 2.
+    Fail all:((once (typeclasses eauto with typeclass_instances))
+              + apply eq_refl).
     (* Does backtrack if other goals fail *)
-    all:((typeclasses eauto) + reflexivity).
+    all:[> typeclasses eauto + reflexivity .. ].
+    Undo 1.
+    all:(typeclasses eauto + reflexivity). (* Note "+" is a focussing combinator *)
     Show Proof.  
   Qed.
 
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index 9bcecfe1f3..160f2d9deb 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -176,6 +176,7 @@ Definition trivial a (H : Foo a) : {b : myType & Qux b}.
 Proof.
   Time typeclasses eauto 10 with typeclass_instances.
   Undo. Set Typeclasses Iterative Deepening.
+  (* Much faster in iteratove deepening mode *)
   Time typeclasses eauto with typeclass_instances.
 Defined.
 
-- 
cgit v1.2.3


From 0ab187ee578f0ef49ecf484278b8d3569630ee48 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 29 Oct 2016 11:55:29 +0200
Subject: Fixed bug #4095.

---
 test-suite/bugs/closed/4095.v | 87 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 87 insertions(+)
 create mode 100644 test-suite/bugs/closed/4095.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4095.v b/test-suite/bugs/closed/4095.v
new file mode 100644
index 0000000000..83d4ed69d4
--- /dev/null
+++ b/test-suite/bugs/closed/4095.v
@@ -0,0 +1,87 @@
+(* File reduced by coq-bug-finder from original input, then from 5752 lines to 3828 lines, then from 2707 lines to 558 lines, then from 472 lines to 168 lines, then from 110 lines to 101 lines, then from 96 lines to 77 lines, then from 80 lines to 64 lines, then from 92 lines to 79 lines *)
+(* coqc version 8.5beta1 (February 2015) compiled on Feb 23 2015 18:32:3 with OCaml 4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (ebfc19d792492417b129063fb511aa423e9d9e08) *)
+Require Import TestSuite.admit.
+Require Import Coq.Setoids.Setoid.
+Generalizable All Variables.
+Axiom admit : forall {T}, T.
+Class Equiv (A : Type) := equiv : relation A.
+Class type (A : Type) {e : Equiv A} := eq_equiv : Equivalence equiv.
+Class ILogicOps Frm := { lentails: relation Frm;
+                         ltrue: Frm;
+                         land: Frm -> Frm -> Frm;
+                         lor: Frm -> Frm -> Frm }.
+Infix "|--"  := lentails (at level 79, no associativity).
+Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }.
+Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P.
+Infix "-|-"  := lequiv (at level 85, no associativity).
+Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit.
+Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }.
+Section ILogic_Fun.
+  Context (T: Type) `{TType: type T}.
+  Context `{IL: ILogic Frm}.
+  Local Instance ILFun_Ops : ILogicOps (@ILFunFrm T _ Frm _) := admit.
+  Definition ILFun_ILogic : ILogic (@ILFunFrm T _ Frm _) := admit.
+End ILogic_Fun.
+Implicit Arguments ILFunFrm [[ILOps] [e]].
+Instance ILogicOps_Prop : ILogicOps Prop | 2 := {| lentails P Q := (P : Prop) -> Q;
+                                                   ltrue        := True;
+                                                   land     P Q := P /\ Q;
+                                                   lor      P Q := P \/ Q |}.
+Axiom Action : Set.
+Definition Actions := list Action.
+Instance ActionsEquiv : Equiv Actions := { equiv a1 a2 := a1 = a2 }.
+Definition OPred := ILFunFrm Actions Prop.
+Local Existing Instance ILFun_Ops.
+Local Existing Instance ILFun_ILogic.
+Definition catOP (P Q: OPred) : OPred := admit.
+Add Parametric Morphism : catOP with signature lentails ==> lentails ==> lentails as catOP_entails_m.
+admit.
+Defined.
+Definition catOPA (P Q R : OPred) : catOP (catOP P Q) R -|- catOP P (catOP Q R) := admit.
+Class IsPointed (T : Type) := point : T.
+Notation IsPointed_OPred P := (IsPointed (exists x : Actions, (P : OPred) x)).
+Record PointedOPred := mkPointedOPred {
+                           OPred_pred :> OPred;
+                           OPred_inhabited: IsPointed_OPred OPred_pred
+                         }.
+Existing Instance OPred_inhabited.
+Canonical Structure default_PointedOPred O `{IsPointed_OPred O} : PointedOPred
+  := {| OPred_pred := O ; OPred_inhabited := _ |}.
+Instance IsPointed_catOP `{IsPointed_OPred P, IsPointed_OPred Q} : IsPointed_OPred (catOP P Q) := admit.
+Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred)
+            (tr : T -> T) (O2 : PointedOPred) (x : T)
+            (H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0),
+     exists e1 e2,
+       catOP (O0 e1) (OPred_pred e2) |-- catOP (O1 x) O2.
+  intros; do 2 esplit.
+  rewrite <- catOPA.
+  lazymatch goal with
+  | |- ?R (?f ?a ?b) (?f ?a' ?b') =>
+    let P := constr:(fun H H' => @Morphisms.proper_prf (OPred -> OPred -> OPred)
+         (@Morphisms.respectful OPred (OPred -> OPred)
+            (@lentails OPred
+               (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop))
+            (@lentails OPred
+               (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop) ==>
+             @lentails OPred
+               (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop))) catOP
+         catOP_entails_m_Proper a a' H b b' H') in
+    pose P;
+    refine (P _ _)
+  end.
+  Undo.
+  lazymatch goal with
+  | |- ?R (?f ?a ?b) (?f ?a' ?b') =>
+    let P := constr:(fun H H' => Morphisms.proper_prf a a' H b b' H') in
+    set(p:=P)
+  end. (* Toplevel input, characters 15-182:
+Error: Cannot infer an instance of type
+"PointedOPred" for the variable p in environment:
+T : Type
+O0 : T -> OPred
+O1 : T -> PointedOPred
+tr : T -> T
+O2 : PointedOPred
+x0 : T
+H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0 *)
\ No newline at end of file
-- 
cgit v1.2.3


From d51c384e52003668bd97ca44da77a14c91e5cb14 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 29 Oct 2016 12:37:46 +0200
Subject: Fix test-suite files relying on tcs bugs

- One was expecting shelved goals to remain after resolution (from refine).
- The other too were relying on the wrong classification of subgoals
  as typeclass subgoals at toplevel.
---
 test-suite/bugs/closed/3699.v | 12 ++++--------
 test-suite/bugs/closed/4863.v |  7 ++++---
 test-suite/success/bteauto.v  |  2 +-
 3 files changed, 9 insertions(+), 12 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v
index 8dadc2419c..efa4325264 100644
--- a/test-suite/bugs/closed/3699.v
+++ b/test-suite/bugs/closed/3699.v
@@ -34,8 +34,7 @@ Module NonPrim.
   : forall b:B, P b.
   Proof.
     intros b.
-    unshelve (refine (pr1 (isconnected_elim _ _))).
-    exact b.
+    unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))).
     intro x.
     exact (transport P x.2 (d x.1)).
   Defined.
@@ -47,8 +46,7 @@ Module NonPrim.
   : forall b:B, P b.
   Proof.
     intros b.
-    unshelve (refine (pr1 (isconnected_elim _ _))).
-    exact b.
+    unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))).
     intros [a p].
     exact (transport P p (d a)).
   Defined.
@@ -111,8 +109,7 @@ Module Prim.
   : forall b:B, P b.
   Proof.
     intros b.
-    unshelve (refine (pr1 (isconnected_elim _ _))).
-    exact b.
+    unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))).
     intro x.
     exact (transport P x.2 (d x.1)).
   Defined.
@@ -124,8 +121,7 @@ Module Prim.
   : forall b:B, P b.
   Proof.
     intros b.
-    unshelve (refine (pr1 (isconnected_elim _ _))).
-    exact b.
+    unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))).
     intros [a p].
     exact (transport P p (d a)).
   Defined.
diff --git a/test-suite/bugs/closed/4863.v b/test-suite/bugs/closed/4863.v
index e884355fde..1e47f2957b 100644
--- a/test-suite/bugs/closed/4863.v
+++ b/test-suite/bugs/closed/4863.v
@@ -3,14 +3,14 @@ Require Import Classes.DecidableClass.
 Inductive Foo : Set :=
 | foo1 | foo2.
 
-Instance Decidable_sumbool : forall P, {P}+{~P} -> Decidable P.
+Lemma Decidable_sumbool : forall P, {P}+{~P} -> Decidable P.
 Proof.
   intros P H.
   refine (Build_Decidable _ (if H then true else false) _).
   intuition congruence.
 Qed.
 
-Hint Extern 100 ({?A = ?B}+{~ ?A = ?B}) => abstract (abstract (abstract (decide equality))) : typeclass_instances.
+Hint Extern 100 (Decidable (?A = ?B)) => abstract (abstract (abstract (apply Decidable_sumbool; decide equality))) : typeclass_instances.
 
 Goal forall (a b : Foo), {a=b}+{a<>b}.
 intros.
@@ -21,7 +21,8 @@ Check ltac:(abstract (exact I)) : True.
 
 Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b).
 intros.
-split. typeclasses eauto. typeclasses eauto. Qed.
+split. typeclasses eauto. 
+typeclasses eauto. Qed.
 
 Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b).
 intros.
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index f97f764b4d..3178c6fc15 100644
--- a/test-suite/success/bteauto.v
+++ b/test-suite/success/bteauto.v
@@ -1,3 +1,4 @@
+Require Import Program.Tactics.
 Module Backtracking.
   Class A := { foo : nat }.
 
@@ -8,7 +9,6 @@ Module Backtracking.
   Qed.
   
   Arguments foo A : clear implicits.
-  Require Import Program.Tactics.
   Example find42 : exists n, n = 42.
   Proof.
     eexists.
-- 
cgit v1.2.3


From 22dfbff296cf03b6fab2bcec4eb5f9cf6ee8368c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 4 Nov 2016 15:55:52 +0100
Subject: Fix #3441 Use pf_get_type_of to avoid blowup

... in pose proof of large proof terms
---
 test-suite/bugs/closed/3441.v | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)
 create mode 100644 test-suite/bugs/closed/3441.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3441.v b/test-suite/bugs/closed/3441.v
new file mode 100644
index 0000000000..50d2978077
--- /dev/null
+++ b/test-suite/bugs/closed/3441.v
@@ -0,0 +1,23 @@
+Axiom f : nat -> nat -> nat.
+Fixpoint do_n (n : nat) (k : nat) :=
+  match n with
+    | 0 => k
+    | S n' => do_n n' (f k k)
+  end.
+
+Notation big := (_ = _).
+Axiom k : nat.
+Goal True.
+Timeout 1 let H := fresh "H" in
+     let x := constr:(let n := 17 in do_n n = do_n n) in
+     let y := (eval lazy in x) in 
+     pose proof y as H. (* Finished transaction in 1.102 secs (1.084u,0.016s) (successful) *)
+Timeout 1 let H := fresh "H" in
+     let x := constr:(let n := 17 in do_n n = do_n n) in
+     let y := (eval lazy in x) in
+     pose y as H; clearbody H. (* Finished transaction in 0.412 secs (0.412u,0.s) (successful) *)
+
+Timeout 1 Time let H := fresh "H" in
+     let x := constr:(let n := 17 in do_n n = do_n n) in
+     let y := (eval lazy in x) in
+     assert (H := y). (* Finished transaction in 1.19 secs (1.164u,0.024s) (successful) *)
\ No newline at end of file
-- 
cgit v1.2.3


From 94bdd90bacc4d4a92b79bbe0db532e523fbcbce8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 4 Nov 2016 17:03:04 +0100
Subject: Test for #4966 ("auto" wrongly seen as "auto with *" when in position
 of ident).

---
 test-suite/bugs/closed/4966.v | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 test-suite/bugs/closed/4966.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4966.v b/test-suite/bugs/closed/4966.v
new file mode 100644
index 0000000000..bd93cdc858
--- /dev/null
+++ b/test-suite/bugs/closed/4966.v
@@ -0,0 +1,10 @@
+(* Interpretation of auto as an argument of an ltac function (i.e. as an ident) was wrongly "auto with *" *)
+
+Axiom proof_admitted : False.
+Hint Extern 0 => case proof_admitted : unused.
+Ltac do_tac tac := tac.
+
+Goal False.
+  Set Ltac Profiling.
+  Fail solve [ do_tac auto ].
+Abort.
-- 
cgit v1.2.3


From e6edb3319c850cc7e30e5c31b0bfbf16c5c1a32c Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 7 Nov 2016 08:41:21 +0100
Subject: More explicit name for status of unification constraints.

---
 test-suite/bugs/closed/2310.v       | 2 +-
 test-suite/bugs/closed/3647.v       | 2 +-
 test-suite/bugs/closed/4416.v       | 2 +-
 test-suite/bugs/closed/5149.v       | 2 +-
 test-suite/output/unifconstraints.v | 2 +-
 5 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/2310.v b/test-suite/bugs/closed/2310.v
index 9fddede7e9..7fae328715 100644
--- a/test-suite/bugs/closed/2310.v
+++ b/test-suite/bugs/closed/2310.v
@@ -15,7 +15,7 @@ Definition replace a (y:Nest (prod a a)) : a = a -> Nest a.
    leave P as subgoal or choose itself one solution *)
 
   intros. Fail refine (Cons (cast H _ y)).
-  Unset Use Unification Heuristics. (* Keep the unification constraint around *)
+  Unset Solve Unification Constraints. (* Keep the unification constraint around *)
   refine (Cons (cast H _ y)).
   intros.
   refine (Nest (prod X X)). Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3647.v b/test-suite/bugs/closed/3647.v
index f2cd41203c..f5a22bd508 100644
--- a/test-suite/bugs/closed/3647.v
+++ b/test-suite/bugs/closed/3647.v
@@ -651,4 +651,4 @@ Goal    forall (ptest : program) (cond : Condition) (value : bool)
   Grab Existential Variables.
   subst_body; simpl.
   Fail refine (all_behead (projT2 _)).
-  Unset Use Unification Heuristics. refine (all_behead (projT2 _)).
+  Unset Solve Unification Constraints. refine (all_behead (projT2 _)).
diff --git a/test-suite/bugs/closed/4416.v b/test-suite/bugs/closed/4416.v
index afe8c62ed0..3189685ec0 100644
--- a/test-suite/bugs/closed/4416.v
+++ b/test-suite/bugs/closed/4416.v
@@ -1,4 +1,4 @@
 Goal exists x, x.
-Unset Use Unification Heuristics.
+Unset Solve Unification Constraints.
 unshelve refine (ex_intro _ _ _); match goal with _ => refine (_ _) end.
 (* Error: Incorrect number of goals (expected 2 tactics). *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/5149.v b/test-suite/bugs/closed/5149.v
index 01b9d158fe..684dba1961 100644
--- a/test-suite/bugs/closed/5149.v
+++ b/test-suite/bugs/closed/5149.v
@@ -40,7 +40,7 @@ Proof.
   Fail solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption) ].
   solve [eapply interpf_SmartVarVar; subst; eassumption].
   Undo.
-  Unset Use Unification Heuristics.
+  Unset Solve Unification Constraints.
   (* User control of when constraints are solved *)
   solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption); solve_constraints ].
 Qed.
diff --git a/test-suite/output/unifconstraints.v b/test-suite/output/unifconstraints.v
index c7fb82adac..b9413a4ac2 100644
--- a/test-suite/output/unifconstraints.v
+++ b/test-suite/output/unifconstraints.v
@@ -1,5 +1,5 @@
 (* Set Printing Existential Instances. *)
-Unset Use Unification Heuristics.
+Unset Solve Unification Constraints.
 Axiom veeryyyyyyyyyyyyloooooooooooooonggidentifier : nat.
 Goal True /\ True /\ True \/
              veeryyyyyyyyyyyyloooooooooooooonggidentifier =
-- 
cgit v1.2.3


From 3308336f1a412cb2a218e3a70a171cb7ff88bfbe Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sun, 6 Nov 2016 13:29:18 +0100
Subject: Fix #5182: "Arguments names must be distinct." is bogus and
 underinformative

---
 test-suite/output/Arguments_renaming.out | 10 ++++------
 test-suite/output/Arguments_renaming.v   |  2 +-
 2 files changed, 5 insertions(+), 7 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 9d90de47cb..b084ad4984 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,6 +1,5 @@
 The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be
-specified.
+Error: To rename arguments the "rename" flag must be specified.
 Argument A renamed to B.
 File "stdin", line 2, characters 0-25:
 Warning: This command is just asserting the names of arguments of identity.
@@ -104,16 +103,15 @@ Expands to: Constant Top.myplus
 @myplus
      : forall Z : Type, Z -> nat -> nat -> nat
 The command has indeed failed with message:
-Error: Arguments lists should agree on names they provide.
+Error: Argument lists should agree on the names they provide.
 The command has indeed failed with message:
 Error: Sequences of implicit arguments must be of different lengths.
 The command has indeed failed with message:
-Error: Arguments names must be distinct.
+Error: Some argument names are duplicated: F
 The command has indeed failed with message:
 Error: Argument z cannot be declared implicit.
 The command has indeed failed with message:
 Error: Extra arguments: y.
 The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be
-specified.
+Error: To rename arguments the "rename" flag must be specified.
 Argument A renamed to R.
diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v
index 2d14c94ac8..0cb331347d 100644
--- a/test-suite/output/Arguments_renaming.v
+++ b/test-suite/output/Arguments_renaming.v
@@ -47,7 +47,7 @@ Check @myplus.
 
 Fail Arguments eq_refl {F g}, [H] k.
 Fail Arguments eq_refl {F}, [F] : rename.
-Fail Arguments eq_refl {F F}, [F] F.
+Fail Arguments eq_refl {F F}, [F] F : rename.
 Fail Arguments eq {F} x [z] : rename.
 Fail Arguments eq {F} x z y.
 Fail Arguments eq {R} s t.
-- 
cgit v1.2.3


From 75b49b14987ec9467ec5916609da8ce3136d3e11 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sun, 6 Nov 2016 13:46:25 +0100
Subject: Fix #5181: [Arguments] no longer correctly checks the length of
 arguments lists

---
 test-suite/bugs/closed/5181.v | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 test-suite/bugs/closed/5181.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5181.v b/test-suite/bugs/closed/5181.v
new file mode 100644
index 0000000000..0e6d471979
--- /dev/null
+++ b/test-suite/bugs/closed/5181.v
@@ -0,0 +1,3 @@
+Definition foo (x y : nat) := x.
+Fail Arguments foo {_} : assert.
+
-- 
cgit v1.2.3


From a279547e2d4e6cad75c266e4a9e436b524f5df99 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 10 Nov 2016 11:45:59 +0100
Subject: Updating a comment in test-suite.

---
 test-suite/output/PatternsInBinders.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v
index fff86d6fae..6fa357a90c 100644
--- a/test-suite/output/PatternsInBinders.v
+++ b/test-suite/output/PatternsInBinders.v
@@ -58,7 +58,7 @@ Definition F '(n,p) : Type := (Fin n * Fin p)%type.
 Definition both_z '(n,p) : F (n,p) := (Z _,Z _).
 Print both_z.
 
-(** These tests show examples which do not factorize binders *)
+(** Test factorization of binders *)
 
 Check fun '((x,y) : A*B) '(z,t) => swap (x,y) = (z,t).
 Check forall '(x,y) '((z,t) : B*A), swap (x,y) = (z,t).
-- 
cgit v1.2.3


From 4b8f19c58a2b6cc841db2c011d23aa8106211fd6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 15 Nov 2016 13:53:57 +0100
Subject: Revert part of a477dc, disallow_shelved

In only_classes mode we do not try to implement a stricter semantics for
shelved goals in 8.6. Leaving this for 8.7.
Update the documentation as well.
Remove a spurious printf call as well.

Fix test-suite now that shelved goals are allowed
---
 test-suite/bugs/closed/3513.v    | 3 ++-
 test-suite/bugs/closed/4095.v    | 4 ++--
 test-suite/success/Typeclasses.v | 2 +-
 test-suite/success/bteauto.v     | 6 +++---
 4 files changed, 8 insertions(+), 7 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v
index ff515038ec..9ed0926a66 100644
--- a/test-suite/bugs/closed/3513.v
+++ b/test-suite/bugs/closed/3513.v
@@ -89,5 +89,6 @@ Debug: 2.2.1.1.1.1: apply ILFun_ILogic on (ILogic OPred)
   Show Existentials.
   Set Typeclasses Debug Verbosity 2.
   Set Printing All.
-  Fail apply reflexivity.
+  (* As in 8.5, allow a shelved subgoal to remain *)
+  apply reflexivity.
   
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4095.v b/test-suite/bugs/closed/4095.v
index 83d4ed69d4..ffd33d3813 100644
--- a/test-suite/bugs/closed/4095.v
+++ b/test-suite/bugs/closed/4095.v
@@ -1,10 +1,10 @@
 (* File reduced by coq-bug-finder from original input, then from 5752 lines to 3828 lines, then from 2707 lines to 558 lines, then from 472 lines to 168 lines, then from 110 lines to 101 lines, then from 96 lines to 77 lines, then from 80 lines to 64 lines, then from 92 lines to 79 lines *)
 (* coqc version 8.5beta1 (February 2015) compiled on Feb 23 2015 18:32:3 with OCaml 4.01.0
    coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (ebfc19d792492417b129063fb511aa423e9d9e08) *)
-Require Import TestSuite.admit.
 Require Import Coq.Setoids.Setoid.
 Generalizable All Variables.
 Axiom admit : forall {T}, T.
+Ltac admit := apply admit.
 Class Equiv (A : Type) := equiv : relation A.
 Class type (A : Type) {e : Equiv A} := eq_equiv : Equivalence equiv.
 Class ILogicOps Frm := { lentails: relation Frm;
@@ -71,7 +71,7 @@ Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred)
     refine (P _ _)
   end.
   Undo.
-  lazymatch goal with
+  Fail lazymatch goal with
   | |- ?R (?f ?a ?b) (?f ?a' ?b') =>
     let P := constr:(fun H H' => Morphisms.proper_prf a a' H b b' H') in
     set(p:=P)
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 6885717ec5..5557ba8379 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -6,7 +6,7 @@ Module onlyclasses.
   Goal Foo * Foo.
     split. shelve.
     Set Typeclasses Debug.
-    Fail typeclasses eauto.
+    Fail (unshelve typeclasses eauto); fail.
     typeclasses eauto with typeclass_instances.
     Unshelve. typeclasses eauto with typeclass_instances.
   Qed.
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index 3178c6fc15..0af367781a 100644
--- a/test-suite/success/bteauto.v
+++ b/test-suite/success/bteauto.v
@@ -24,9 +24,9 @@ Module Backtracking.
     Fail all:((once (typeclasses eauto with typeclass_instances))
               + apply eq_refl).
     (* Does backtrack if other goals fail *)
-    all:[> typeclasses eauto + reflexivity .. ].
+    all:[> (unshelve typeclasses eauto; fail) + reflexivity .. ].
     Undo 1.
-    all:(typeclasses eauto + reflexivity). (* Note "+" is a focussing combinator *)
+    all:((unshelve typeclasses eauto; fail) + reflexivity). (* Note "+" is a focussing combinator *)
     Show Proof.  
   Qed.
 
@@ -66,7 +66,7 @@ Module Backtracking.
       unshelve evar (t : A). all:cycle 1.
       refine (@ex_intro _ _ t _).
       all:cycle 1.
-      all:(typeclasses eauto + reflexivity).
+      all:((unshelve typeclasses eauto; fail) + reflexivity).
     Qed.      
   End Leivant.
 End Backtracking.
-- 
cgit v1.2.3


From 09fd1e8b5e810bae0e50ecd4901cd7c8f1464f4a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 16 Nov 2016 10:45:25 +0100
Subject: Revert more of a477dc for good measure

We stop failing automatically on non-declared-class nested or toplevel
subgoals as in 8.5, instead of the previous a477dc behavior of shelving
those goals and failing if shelved goals remained at the end of
resolution. It means typeclass resolution during refinement is closer to
all:typeclasses eauto. Hints in typeclass_instances for non-declared
classes can be used during resolution of _nested_ subgoals when it is
fired from type-inference, toplevel goals considered in this case are
still only classes (as in 8.5 and before). The code that triggers the
restriction to only declared class subgoals is commented.

Revert changes to test-suite, adding test for #5203, #5198 is fixed too.

Add corresponding tests in the test-suite (that will break if we,
e.g. disallow non-class subgoals) and update the refman accordingly.
---
 test-suite/bugs/closed/5198.v    | 39 ++++++++++++++++++++++++++++++++++
 test-suite/bugs/closed/5203.v    |  5 +++++
 test-suite/success/Typeclasses.v | 46 ++++++++++++++++++++++++++++++++++------
 test-suite/success/bteauto.v     |  6 +++---
 4 files changed, 87 insertions(+), 9 deletions(-)
 create mode 100644 test-suite/bugs/closed/5198.v
 create mode 100644 test-suite/bugs/closed/5203.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5198.v b/test-suite/bugs/closed/5198.v
new file mode 100644
index 0000000000..7254afb429
--- /dev/null
+++ b/test-suite/bugs/closed/5198.v
@@ -0,0 +1,39 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-boot" "-nois") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 286 lines to 
+27 lines, then from 224 lines to 53 lines, then from 218 lines to 56 lines, 
+then from 269 lines to 180 lines, then from 132 lines to 48 lines, then from 
+253 lines to 65 lines, then from 79 lines to 65 lines *)
+(* coqc version 8.6.0 (November 2016) compiled on Nov 12 2016 14:43:52 with 
+OCaml 4.02.3
+   coqtop version jgross-Leopard-WS:/home/jgross/Downloads/coq/coq-v8.6,v8.6 
+(7e992fa784ee6fa48af8a2e461385c094985587d) *)
+Axiom admit : forall {T}, T.
+Set Printing Implicit.
+Inductive nat := O | S (_ : nat).
+Axiom f : forall (_ _ : nat), nat.
+Class ZLikeOps (e : nat)
+  := { LargeT : Type ; SmallT : Type ; CarryAdd : forall (_ _ : LargeT), LargeT 
+}.
+Class BarrettParameters :=
+  { b : nat ; k : nat ; ops : ZLikeOps (f b k) }.
+Axiom barrett_reduce_function_bundled : forall {params : BarrettParameters}
+                                               (_ : @LargeT _ (@ops params)),
+    @SmallT _ (@ops params).
+
+Global Instance ZZLikeOps e : ZLikeOps (f (S O) e)
+  := { LargeT := nat ; SmallT := nat ; CarryAdd x y := y }.
+Definition SRep := nat.
+Local Instance x86_25519_Barrett : BarrettParameters
+  := { b := S O ; k := O ; ops := ZZLikeOps O }.
+Definition SRepAdd : forall (_ _ : SRep), SRep
+  := let v := (fun x y => barrett_reduce_function_bundled (CarryAdd x y)) in
+     v.
+Definition SRepAdd' : forall (_ _ : SRep), SRep
+  := (fun x y => barrett_reduce_function_bundled (CarryAdd x y)).
+(* Error:
+In environment
+x : SRep
+y : SRep
+The term "x" has type "SRep" while it is expected to have type
+ "@LargeT ?e ?ZLikeOps".
+ *)
diff --git a/test-suite/bugs/closed/5203.v b/test-suite/bugs/closed/5203.v
new file mode 100644
index 0000000000..ed137395fc
--- /dev/null
+++ b/test-suite/bugs/closed/5203.v
@@ -0,0 +1,5 @@
+Goal True.
+  Typeclasses eauto := debug.
+  Fail solve [ typeclasses eauto ].
+  Fail typeclasses eauto.
+  
\ No newline at end of file
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 5557ba8379..f62427ef47 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -1,15 +1,28 @@
 Module onlyclasses.
 
+(* In 8.6 we still allow non-class subgoals *)
   Variable Foo : Type.
   Variable foo : Foo.
   Hint Extern 0 Foo => exact foo : typeclass_instances.
   Goal Foo * Foo.
     split. shelve.
     Set Typeclasses Debug.
-    Fail (unshelve typeclasses eauto); fail.
-    typeclasses eauto with typeclass_instances.
-    Unshelve. typeclasses eauto with typeclass_instances.
+    typeclasses eauto.
+    Unshelve. typeclasses eauto.
   Qed.
+
+  Module RJung.
+    Class Foo (x : nat).
+      
+      Instance foo x : x = 2 -> Foo x.
+      Hint Extern 0 (_ = _) => reflexivity : typeclass_instances.
+      Typeclasses eauto := debug.
+      Check (_ : Foo 2).
+
+
+      Fail Definition foo := (_ : 0 = 0).
+
+  End RJung.
 End onlyclasses.
 
 Module shelve_non_class_subgoals.
@@ -17,16 +30,36 @@ Module shelve_non_class_subgoals.
   Variable foo : Foo.
   Hint Extern 0 Foo => exact foo : typeclass_instances.
   Class Bar := {}.
-  Instance bar1 (f:Foo) : Bar.
+  Instance bar1 (f:Foo) : Bar := {}.
 
   Typeclasses eauto := debug.
   Set Typeclasses Debug Verbosity 2.
   Goal Bar.
     (* Solution has shelved subgoals (of non typeclass type) *)
-    Fail typeclasses eauto.
+    typeclasses eauto.
   Abort.
 End shelve_non_class_subgoals.
 
+Module RefineVsNoTceauto.
+
+  Class Foo (A : Type) := foo : A.
+  Instance: Foo nat := { foo := 0 }.
+  Instance: Foo nat := { foo := 42 }.
+  Hint Extern 0 (_ = _) => refine eq_refl : typeclass_instances.
+  Goal exists (f : Foo nat), @foo _ f = 0.
+  Proof.
+    unshelve (notypeclasses refine (ex_intro _ _ _)). 
+    Set Typeclasses Debug. Set Printing All.
+    all:once (typeclasses eauto).
+    Fail idtac. (* Check no subgoals are left *)
+    Undo 3.
+    (** In this case, the (_ = _) subgoal is not considered 
+        by typeclass resolution *)
+    refine (ex_intro _ _ _). Fail reflexivity.
+  Abort.
+
+End RefineVsNoTceauto.
+
 Module Leivantex2PR339.
   (** Was a bug preventing to find hints associated with no pattern *)
   Class Bar := {}.
@@ -34,8 +67,9 @@ Module Leivantex2PR339.
   Hint Extern 0 => exact True : typeclass_instances.
   Typeclasses eauto := debug.
   Goal Bar.
-    Fail typeclasses eauto.
     Set Typeclasses Debug Verbosity 2.
+    typeclasses eauto. (* Relies on resolution of a non-class subgoal *)
+    Undo 1.
     typeclasses eauto with typeclass_instances.
   Qed.
 End Leivantex2PR339.
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index 0af367781a..3178c6fc15 100644
--- a/test-suite/success/bteauto.v
+++ b/test-suite/success/bteauto.v
@@ -24,9 +24,9 @@ Module Backtracking.
     Fail all:((once (typeclasses eauto with typeclass_instances))
               + apply eq_refl).
     (* Does backtrack if other goals fail *)
-    all:[> (unshelve typeclasses eauto; fail) + reflexivity .. ].
+    all:[> typeclasses eauto + reflexivity .. ].
     Undo 1.
-    all:((unshelve typeclasses eauto; fail) + reflexivity). (* Note "+" is a focussing combinator *)
+    all:(typeclasses eauto + reflexivity). (* Note "+" is a focussing combinator *)
     Show Proof.  
   Qed.
 
@@ -66,7 +66,7 @@ Module Backtracking.
       unshelve evar (t : A). all:cycle 1.
       refine (@ex_intro _ _ t _).
       all:cycle 1.
-      all:((unshelve typeclasses eauto; fail) + reflexivity).
+      all:(typeclasses eauto + reflexivity).
     Qed.      
   End Leivant.
 End Backtracking.
-- 
cgit v1.2.3


From 633ed9c528c64dc2daa0b3e83749bc392aab7fd2 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 6 Jun 2016 14:54:23 -0400
Subject: Add test suite files for 4700-4785

I didn't add any test-cases for timing-based bugs (4707, 4768, 4776,
4777, 4779, 4783), nor CoqIDE bugs (4700, 4751, 4752, 4756), nor
bugs about printing (4709, 4711, 4720, 4723, 4734, 4736, 4738, 4741,
4743, 4748, 4749, 4750, 4757, 4758, 4765, 4784).  I'm not sure what to
do with 4712, 4714, 4732, 4740.
---
 test-suite/bugs/closed/4708.v    |  8 ++++
 test-suite/bugs/closed/4718.v    | 15 +++++++
 test-suite/bugs/closed/4722.v    |  1 +
 test-suite/bugs/closed/4722/tata |  1 +
 test-suite/bugs/closed/4727.v    | 10 +++++
 test-suite/bugs/closed/4745.v    | 35 +++++++++++++++
 test-suite/bugs/closed/4772.v    |  6 +++
 test-suite/bugs/opened/4701.v    | 23 ++++++++++
 test-suite/bugs/opened/4717.v    | 19 ++++++++
 test-suite/bugs/opened/4721.v    | 13 ++++++
 test-suite/bugs/opened/4728.v    | 72 ++++++++++++++++++++++++++++++
 test-suite/bugs/opened/4755.v    | 34 +++++++++++++++
 test-suite/bugs/opened/4771.v    | 22 ++++++++++
 test-suite/bugs/opened/4778.v    | 35 +++++++++++++++
 test-suite/bugs/opened/4781.v    | 94 ++++++++++++++++++++++++++++++++++++++++
 15 files changed, 388 insertions(+)
 create mode 100644 test-suite/bugs/closed/4708.v
 create mode 100644 test-suite/bugs/closed/4718.v
 create mode 100644 test-suite/bugs/closed/4722.v
 create mode 120000 test-suite/bugs/closed/4722/tata
 create mode 100644 test-suite/bugs/closed/4727.v
 create mode 100644 test-suite/bugs/closed/4745.v
 create mode 100644 test-suite/bugs/closed/4772.v
 create mode 100644 test-suite/bugs/opened/4701.v
 create mode 100644 test-suite/bugs/opened/4717.v
 create mode 100644 test-suite/bugs/opened/4721.v
 create mode 100644 test-suite/bugs/opened/4728.v
 create mode 100644 test-suite/bugs/opened/4755.v
 create mode 100644 test-suite/bugs/opened/4771.v
 create mode 100644 test-suite/bugs/opened/4778.v
 create mode 100644 test-suite/bugs/opened/4781.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4708.v b/test-suite/bugs/closed/4708.v
new file mode 100644
index 0000000000..ad2e581004
--- /dev/null
+++ b/test-suite/bugs/closed/4708.v
@@ -0,0 +1,8 @@
+(*Doc, it hurts when I poke myself.*)
+
+Notation "'" := 1. (* was:
+Setting notation at level 0.
+Toplevel input, characters 0-18:
+> Notation "'" := 1.
+> ^^^^^^^^^^^^^^^^^^
+Anomaly: Uncaught exception Invalid_argument("index out of bounds"). Please report. *)
diff --git a/test-suite/bugs/closed/4718.v b/test-suite/bugs/closed/4718.v
new file mode 100644
index 0000000000..12a4e8fc1a
--- /dev/null
+++ b/test-suite/bugs/closed/4718.v
@@ -0,0 +1,15 @@
+(*Congruence is weaker than reflexivity when it comes to higher level than necessary equalities:*)
+
+Goal @eq Set nat nat.
+congruence.
+Qed.
+
+Goal @eq Type nat nat.
+congruence. (*bug*)
+Qed.
+
+Variable T : Type.
+
+Goal @eq Type T T.
+congruence.
+Qed.
diff --git a/test-suite/bugs/closed/4722.v b/test-suite/bugs/closed/4722.v
new file mode 100644
index 0000000000..f047624c84
--- /dev/null
+++ b/test-suite/bugs/closed/4722.v
@@ -0,0 +1 @@
+(* -*- coq-prog-args: ("-emacs" "-R" "4722" "Foo") -*- *)
diff --git a/test-suite/bugs/closed/4722/tata b/test-suite/bugs/closed/4722/tata
new file mode 120000
index 0000000000..b38e66e75f
--- /dev/null
+++ b/test-suite/bugs/closed/4722/tata
@@ -0,0 +1 @@
+toto
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4727.v b/test-suite/bugs/closed/4727.v
new file mode 100644
index 0000000000..3854bbffdd
--- /dev/null
+++ b/test-suite/bugs/closed/4727.v
@@ -0,0 +1,10 @@
+(* -*- coq-prog-args: ("-emacs" "-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/4745.v b/test-suite/bugs/closed/4745.v
new file mode 100644
index 0000000000..c090125e64
--- /dev/null
+++ b/test-suite/bugs/closed/4745.v
@@ -0,0 +1,35 @@
+(*I get an Anomaly in the following code.
+
+```*)
+Require Vector.
+
+Module M.
+  Lemma Vector_map_map :
+    forall A B C (f : A -> B) (g : B -> C) n (v : Vector.t A n),
+      Vector.map g (Vector.map f v) = Vector.map (fun a => g (f a)) v.
+  Proof.
+    induction v; simpl; auto using f_equal.
+  Qed.
+
+  Lemma Vector_map_map_transparent :
+    forall A B C (f : A -> B) (g : B -> C) n (v : Vector.t A n),
+      Vector.map g (Vector.map f v) = Vector.map (fun a => g (f a)) v.
+  Proof.
+    induction v; simpl; auto using f_equal.
+  Defined.
+  (* Anomaly: constant not found in kind_of_head: Coq.Vectors.Vector.t_ind. Please report. *)
+
+  (* strangely, explicitly passing the principle to induction works *)
+  Lemma Vector_map_map_transparent' :
+    forall A B C (f : A -> B) (g : B -> C) n (v : Vector.t A n),
+      Vector.map g (Vector.map f v) = Vector.map (fun a => g (f a)) v.
+  Proof.
+    induction v using Vector.t_ind; simpl; auto using f_equal.
+  Defined.
+End M.
+(*```
+
+Changing any of the following things eliminates the Anomaly
+   * moving the lemma out of the module M to the top level
+   * proving the lemma as a Fixpoint instead of using induction
+   * proving the analogous lemma on lists instead of vectors*)
diff --git a/test-suite/bugs/closed/4772.v b/test-suite/bugs/closed/4772.v
new file mode 100644
index 0000000000..c3109fa31c
--- /dev/null
+++ b/test-suite/bugs/closed/4772.v
@@ -0,0 +1,6 @@
+
+Record TruncType := BuildTruncType {
+  trunctype_type : Type
+}.
+
+Fail Arguments BuildTruncType _ _ {_}. (* This should fail *)
diff --git a/test-suite/bugs/opened/4701.v b/test-suite/bugs/opened/4701.v
new file mode 100644
index 0000000000..9286f0f1f0
--- /dev/null
+++ b/test-suite/bugs/opened/4701.v
@@ -0,0 +1,23 @@
+(*Suppose we have*)
+
+  Inductive my_if {A B} : bool -> Type :=
+  | then_case (_ : A) : my_if true
+  | else_case (_ : B) : my_if false.
+  Notation "'If' b 'Then' A 'Else' B" := (@my_if A B b) (at level 10).
+
+(*then here are three inductive type declarations that work:*)
+
+  Inductive I1 :=
+  | i1 (x : I1).
+  Inductive I2 :=
+  | i2 (x : nat).
+  Inductive I3 :=
+  | i3 (b : bool) (x : If b Then I3 Else nat).
+
+(*and here is one that does not, despite being equivalent to [I3]:*)
+
+  Fail Inductive I4 :=
+  | i4 (b : bool) (x : if b then I4 else nat). (* Error: Non strictly positive occurrence of "I4" in
+   "forall b : bool, (if b then I4 else nat) -> I4". *)
+
+(*I think this one should work.  I believe this is a conservative extension over CIC: Since [match] statements returning types can always be re-encoded as inductive type families, the analysis should be independent of whether the constructor uses an inductive or a [match] statement.*)
diff --git a/test-suite/bugs/opened/4717.v b/test-suite/bugs/opened/4717.v
new file mode 100644
index 0000000000..9ad4746723
--- /dev/null
+++ b/test-suite/bugs/opened/4717.v
@@ -0,0 +1,19 @@
+(*See below. They sometimes work, and sometimes do not. Is this a bug?*)
+
+Require Import Omega Psatz.
+
+Definition foo := nat.
+
+Goal forall (n : foo), 0 = n - n.
+Proof. intros. omega. (* works *) Qed.
+
+Goal forall (x n : foo), x = x + n - n.
+Proof.
+  intros.
+  Fail omega. (* Omega can't solve this system *)
+  Fail lia. (* Cannot find witness. *)
+  unfold foo in *.
+  omega. (* works *)
+Qed.
+
+(* Guillaume Melquiond: What matters is the equality. In the first case, it is @eq nat. In the second case, it is @eq foo. The same issue exists for ring and field. So it is not a bug, but it is worth fixing.*)
diff --git a/test-suite/bugs/opened/4721.v b/test-suite/bugs/opened/4721.v
new file mode 100644
index 0000000000..1f184b3930
--- /dev/null
+++ b/test-suite/bugs/opened/4721.v
@@ -0,0 +1,13 @@
+Variables S1 S2 : Set.
+
+Goal @eq Type S1 S2 -> @eq Type S1 S2.
+intro H.
+Fail tauto.
+assumption.
+Qed.
+
+(*This is in 8.5pl1, and Matthieq Sozeau says: "That's a regression in tauto indeed, which now requires exact equality of the universes, through a non linear goal pattern matching:
+match goal with ?X1 |- ?X1 forces both instances of X1 to be convertible,
+with no additional universe constraints currently, but the two types are
+initially different. This can be fixed easily to allow the same flexibility
+as in 8.4 (or assumption) to unify the universes as well."*)
diff --git a/test-suite/bugs/opened/4728.v b/test-suite/bugs/opened/4728.v
new file mode 100644
index 0000000000..230b4beb6c
--- /dev/null
+++ b/test-suite/bugs/opened/4728.v
@@ -0,0 +1,72 @@
+(*I'd like the final [Check] in the following to work:*)
+
+Ltac fin_eta_expand :=
+  [ > lazymatch goal with
+      | [ H : _ |- _ ] => clear H
+      end..
+  | lazymatch goal with
+    | [ H : ?T |- ?T ]
+      => exact H
+    | [ |- ?G ]
+      => fail 0 "No hypothesis matching" G
+    end ];
+  let n := numgoals in
+  tryif constr_eq numgoals 0
+  then idtac
+  else fin_eta_expand.
+
+Ltac pre_eta_expand x :=
+  let T := type of x in
+  let G := match goal with |- ?G => G end in
+  unify T G;
+  unshelve econstructor;
+  destruct x;
+  fin_eta_expand.
+
+Ltac eta_expand x :=
+  let v := constr:(ltac:(pre_eta_expand x)) in
+  idtac v;
+  let v := (eval cbv beta iota zeta in v) in
+  exact v.
+
+Notation eta_expand x := (ltac:(eta_expand x)) (only parsing).
+
+Ltac partial_unify eqn :=
+  lazymatch eqn with
+  | ?x = ?x => idtac
+  | ?f ?x = ?g ?y
+    => partial_unify (f = g);
+       (tryif unify x y then
+           idtac
+         else tryif has_evar x then
+             unify x y
+           else tryif has_evar y then
+               unify x y
+             else
+               idtac)
+  | ?x = ?y
+    => idtac;
+       (tryif unify x y then
+           idtac
+         else tryif has_evar x then
+             unify x y
+           else tryif has_evar y then
+               unify x y
+             else
+               idtac)
+  end.
+
+Tactic Notation "{" open_constr(old_record) "with" open_constr(new_record) "}" :=
+  let old_record' := eta_expand old_record in
+  partial_unify (old_record = new_record);
+  eexact new_record.
+
+Set Implicit Arguments.
+Record prod A B := pair { fst : A ; snd : B }.
+Infix "*" := prod : type_scope.
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
+
+Notation "{ old 'with' new }" := (ltac:({ old with new })) (only parsing).
+
+Check ltac:({ (1, 1) with {| snd := 2 |} }).
+Fail Check { (1, 1) with {| snd := 2 |} }. (* Error: Cannot infer this placeholder of type "Type"; should succeed *)
diff --git a/test-suite/bugs/opened/4755.v b/test-suite/bugs/opened/4755.v
new file mode 100644
index 0000000000..9cc0d361ea
--- /dev/null
+++ b/test-suite/bugs/opened/4755.v
@@ -0,0 +1,34 @@
+(*I'm not sure which behavior is better.  But if the change is intentional, it should be documented (I don't think it is), and it'd be nice if there were a flag for this, or if -compat 8.4 restored the old behavior.*)
+
+Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms.
+Definition f (v : option nat) := match v with
+                                 | Some k => Some k
+                                 | None => None
+                                 end.
+
+Axioms F G : (option nat -> option nat) -> Prop.
+Axiom FG : forall f, f None = None -> F f = G f.
+
+Axiom admit : forall {T}, T.
+
+Existing Instance eq_Reflexive.
+
+Global Instance foo (A := nat)
+  : Proper ((pointwise_relation _ eq)
+              ==> eq ==> forall_relation (fun _ => Basics.flip Basics.impl))
+           (@option_rect A (fun _ => Prop)) | 0.
+exact admit.
+Qed.
+
+Global Instance bar (A := nat)
+  : Proper ((pointwise_relation _ eq)
+              ==> eq ==> eq ==> Basics.flip Basics.impl)
+           (@option_rect A (fun _ => Prop)) | 0.
+exact admit.
+Qed.
+
+Goal forall k, option_rect (fun _ => Prop) (fun v : nat => v = v /\ F f) True k.
+Proof.
+  intro.
+  pose proof (_ : (Proper (_ ==> eq ==> _) and)).
+  Fail setoid_rewrite (FG _ _); []. (* In 8.5: Error: Tactic failure: Incorrect number of goals (expected 2 tactics); works in 8.4 *)
diff --git a/test-suite/bugs/opened/4771.v b/test-suite/bugs/opened/4771.v
new file mode 100644
index 0000000000..396d74bdbf
--- /dev/null
+++ b/test-suite/bugs/opened/4771.v
@@ -0,0 +1,22 @@
+Module Type Foo.
+
+Parameter Inline t : nat.
+
+End Foo.
+
+Module F(X : Foo).
+
+Tactic Notation "foo" ref(x) := idtac.
+
+Ltac g := foo X.t.
+
+End F.
+
+Module N.
+Definition t := 0 + 0.
+End N.
+
+Module K := F(N).
+
+(* Was
+Anomaly: Uncaught exception Not_found. Please report. *)
diff --git a/test-suite/bugs/opened/4778.v b/test-suite/bugs/opened/4778.v
new file mode 100644
index 0000000000..633d158e96
--- /dev/null
+++ b/test-suite/bugs/opened/4778.v
@@ -0,0 +1,35 @@
+Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms.
+Definition f (v : option nat) := match v with
+                                 | Some k => Some k
+                                 | None => None
+                                 end.
+
+Axioms F G : (option nat -> option nat) -> Prop.
+Axiom FG : forall f, f None = None -> F f = G f.
+
+Axiom admit : forall {T}, T.
+
+Existing Instance eq_Reflexive.
+
+(* This instance is needed in 8.4, but is useless in 8.5 *)
+Global Instance foo (A := nat)
+  : Proper ((pointwise_relation _ eq)
+              ==> eq ==> forall_relation (fun _ => Basics.flip Basics.impl))
+           (@option_rect A (fun _ => Prop)) | 0.
+exact admit.
+Qed.
+
+(*
+(* This is required in 8.5, but useless in 8.4 *)
+Global Instance bar (A := nat)
+  : Proper ((pointwise_relation _ eq)
+              ==> eq ==> eq ==> Basics.flip Basics.impl)
+           (@option_rect A (fun _ => Prop)) | 0.
+exact admit.
+Qed.
+*)
+
+Goal forall k, option_rect (fun _ => Prop) (fun v : nat => v = v /\ F f) True k. Proof.
+  intro.
+  pose proof (_ : (Proper (_ ==> eq ==> _) and)).
+  Fail setoid_rewrite (FG _ _); [ | reflexivity.. ]. (* this should succeed without [Fail], as it does in 8.4 *)
diff --git a/test-suite/bugs/opened/4781.v b/test-suite/bugs/opened/4781.v
new file mode 100644
index 0000000000..8b651ac22e
--- /dev/null
+++ b/test-suite/bugs/opened/4781.v
@@ -0,0 +1,94 @@
+Ltac force_clear :=
+  clear;
+  repeat match goal with
+         | [ H : _ |- _ ] => clear H
+         | [ H := _ |- _ ] => clearbody H
+         end.
+
+Class abstract_term {T} (x : T) := by_abstract_term : T.
+Hint Extern 0 (@abstract_term ?T ?x) => force_clear; change T; abstract (exact x) : typeclass_instances.
+
+Goal True.
+(* These work: *)
+  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  pose x.
+  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := (eval cbv iota in (let v : T := x in v)) in
+  pose x.
+  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := match constr:(Set) with ?y => constr:(y) end in
+  pose x.
+(* This fails with an error: *)
+  Fail let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := match constr:(x) with ?y => constr:(y) end in
+  pose x. (* The command has indeed failed with message:
+Error: Variable y should be bound to a term. *)
+(* And the rest fail with Anomaly: Uncaught exception Not_found. Please report. *)
+  Fail let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := match constr:(x) with ?y => y end in
+  pose x.
+  Fail let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := (eval cbv iota in x) in
+  pose x.
+  Fail let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := type of x in
+  pose x. (* should succeed *)
+  Fail let term := constr:(I) in
+  let T := type of term in
+  let x := constr:(_ : abstract_term term) in
+  let x := type of x in
+  pose x. (* should succeed *)
+
+(*Apparently what [cbv iota] doesn't see can't hurt it, and [pose] is perfectly happy with abstracted lemmas only some of the time.
+
+Even stranger, consider:*)
+  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let y := (eval cbv iota in (let v : T := x in v)) in
+  pose y;
+    let x' := fresh "x'" in
+    pose x as x'.
+      let x := (eval cbv delta [x'] in x') in
+      pose x;
+      let z := (eval cbv iota in x) in
+      pose z.
+
+(*This works fine.  But if I change the period to a semicolon, I get:*)
+
+      Fail let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let y := (eval cbv iota in (let v : T := x in v)) in
+  pose y;
+    let x' := fresh "x'" in
+    pose x as x';
+      let x := (eval cbv delta [x'] in x') in
+      pose x. (* Anomaly: Uncaught exception Not_found. Please report. *)
+ (* should succeed *)
+(*and if I use the second one instead of [pose x] (note that using [idtac] works fine), I get:*)
+
+ Fail  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let y := (eval cbv iota in (let v : T := x in v)) in
+  pose y;
+    let x' := fresh "x'" in
+    pose x as x';
+      let x := (eval cbv delta [x'] in x') in
+      let z := (eval cbv iota in x) in (* Error: Variable x should be bound to a term. *)
+      idtac. (* should succeed *)
-- 
cgit v1.2.3