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-10-20	Indexing Proofview.goals with a stage.	Pierre-Marie Pédrot
	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.
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.