aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2127.v
blob: 142ada268be37ece954e0ab0563ac3d895895f2e (plain)
1
2
3
4
5
6
7
8
(* Check that "apply eq_refl" is not exported as an interactive
   tactic but as a statically globalized one *)

(* (this is a simplification of the original bug report) *)

Module A.
Hint Rewrite eq_sym using apply eq_refl : foo.
End A.