Add elaboration of qualities#21450

Open

TDiazT wants to merge 9 commits intorocq-prover:masterfrom

TDiazT:elab-sorts

Commits on Jan 27, 2026

feat: Add more specific elim constraints to non-prim projections
TDiazT
committed

Commits on Jan 29, 2026

Address comments
TDiazT
committed

Commits on Feb 2, 2026

refactor: Pass on sigma in search_guard
TDiazT
committed

Commits on Feb 5, 2026

test: Move sort_poly_elab test to output folder
TDiazT
committed