Merge branch 'v8.5'

3 files changed, 115 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4596.v b/test-suite/bugs/closed/4596.v
new file mode 100644
index 0000000000..592fdb6580
--- /dev/null
+++ b/test-suite/bugs/closed/4596.v
@@ -0,0 +1,14 @@
+Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms.
+
+Definition T (x : bool) := x = true.
+
+Goal forall (S : Type) (b b0 : S -> nat -> bool) (str : S) (p : nat)
+  (s : forall n : nat, bool)
+  (s0 s1 : nat -> S -> S),
+  (forall (str0 : S) (n m : nat),
+  (if s m then T (b0 (s1 n str0) 0) else T (b (s1 n str0) 0)) -> T (b (s0 n str0) m) ->
+    T (b str0 m)) ->
+  T (b str p).
+Proof.
+intros ???????? H0.
+rewrite H0.
diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v
index aaa7b3a514..5477c83316 100644
--- a/test-suite/success/auto.v
+++ b/test-suite/success/auto.v
@@ -45,3 +45,92 @@ Proof.
   eexists. Fail progress debug eauto with test2. 
   progress eauto with test.
 Qed.
+
+(** Patterns of Extern have a "matching" semantics.
+    It is not so for apply/exact hints *)
+
+Class B (A : Type).
+Class I. 
+Instance i : I.
+  
+Definition flip {A B C : Type} (f : A -> B -> C) := fun y x => f x y.
+Class D (f : nat -> nat -> nat).
+Definition ftest (x y : nat) := x + y.
+Definition flipD (f : nat -> nat -> nat) : D f -> D (flip f).
+  Admitted.
+Module Instnopat.
+  Local Instance: B nat.
+  (* pattern_of_constr -> B nat *)
+  (* exact hint *)
+  Check (_ : B nat).
+  (* map_eauto -> B_instance0 *)
+  (* NO Constr_matching.matches !!! *)
+  Check (_ : B _).
+
+  Goal exists T, B T.
+    eexists.
+    eauto with typeclass_instances.
+  Qed.
+
+  Local Instance: D ftest.
+  Local Hint Resolve flipD | 0 : typeclass_instances.
+  (* pattern: D (flip _) *)
+  Fail Timeout 1 Check (_ : D _). (* loops applying flipD *)  
+  
+End Instnopat.
+
+Module InstnopatApply.
+  Local Instance: I -> B nat.
+  (* pattern_of_constr -> B nat *)
+  (* apply hint  *)
+  Check (_ : B nat).
+  (* map_eauto -> B_instance0 *)
+  (* NO Constr_matching.matches !!! *)
+  Check (_ : B _).
+
+  Goal exists T, B T.
+    eexists.
+    eauto with typeclass_instances.
+  Qed.
+End InstnopatApply.
+  
+Module InstPat.
+  Hint Extern 3 (B nat) => split : typeclass_instances.
+  (* map_eauto -> Extern hint *)
+  (* Constr_matching.matches -> true *)
+  Check (_ : B nat).
+  (* map_eauto -> Extern hint *)
+  (* Constr_matching.matches -> false:
+     Because an inductive in the pattern does not match an evar in the goal *)
+  Check (_ : B _).
+
+  Goal exists T, B T.
+    eexists.
+    (* map_existential -> Extern hint *)
+    (* Constr_matching.matches -> false *)
+    Fail progress eauto with typeclass_instances.
+    (* map_eauto -> Extern hint *)
+    (* Constr_matching.matches -> false *)
+    Fail typeclasses eauto.
+  Abort.
+
+  Hint Extern 0 (D (flip _)) => apply flipD : typeclass_instances.
+  Module withftest.
+    Local Instance: D ftest.
+
+    Check (_ : D _).
+    (* D_instance_0 : D ftest *)
+    Check (_ : D (flip _)).
+    (* ... : D (flip ftest) *)
+  End withftest.
+  Module withoutftest.
+    Hint Extern 0 (D ftest) => split : typeclass_instances.
+    Check (_ : D _).
+    (* ? : D ?, _not_ looping *)
+    Check (_ : D (flip _)).
+    (* ? : D (flip ?), _not_ looping *)
+
+    Check (_ : D (flip ftest)).
+    (* flipD ftest {|  |} : D (flip ftest) *)
+  End withoutftest.
+End InstPat.
diff --git a/test-suite/typeclasses/open_constr.v b/test-suite/typeclasses/open_constr.v
new file mode 100644
index 0000000000..5f1785c706
--- /dev/null
+++ b/test-suite/typeclasses/open_constr.v
@@ -0,0 +1,12 @@
+Tactic Notation "opose" open_constr(foo) := pose foo.
+Class Foo := Build_Foo : Set.
+Axiom f : forall `{Foo}, Set.
+Set Printing Implicit.
+Goal forall `{Foo}, True.
+Proof.
+  intro H.
+  pose f.
+  opose f.
+  Fail let x := (eval hnf in P) in has_evar x.
+  let x := (eval hnf in P0) in has_evar x.
+