Skip to content
Snippets Groups Projects
user avatar
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.
f0b073ee
History
Name Last commit Last update
..