Discharge on the fly - #17888

Closed

herbelin wants to merge 8 commits into

rocq-prover:masterfrom

herbelin:master+discharge-on-the-fly

Commits on Sep 2, 2023

Unify test for hconsing between constant and inductive types.
herbelin
committed
e5d9a23
Adding Section.on_previous_section.
herbelin
committed
02f8901
Adding functions to pop the dirpath of kns.
herbelin
committed
f787305
DeclareUniv: Cosmetic name uniformization.
herbelin
committed
0392cd8
ssr_mini_mathcomp.v: address various warnings.
herbelin
committed
d2a2e92
Write discharge functions in a principled way.
herbelin
committed
f412f7a
Implement discharge on the fly.
herbelin
committed
c5199cf
Overlays for Equations, HoTT and metacoq
herbelin
committed
219bc2f