coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-04-28	Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of ↵	Maxime Dénès
	let-ins
2017-04-09	Fixing #5420 as well as many related bugs due to miscounting let-ins.	Hugo Herbelin
	- Supporting let-ins in tactic "fix", and hence in interactive Fixpoint and mutual theorems. - Documenting more precisely the meaning of n in tactic "fix id n". - Fixing computation of recursive index at interpretation time in the presence of let-ins.
2017-04-04	Merge branch 'trunk' into pr379	Maxime Dénès

2017-03-24	Merge branch 'trunk' into pr379	Maxime Dénès

2017-03-24	Renaming local_binder into local_binder_expr.	Hugo Herbelin
	This is a bit long, but it is to keep a symmetry with constr_expr.
2017-02-15	[stm] Break stm/toplevel dependency loop.	Emilio Jesus Gallego Arias
	Currently, the STM, vernac interpretation, and the toplevel are intertwined in a mutual dependency that needs to be resolved using imperative callbacks. This is problematic for a few reasons, in particular it makes the interpretation of commands that affect the document quite intricate. As a first step, we split the `toplevel/` directory into two: "pure" vernac interpretation is moved to the `vernac/` directory, on which the STM relies. Test suite passes, and only one command seems to be disabled with this approach, "Show Script" which is to my understanding obsolete. Subsequent commits will fix this and refine some of the invariants that are not needed anymore.