Skip to content

Seal `fresh_generic`.

Robbert Krebbers requested to merge robbert/seal_fresh_generic into master

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.

Edited by Robbert Krebbers

Merge request reports