Factorizing universe treatment for Definition, Theorem and Fixpoint (part of CEP #89) - #19322

Merged

coqbot-app[bot] merged 5 commits into

rocq-prover:masterfrom

herbelin:master+declare-make-univs-late

Oct 11, 2024

Commits on Oct 4, 2024

Recursive message
herbelin
committed
272f6e5
Merge declare_entry and declare_entry_core.
herbelin
committed
30c4d85

Commits on Oct 8, 2024

Add ability to accumulate used universes in make_univs_immediate.

herbelin
and
SkySkimmer
committed
b7e7a6a
Merging declare_definition and declare_mutual_definitions with declare_possibly_mutual_definitions
herbelin
committed
1940ea6
Move declare_definition to export section.
herbelin
committed
603db3d