coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-06-01	Slight improvement in naming existential variables.	Hugo Herbelin
	In a Meta := Evar unification problem and the Meta is bound to a (named) binder, and the Evar is a GoalEvar, we set the source of the evar to be the one of the Meta.
2019-12-23	Fixes a small bug exposing an _ANONYMOUS_REL in a unification error message.	Hugo Herbelin
	Might be improvable further. In the first example, we have two environments involved and one is implicit. It does not seem excluded that a variable name of the second environment shows up which is not listed in the first environment.