Algebraic universes and variances#21603

Draft

mattam82 wants to merge 47 commits intorocq-prover:masterfrom

mattam82:universes-and-variances

Commits on Mar 10, 2026

Algebraic Universes and Variances
mattam82
committed
Scheme equality was uterly broken w.r.t. universes
mattam82
committed
Minor fixes
mattam82
committed
Minor fix in Module With Definition (taking poly into account)
mattam82
committed
Fix 7967, thread poly flag in interp of constructors
mattam82
committed
Fix restriction (became a noop in rebase)
mattam82
committed
Fixed `par: abstract` test.
mattam82
committed
Avoid clash between univ poly product in CRelationClasses and pairs
mattam82
committed
Fix goal equality check (progress/not same goal) and inductive restriction
mattam82
committed
Fix test
mattam82
committed
Fix Derive.v test-suite file
mattam82
committed
Fix test-suite file module_with_def_univ_poly
mattam82
committed
Fix test-suite file, EQ minimizes to Set now
mattam82
committed
Fix test-suite file, rewrite no longer needed
mattam82
committed
Reverted HoTT_coq_103.v
mattam82
committed
Fix externalisation (revert change in univalg)
mattam82
committed
Fix output tests
mattam82
committed
Fix regression in minimization of rewrite rules
mattam82
committed
Expected changes in output tests
mattam82
committed
Add new debug printing functions
mattam82
committed
Remove stray file
mattam82
committed
Still collapse sort variables without minimizing in build_constant_by_tactic
mattam82
committed
Fix FIXME
mattam82
committed
Start doc on OCaml API for minimization and variances
mattam82
committed
Catch an exception from UGraph
mattam82
committed
Catch exceptions at calls to UGraph.set
mattam82
committed
Debug in inferCumulativit, to merge
mattam82
committed
Typo in comment, on master
mattam82
committed
[Set Kernel Cumulativity Zeta] flag for zeta-reduction cumul inference
mattam82
committed
Add overlays
mattam82
committed
Set Universe Polymorphism in ssr/*

CohenCyril
authored and
mattam82
committed
Fix overlay
mattam82
committed
Dune setup for composed build with ci
mattam82
committed
Fixes after rebase
mattam82
committed
merge_universe_context back to merge_universe_context_set
mattam82
committed
Fixes after rebase
mattam82
committed
Fix after rebase (do not collapse by default in ind_tables.ml#define)
mattam82
committed
Fix test-suite file 20242: change of semantics for polymorphic assumptions
mattam82
committed
Thanks to irrelevance, bug_21674 now succeeds to convert length calls
mattam82
committed
Fix after rebase: Assumptions should not be cumulative by default
mattam82
committed
Fix bug 20242 (to squash)
mattam82
committed
Call minimization for Module with Definition with the right flags
mattam82
committed
Squash fix
mattam82
committed
Minor fix in comment. We just have the core lib universes now
mattam82
committed
New output of cumulativity information
mattam82
committed
Fix output test
mattam82
committed
Down to 1 monomorphic universe above Set in the core library.
mattam82
committed