Seal `fresh_generic`.
There are currently no pipelines.
To run a merge request pipeline, the jobs in the CI/CD configuration file must be configured to run in merge request pipelines and you must have sufficient permissions in the source project.
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.
To run a merge request pipeline, the jobs in the CI/CD configuration file must be configured to run in merge request pipelines and you must have sufficient permissions in the source project.