coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin	2014-09-12
*	No plural for only one non existing focused goal.	Hugo Herbelin	2014-09-12
*	Fix source of initial 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
*	Ensuring the invariant that hypotheses and named context of the environment of	Pierre-Marie Pédrot	2014-09-04
*	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
*	Using goal-tactics to interpret arguments to idtac.	Pierre-Marie Pédrot	2014-09-04
*	Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."	Pierre-Marie Pédrot	2014-09-04
*	Putting back normalized goals when entering them.	Pierre-Marie Pédrot	2014-09-03
*	Simplification of the tclCHECKINTERRUPT tactic.	Pierre-Marie Pédrot	2014-08-28
*	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
*	Hypotheses in [Proofview.Goal.enter] were not normalised.	Arnaud Spiwack	2014-08-07
*	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
*	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
*	Adding a tail-rec tclONCE.	Pierre-Marie Pédrot	2014-07-24
*	Proof_global.start_dependent_proof: properly threads the sigma through the te...	Arnaud Spiwack	2014-07-23
*	Adding a delay to tclTIME.	Pierre-Marie Pédrot	2014-07-14
*	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
*	- Fix eq_constr_universes restricted to Sorts.equal	Matthieu Sozeau	2014-05-06
*	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
*	Fixing various backtrace recordings.	Pierre-Marie Pédrot	2014-04-25
*	Adding a [map] primitive to the tactic monad. Hopefully this should be	Pierre-Marie Pédrot	2014-04-20
*	Transfering the initial goals from the proofview to the proof object.	Pierre-Marie Pédrot	2014-04-07
*	Actually using the [modify] primitive.	Pierre-Marie Pédrot	2014-04-06
*	Evars introduced by Proofview refining are flagged as GoalEvar. For some	Pierre-Marie Pédrot	2014-04-01
*	Lighter interface for creating refining tactics.	Pierre-Marie Pédrot	2014-03-28