coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Info: tactic notations (TacAlias) print their names.	Arnaud Spiwack	2014-11-01
\| \| \| \|	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.
*	Renaming goal-entering functions.	Pierre-Marie Pédrot	2014-09-06
\| \| \| \| \| \| \| \| \| \| \|	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.
*	Adding a Ftactic module for potentially focussing tactics.	Pierre-Marie Pédrot	2014-09-05
	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.