coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Putting Tactic_debug just below Tacinterp.	Pierre-Marie Pédrot	2016-03-06
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
\| \|
* \|	Monotonizing Ftactic.	Pierre-Marie Pédrot	2016-01-08
\| \|
* \|	Implementing non-focussed generic arguments.	Pierre-Marie Pédrot	2015-12-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	Kind of enhances the situation of bug #4409. Now arguments can be interpreted globally or focussedly in a dynamic fashion because the interpretation function returns a Ftactic.t. The bug is not fixed yet because we should tweak the interpretation of tactic arguments.
* \|	Indexing Proofview.goals with a stage.	Pierre-Marie Pédrot	2015-10-20
\|/ \| \| \| \| \|	This is not perfect though, some primitives are unsound, and some higher-order API should use polymorphic functions so as not to depend on a given level.
*	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.
*	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.