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: Jan 31 2023 at 14:03 UTC