blob: 20ea460325a8ad2f3d98c2b077ac3f7869b5d06d (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
(* Check that "apply refl_equal" 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 sym_equal using apply refl_equal : foo.
End A.
|
