coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	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.
*	Add more primitives to the [Monad.Make] arguments.	Arnaud Spiwack	2014-10-22
\| \| \| \|	For optimisation purposes.
*	Fixing strange evarmap leak in goals.	Pierre-Marie Pédrot	2014-09-18
\| \| \| \| \| \|	Goals have to be refreshed when observed, because the evarmap may have changed between the moment where the goal was generated and the moment the goal is used.
*	Fix timing of evar-normalisation of goals in [Ftactic.nf_enter].	Arnaud Spiwack	2014-09-15
\| \| \| \|	All goals were normalised up front, rather than normalised after the tactic acting on previous goal had the chance to solve some evars, which then appeared non-instantiated to tactics which do not work up to evar map (most of them).
*	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.