see https://github.com/coq/coq/issues/15213 what sort of things should be implemented? eg Hint Db Copy or Hint Db Remove Transparency or whatever you want
Last updated: Sep 23 2023 at 08:01 UTC