Imported Upstream version 8.5~beta1+dfsg

1 files changed, 22 insertions, 1 deletions

diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v
index 9b691e25..db3b19af 100644
--- a/test-suite/success/auto.v
+++ b/test-suite/success/auto.v
@@ -14,7 +14,7 @@ Hint Resolve L.
 
 Goal G unit Q -> F (Q tt).
   intro.
-  auto.
+  eauto. 
 Qed.
 
 (* Test implicit arguments in "using" clause *)
@@ -24,3 +24,24 @@ auto using (pair O).
 Undo.
 eauto using (pair O).
 Qed.
+
+Create HintDb test discriminated.
+
+Parameter foo : forall x, x = x + 0.
+Hint Resolve foo : test.
+
+Variable C : nat -> Type -> Prop.
+
+Variable c_inst : C 0 nat.
+
+Hint Resolve c_inst : test.
+
+Hint Mode C - + : test.
+Hint Resolve c_inst : test2.
+Hint Mode C + + : test2.
+
+Goal exists n, C n nat.
+Proof.
+  eexists. Fail progress debug eauto with test2. 
+  progress eauto with test.
+Qed.