-
Robbert Krebbers authored
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.
Robbert Krebbers authoredSince `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.