coq - The formal proof system

Age	Commit message (Collapse)	Author
2015-01-12	Update headers.	Maxime Dénès

2014-11-01	Info: tactic notations (TacAlias) print their names.	Arnaud Spiwack
	Empirically it works better on some notations than on others and I have no idea why. I've seen notations not printing their arguments, for instance, and other printing perfectly.
2014-09-06	Renaming goal-entering functions.	Pierre-Marie Pédrot
	1. Proofview.Goal.enter into Proofview.Goal.nf_enter. 2. Proofview.Goal.raw_enter into Proofview.Goal.enter. 3. Proofview.Goal.goals -> Proofview.Goals.nf_goals 4. Proofview.Goal.raw_goals -> Proofview.Goals.goals 5. Ftactic.goals -> Ftactic.nf_goals 6. Ftactic.raw_goals -> Ftactic.goals This is more uniform with the other functions of Coq.
2014-09-05	Adding a Ftactic module for potentially focussing tactics.	Pierre-Marie Pédrot
	The code for the module was moved from Tacinterp. We still expose partially the implementation of the Ftactic.t type, for the sake of simplicity. It may be dangerous if used improperly though.