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.
|
