Gaëtan Gilbert (Dec 02 2020 at 13:58): Gaëtan Gilbert (Dec 02 2020 at 13:58):this is an idea about extending local/global
for instance for hints we could have
Module M.
Module N.
Global(M) Hint foo.
Local(M) Hint bar.
(* foo and bar active *)
End N.
(* foo and bar active *)
End M.
(* nothing active *)
Import M.
(* foo active *)
Anything.
(* bar never activates *)
Not sure if Import N would activate foo though
Last updated: Jun 09 2023 at 08:01 UTC