Skip to content
  • Robbert Krebbers's avatar
    Seal `fresh_generic`. · f0b073ee
    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