coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-10-31	Closes #13278: take into account elimination constraints in small inversion.	Hugo Herbelin
	Ideally, if equations t <= ?x were preserving subtyping that could be simpler. Currently we need however to put a rigid universe as constraint on the return predicate so that one branch does not force the return sort to be lower by unification than what another branch would have needed.
2020-10-31	Fine-tuning the sort of the predicate obtained by small inversion.	Hugo Herbelin
	If the result is in SProp, Prop or (impredicative) Set, we preserve this information since the elimination sort might be restricted by the sort of the destructed type. If the result is in Type, we use a fresh sort upper bound so that we are sure not having residual algebraic universes which would raise problems in a type constraint (e.g. in define_evar_as_product). This fixes the part of #13278 posted on discourse.