coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-01-13	Avoid using "subgoals" in the UI, it means the same as "goals"	Jim Fehrle

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.
2020-02-25	Use implicit arguments in notations for eq.	Gaëtan Gilbert
	This gives IMO slightly nicer errors when the type cannot be inferred, ie ~~~coq Type (forall x, x = x). ~~~ says "cannot infer the implicit parameter A of eq" instead of "cannot infer this placeholder".
2019-10-29	Show diffs in "Show Proof."	Jim Fehrle
	Add experimental "Show Proof" command to the toplevel that shadows the current command in the parser (in coqtop and PG only). Apply existing code to highlight diffs in the output
2019-09-19	Fix #10420 Add dependent evar mapping info to output	Jim Fehrle

2019-06-25	Re-add the "Show Goal" command for Prooftree in PG.	Jim Fehrle
	It prints a goal given its internal goal id and the Stm state id.