Stream: Coq devs & plugin devs

Topic: lazy linking of constants


view this post on Zulip Hugo Herbelin (Nov 13 2020 at 18:36):

@ppedrot: A late remark about last week discussion on linking constants at require-time. Would there be disadvantages at the end at linking lazily (using an option mutable field in Const/Ind/Construct constructors)? How much could we expect to gain?


Last updated: Oct 21 2021 at 21:03 UTC