1 files changed, 48 insertions, 0 deletions
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
new file mode 100644
index 00000000..f32753e0
--- /dev/null
+++ b/test-suite/success/Hints.v
@@ -0,0 +1,48 @@
+(* Checks syntax of Hints commands *)
+(* Checks that qualified names are accepted *)
+
+(* New-style syntax *)
+Hint h1 : core arith := Resolve Logic.refl_equal.
+Hint h2 := Immediate Logic.trans_equal.
+Hint h3 : core := Unfold Logic.sym_equal.
+Hint h4 : foo bar := Constructors Logic.eq.
+Hint h5 : foo bar := Extern 3 (eq ? ? ?) Apply Logic.refl_equal.
+
+(* Old-style syntax *)
+Hints Resolve Coq.Init.Logic.refl_equal Coq.Init.Logic.sym_equal.
+Hints Resolve Coq.Init.Logic.refl_equal Coq.Init.Logic.sym_equal : foo.
+Hints Immediate Coq.Init.Logic.refl_equal Coq.Init.Logic.sym_equal.
+Hints Immediate Coq.Init.Logic.refl_equal Coq.Init.Logic.sym_equal : foo.
+Hints Unfold Coq.Init.Datatypes.fst Coq.Init.Logic.sym_equal.
+Hints Unfold Coq.Init.Datatypes.fst Coq.Init.Logic.sym_equal : foo.
+
+(* What's this stranged syntax ? *)
+HintDestruct Conclusion h6 (le ? ?) 4 [ Fun H -> Apply H ].
+HintDestruct Discardable Hypothesis h7 (le ? ?) 4 [ Fun H -> Apply H ].
+HintDestruct Hypothesis h8 (le ? ?) 4 [ Fun H -> Apply H ].
+
+(* Checks that local names are accepted *)
+Section A.
+  Remark Refl : (A:Set)(x:A)x=x. 
+  Proof refl_equal.
+  Definition Sym := sym_equal.
+  Local Trans := trans_equal.
+ 
+  Hint h1 : foo := Resolve Refl.
+  Hint h2 : bar := Resolve Sym.
+  Hint h3 : foo2 := Resolve Trans.
+
+  Hint h2 := Immediate Refl.
+  Hint h2 := Immediate Sym.
+  Hint h2 := Immediate Trans.
+
+  Hint h3 := Unfold Refl.
+  Hint h3 := Unfold Sym.
+  Hint h3 := Unfold Trans.
+
+  Hints Resolve Sym Trans Refl.
+  Hints Immediate Sym Trans Refl.
+  Hints Unfold Sym Trans Refl.
+
+End A.
+