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 *)
Anything.
(* bar never activates *)

Not sure if Import N would activate foo though


Last updated: Oct 16 2021 at 01:03 UTC