Seal `fresh_generic`.

Since fresh_generic is too inefficient for all practical purposes, we seal off its definition. That way, Coq will not accidentally unfold it during unification or other tactics.

This issue actually occurred in iGPS, as reported by Hai.

changed the description

added 1 commit

• 4fcf0c69 - Seal `fresh_generic`.

Compare with previous version

@haidang Could you test if this fixes your problem?

added 1 commit

• f0b073ee - Seal `fresh_generic`.

Compare with previous version

@robbertkrebbers Yes, this fixes the problem in iGPS. Thanks!

mentioned in commit 824e9723

merged