coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing strange evarmap leak in goals.	Pierre-Marie Pédrot	2014-09-18
*	Be more conservative and keep the use of eq_constr in pretyping/ functions.	Matthieu Sozeau	2014-09-17
*	Fix bug #3593, making constr_eq and progress work up to	Matthieu Sozeau	2014-09-17
*	Revert "While resolving typeclass evars in clenv, touch only the ones that ap...	Matthieu Sozeau	2014-09-17
*	While resolving typeclass evars in clenv, touch only the ones that appear in the	Matthieu Sozeau	2014-09-17
*	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
*	Use evar name to print goal.	Hugo Herbelin	2014-09-12
*	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin	2014-09-12
*	Referring to evars by names. Added a parser for evars (but parsing of	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
*	A step towards better differentiating when w_unify is used for subterm	Hugo Herbelin	2014-09-10
*	Fixing localisation of tactic errors (my mistake in himsg.ml essentially).	Hugo Herbelin	2014-09-10
*	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
*	Removing the old implementation of clear_body.	Pierre-Marie Pédrot	2014-09-05
*	At last a working clearbody!	Pierre-Marie Pédrot	2014-09-05
*	Only using filtered hyps in Goal.enter.	Pierre-Marie Pédrot	2014-09-04
*	Ensuring the invariant that hypotheses and named context of the environment of	Pierre-Marie Pédrot	2014-09-04
*	Revert the two previous commits. I was testing in the wrong branch.	Pierre-Marie Pédrot	2014-09-04
*	Removing the old implementation of clear_body.	Pierre-Marie Pédrot	2014-09-04
*	Fix: shelve_unifiable did not work modulo evar instantiation.	Arnaud Spiwack	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
*	Simplify even further the declaration of primitive projections,	Matthieu Sozeau	2014-08-30
*	Simplification of the tclCHECKINTERRUPT tactic.	Pierre-Marie Pédrot	2014-08-28
*	Change the way primitive projections are declared to the kernel.	Matthieu Sozeau	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
*	Move UnsatisfiableConstraints to a pretype error.	Matthieu Sozeau	2014-08-22
*	Removing unused parts of the Goal.sensitive monad.	Pierre-Marie Pédrot	2014-08-21
*	Removing a use of Goal.refine.	Pierre-Marie Pédrot	2014-08-19
*	New primitive allowing to modify refine handles.	Pierre-Marie Pédrot	2014-08-19
*	Improving error message when applying rewrite to an expression which is not a...	Hugo Herbelin	2014-08-18
*	Reorganization of tactics:	Hugo Herbelin	2014-08-18
*	More self-contained code for tclWITHHOLES.	Pierre-Marie Pédrot	2014-08-15
*	Removing unused Refiner.tclWITHHOLES.	Pierre-Marie Pédrot	2014-08-15
*	Better structure for Ltac pretyping environments.	Pierre-Marie Pédrot	2014-08-07
*	Hypotheses in [Proofview.Goal.enter] were not normalised.	Arnaud Spiwack	2014-08-07
*	[uconstr]: use a closure instead of eager substitution.	Arnaud Spiwack	2014-08-06
*	Adding a [make] primitive to the NonLogical monad.	Pierre-Marie Pédrot	2014-08-05
*	Uncountably many bullets (+,-,,++,--,*,+++,...).	Hugo Herbelin	2014-08-05
*	A new step in the new "standard" naming policy for propositional hypotheses	Hugo Herbelin	2014-08-05
*	STM: new "par:" goal selector, like "all:" but in parallel	Enrico Tassi	2014-08-05