coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Tactic unfold always asks for comma between names.	pboutill	2012-05-09
*	Partial revert of r15148 in order to compile with Camlp4	pboutill	2012-04-27
*	migrate g_obligations.ml4 in parsing	letouzey	2012-04-26
*	Program: avoid staying in program mode after a failed Program command	letouzey	2012-04-26
*	remove undocumented and scarcely-used tactic auto decomp	letouzey	2012-04-23
*	Corrects a (very) longstanding bug of tactics. As is were, tactic expecting	aspiwack	2012-04-18
*	Removed syntax BeginSubproof/EndSubproof. It has been replaced by	aspiwack	2012-04-13
*	Remove print call that do not use the pp mechanism	pboutill	2012-04-12
*	"A -> B" is a notation for "forall _ : A, B".	pboutill	2012-04-12
*	Fixing a few bugs (see #2571) related to interpretation of multiple binders	herbelin	2012-04-06
*	Typo in a message.	aspiwack	2012-03-30
*	Added a command "Unfocused" which returns an error when the proof is	aspiwack	2012-03-30
*	info_trivial, info_auto, info_eauto, and debug (trivial\|auto)	letouzey	2012-03-30
*	Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconcl	letouzey	2012-03-30
*	Slight change in the semantics of arguments scopes: scopes can no	herbelin	2012-03-26
*	Remove undocumented command "Delete foo"	letouzey	2012-03-23
*	Remove old proof-managment commands Suspend/Resume	letouzey	2012-03-23
*	Ppvernac: nicer printing of proof delimiters { ... }	letouzey	2012-03-21
*	Fixing bug #2724 (using notations with binders in cases patterns	herbelin	2012-03-20
*	Fixing alpha-conversion bug #2723 introduced in r12485-12486.	herbelin	2012-03-20
*	Continuing r15045-15046 and r15055 (fixing bug #2732 about atomic	herbelin	2012-03-20
*	Hopefully complying with camlp5 < 6.00 syntax	herbelin	2012-03-19
*	Yet another subtlety with bug 2732: when several grammar rules of a	herbelin	2012-03-18
*	Fixing bug #2732 (anomaly when using the tolerance for writing	herbelin	2012-03-18
*	Final part of moving Program code inside the main code. Adapted add_definitio...	msozeau	2012-03-14
*	Glob_term.predicate_pattern: No number of parameters with letins.	pboutill	2012-03-02
*	Noise for nothing	pboutill	2012-03-02
*	In the syntax of pattern matching, "in" clauses are patterns.	pboutill	2012-02-29
*	Arguments supports extra notation scopes	gareuselesinge	2012-02-14
*	A "Grab Existential Variables" to transform the unresolved evars at the end o...	aspiwack	2012-02-07
*	Fix camlp4 compilation	pboutill	2012-01-31
*	Added an pattern / occurence syntax for vm_compute.	ppedrot	2012-01-30
*	Removed a seemingly unused argument in Require of modules, introduced 10 year...	ppedrot	2012-01-23
*	Fixed pretty-printing of Opaque, Transparent and Strategy locality flags.	ppedrot	2012-01-23
*	Reverted previous commit, which broke library compilation.	ppedrot	2012-01-20
*	This is a quick hack to permit the parsing of the locality flag in the Progra...	ppedrot	2012-01-20
*	Fix printing of classes	msozeau	2012-01-20
*	Fix typeclass constraint grammar rule to allow `{_ : Reflexive A R}.	msozeau	2012-01-19
*	Pretty printing of generalized binder	pboutill	2012-01-19
*	Fixed the pretty-printing of the Program plugin.	ppedrot	2012-01-17
*	Some fix in beautify pretty-printer	pboutill	2012-01-17
*	Inductiveops.nb_*{,_env} cleaning	pboutill	2012-01-16
*	Fix printing of instances, generalized arguments.	msozeau	2012-01-10
*	Fixed some printing details for dependent evars in emacs mode. Patch	courtieu	2011-12-19
*	Applied patches proposed suggested by Hendrik Tews to fix existential	courtieu	2011-12-18
*	Removing PrintConstr debugging entry in g_proof.ml4 which was not	herbelin	2011-12-18
*	A pass on warning printings. Made systematic the use of msg_warning so	herbelin	2011-12-17
*	Improving pretty-printing of Ltac functions.	herbelin	2011-12-17
*	Fixing previous commit which was bugging on tactics preceded by goal number (...	courtieu	2011-12-16
*	Moving bullets (-, +, *) into stand-alone commands instead of being	courtieu	2011-12-16