blob: 0fc854b6fd8b7f0d6edd771917aea5f1142659f4 (
plain)
1
2
3
4
5
6
7
8
|
(* 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.
|
