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/bugs')

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 +++++++++++++++++++++++++++++++++++++++++++
 4 files changed, 55 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/bugs/closed/5149.v

(limited to 'test-suite/bugs')

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.
+
-- 
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 ++++++++++++++++++++++++-------
 1 file changed, 24 insertions(+), 7 deletions(-)

(limited to 'test-suite/bugs')

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
-- 
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/bugs')

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 ++++---
 2 files changed, 8 insertions(+), 11 deletions(-)

(limited to 'test-suite/bugs')

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.
-- 
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/bugs')

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/bugs')

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 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'test-suite/bugs')

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.
-- 
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/bugs')

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 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 ++--
 2 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'test-suite/bugs')

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)
-- 
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 +++++
 2 files changed, 44 insertions(+)
 create mode 100644 test-suite/bugs/closed/5198.v
 create mode 100644 test-suite/bugs/closed/5203.v

(limited to 'test-suite/bugs')

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
-- 
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/bugs')

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