Stream: Coq devs & plugin devs

Topic: module attached locality

view this post on Zulip 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 *)
(* bar never activates *)

Not sure if Import N would activate foo though

Last updated: Mar 02 2024 at 17:02 UTC