From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 test-suite/success/auto.v | 89 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 89 insertions(+)

(limited to 'test-suite/success/auto.v')

diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v
index aaa7b3a5..5477c833 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.
-- 
cgit v1.2.3