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: Mar 28 2024 at 14:01 UTC