Jason Gross

Does this PR also change the locality of the existence of HintDbs? What's up with ``` File "./src/Util/ZUtil/AddGetCarry.v", line 37, characters 8-34: Error: Rewriting base zsimplify does not exist. ```...

@ppedrot So `Set Loose Hint Behavior "Warn".` and `Set Loose Hint Behavior "Strict".` do not apply to `Hint Rewrite` at all?! Can this be fixed, or at least add `Set...

Even if it's a hack, it would be nice to be able to get warnings for all the things that have to change all at once, rather than having to...

It would also be very helpful to have a version of `Info 2 autorewrite` that actually displayed the rewrites that were performed. Would getting this be possible?

@ppedrot To make more progress on f-c-l for this without sinking in an enormous amount of time, I really do need to at least be able to see the list...

> I'm not sure it's really worth the effort implementing a dedicated hack inside Coq just to ease the porting of this one development. I agree, but I don't think...

Yes, I'm aware. While the hack would make my task easier, I acknowledge that there's no strong reason to keep f-c-l compatible with old versions of Coq, and I don't...

No, this is just a script I use anytime I set up a new machine to install all the versions of Coq. It installs released versions bank through 8.4 and...

PG is unaffected because coqtop itself is responsible for pruning the context of shelved goals; only the context of the currently focused goal is serialized in `-emacs` mode (which is...

> sorted by logical name (possibly case-insensitive) This is fine for things bound with -Q / COQPATH, but anything bound with -R should be sorted by whatever order Coq uses...