Merge the execution paths for struct and measure/wf in Program Fixpoint - #19258

Merged

coqbot-app[bot] merged 6 commits into

rocq-prover:masterfrom

herbelin:master+merge-fixpoint-struct-measure-wf

Jul 2, 2024

Commits on Jun 28, 2024

Prepare centralized interpretation of fixpoint annotation.
herbelin
committed
8e4fbb3
Removing useless code.
herbelin
committed
c66612e
Removing useless code.
herbelin
committed
cbea83f
Embed Program Fixpoint wf/measure in the main Co/Fixpoint routine.
herbelin
committed
624e2de
Remove now useless set_obligation_internalization_data.
herbelin
committed
713ee82
Towards supporting wf/measure w/o Program nor Function.
herbelin
committed
63c9528