1 files changed, 7 insertions, 1 deletions
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index e1c74048cb..98b5992ade 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -24,7 +24,7 @@ Hint Destruct h8 := 4 Hypothesis (_ <= _) => fun H => apply H.
 (* Checks that local names are accepted *)
 Section A.
   Remark Refl : forall (A : Set) (x : A), x = x. 
-  Proof refl_equal.
+  Proof. exact refl_equal. Defined.
   Definition Sym := sym_equal.
   Let Trans := trans_equal.
  
@@ -46,3 +46,9 @@ Section A.
 
 End A.
 
+Axiom a : forall n, n=0 <-> n<=0.
+
+Hint Resolve -> a.
+Goal forall n, n=0 -> n<=0.
+auto.
+Qed.