Discharge on the fly in the kernel - #18065

Closed

herbelin wants to merge 6 commits into

rocq-prover:masterfrom

herbelin:master+discharge-on-the-fly-kernel

Commits on Sep 19, 2023

Adding functions to pop the dirpath of kns.
herbelin
committed
c8d934a
Write discharge functions in a principled way.
herbelin
committed
e2ea473
Unify test for hconsing between constant and inductive types.
herbelin
committed
cdf4b87
Adding Section.on_previous_section.
herbelin
committed
e305454
DeclareUniv: Cosmetic name uniformization.
herbelin
committed
5fff981
Implement discharge on the fly in the kernel.
herbelin
committed
0b66177