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.
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.