coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing strange evarmap leak in goals.	Pierre-Marie Pédrot	2014-09-18
*	Fix timing of evar-normalisation of goals in [Ftactic.nf_enter].	Arnaud Spiwack	2014-09-15
*	While we don't have a clean alternative to Clenvtac, add a primitive	Matthieu Sozeau	2014-09-12
*	Add syntax [id]: to apply tactic to goal named id.	Hugo Herbelin	2014-09-12
*	No plural for only one non existing focused goal.	Hugo Herbelin	2014-09-12
*	Display number of available goals in "incorrect number of goals" error message.	Arnaud Spiwack	2014-09-08
*	Add a tactic [revgoals] to reverse the list of focused goals.	Arnaud Spiwack	2014-09-08
*	Renaming goal-entering functions.	Pierre-Marie Pédrot	2014-09-06
*	At last a working clearbody!	Pierre-Marie Pédrot	2014-09-05
*	Proofview refiner is now type-safe by default.	Pierre-Marie Pédrot	2014-09-04
*	Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT.	Pierre-Marie Pédrot	2014-09-04
*	Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."	Pierre-Marie Pédrot	2014-09-04
*	Simplification of the tclCHECKINTERRUPT tactic.	Pierre-Marie Pédrot	2014-08-28
*	Cleaning and documenting a bit the Proofview.Refine module.	Pierre-Marie Pédrot	2014-08-28
*	"allows to", like "allowing to", is improper	Jason Gross	2014-08-25
*	Removing unused parts of the Goal.sensitive monad.	Pierre-Marie Pédrot	2014-08-21
*	New primitive allowing to modify refine handles.	Pierre-Marie Pédrot	2014-08-19
*	Adding a [make] primitive to the NonLogical monad.	Pierre-Marie Pédrot	2014-08-05
*	Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter].	Arnaud Spiwack	2014-08-05
*	Cleaning of the new implementation of the tactic monad.	Arnaud Spiwack	2014-08-04
*	Add primtive [num_goal] to Proofview.	Arnaud Spiwack	2014-08-01
*	Clean outdated comment in Proofview.Notations.	Arnaud Spiwack	2014-08-01
*	Adding a tclBREAK primitive to the tactic monad.	Pierre-Marie Pédrot	2014-07-28
*	Add a tactic [swap i j] to swap the position of goals [i] and [j].	Arnaud Spiwack	2014-07-25
*	Adds a cycle tactic to reorder goals in a loop.	Arnaud Spiwack	2014-07-25
*	A handful of useful primitives in Proofview.Refine.	Arnaud Spiwack	2014-07-24
*	Proof_global.start_dependent_proof: properly threads the sigma through the te...	Arnaud Spiwack	2014-07-23
*	Adding a "time" tactical for benchmarking purposes. In case the tactic	Hugo Herbelin	2014-07-13
*	check_for_interrupt: better (but slower) in threading mode	Enrico Tassi	2014-07-10
*	Exporting Proof.split in proofview.	Pierre-Marie Pédrot	2014-07-08
*	Revert "time tac" (committed by mistake).	Hugo Herbelin	2014-07-07
*	time tac	Hugo Herbelin	2014-07-07
*	Adding a raw_goals primitive for Tacinterp.	Pierre-Marie Pédrot	2014-06-19
*	Proofs now take and return an evar_universe_context, simplifying interfaces	Matthieu Sozeau	2014-06-18
*	The tactic interpreter now uses a new type of tactics, through	Pierre-Marie Pédrot	2014-06-03
*	Revert "Chasing the goal entering backward while interpreting tactics. This r...	Pierre-Marie Pédrot	2014-05-24
*	Chasing the goal entering backward while interpreting tactics. This required	Pierre-Marie Pédrot	2014-05-24
*	- Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ...	Matthieu Sozeau	2014-05-08
*	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Transfering the initial goals from the proofview to the proof object.	Pierre-Marie Pédrot	2014-04-07
*	Lighter interface for creating refining tactics.	Pierre-Marie Pédrot	2014-03-28
*	Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.	Pierre-Marie Pédrot	2014-03-26
*	Adding phantom types to discriminate normalized goals, and adding a way to	Pierre-Marie Pédrot	2014-03-19
*	Code refactoring thanks to the new Monad module.	Arnaud Spiwack	2014-02-27
*	Remove unsafe code (Obj.magic) in Tacinterp.	Arnaud Spiwack	2014-02-27
*	Proofview.Notations: Now that (>>=) is free, use it for tclBIND.	Arnaud Spiwack	2014-02-27
*	Get rid of the enterl/glist API for Proofview.Goal.	Arnaud Spiwack	2014-02-27
*	Tacinterp: fewer Proofview.Goal.enterl.	Arnaud Spiwack	2014-02-25
*	Typos in comment.	Arnaud Spiwack	2014-01-31