coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-03-25	[ssr] avoid HO unif when doing truncation analysis	Enrico Tassi
	Eliminators can be: - dependent: ... -> forall x (y : I x), P x y - truncated: ... -> forall x (y : I x), P x - funind like: ..-> forall x, P t The user may provide a term t in `elim: t` - t may be the last argument - t may be the last "pattern" (standing for the last argument of P) We use unification to see if t (and its type) fits in one of these cases (and/or to infer t). This patch refuses to use unification in the HO case eg `?T a = t` since the result is too often a false positive.