coq - The formal proof system

Age	Commit message (Collapse)	Author
2016-05-04	Moving Ftactic and Geninterp to the engine folder.	Pierre-Marie Pédrot

2016-03-06	Putting Tactic_debug just below Tacinterp.	Pierre-Marie Pédrot

2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot

2016-01-20	Update copyright headers.	Maxime Dénès

2016-01-08	Monotonizing Ftactic.	Pierre-Marie Pédrot

2015-12-28	Implementing non-focussed generic arguments.	Pierre-Marie Pédrot
	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.
2015-11-10	Typo.	Hugo Herbelin

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-10-22	Add more primitives to the [Monad.Make] arguments.	Arnaud Spiwack
	For optimisation purposes.
2014-09-18	Fixing strange evarmap leak in goals.	Pierre-Marie Pédrot
	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.
2014-09-15	Fix timing of evar-normalisation of goals in [Ftactic.nf_enter].	Arnaud Spiwack
	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).
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.