coq - The formal proof system

Age	Commit message (Expand)	Author
2012-01-31	Fix camlp4 compilation	pboutill
2012-01-30	Added an pattern / occurence syntax for vm_compute.	ppedrot
2012-01-28	Tentative to fix bug #2628 by not letting intuition break records. Might be t...	msozeau
2012-01-28	Fix simplification of ind. hyps., recognized by a [block] in their type (bug ...	msozeau
2012-01-27	Printing bugs with match patterns:	herbelin
2012-01-26	Fail: discard the effects of a successful command (fix #2682)	letouzey
2012-01-26	Add support for plugin initialization function	gareuselesinge
2012-01-25	Check for unresolved evars in textual order of the params and fields declarat...	msozeau
2012-01-23	Fix bug #2483: anomaly raised due to wrong handling of the evars state.	msozeau
2012-01-23	Fix typeclass resolution error message which included goal evars (bug #2620).	msozeau
2012-01-23	Fix for Program Instance not separately checking the resolution of evars of t...	msozeau
2012-01-23	Another quick hack that works this time, to handle printing of locality in Pr...	ppedrot
2012-01-23	Deleted the only use of BeginSubProof from the standard library.	ppedrot
2012-01-23	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	Bug 739: forbid dumpglob while using Coqtop in interactive mode	pboutill
2012-01-21	Coqtop and coqc: cleaning description of options in RefMan and manpages.	pboutill
2012-01-20	Added documentation for "r foo" in Ltac debugger.	herbelin
2012-01-20	Added documentation for "Set Parsing Explicit" + fixed mistakenly	herbelin
2012-01-20	Breakpoints in Ltac debugger: new command "r foo" to jump to the next	herbelin
2012-01-20	Added new command "Set Parsing Explicit" for deactivating parsing (and	herbelin
2012-01-20	Notations with binders: Accepting using notations for functional terms	herbelin
2012-01-20	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-19	Fix typeclass constraint grammar rule to allow `{_ : Reflexive A R}.	msozeau
2012-01-19	Added the btauto tactic to the documentation.	ppedrot
2012-01-19	Pretty printing of generalized binder	pboutill
2012-01-19	Boolean Option Patterns Compatibility	pboutill
2012-01-19	No more use of tauto in Init/	pboutill
2012-01-17	Fixed the pretty-printing of the Program plugin.	ppedrot
2012-01-17	Makefile: fix make distclean w.r.t. test-suite	letouzey
2012-01-17	MSetAVL: better implementation of filter suggested by X. Leroy	letouzey
2012-01-17	Some fix in beautify pretty-printer	pboutill
2012-01-16	Parameters in pattern first step.	pboutill
2012-01-16	Inductiveops.nb_*{,_env} cleaning	pboutill
2012-01-16	Bug 2679: Do not try to install cmxs with -byte-only	pboutill
2012-01-16	Bug 2676: ./configure --prefix shoudn't ask for a config directory.	pboutill
2012-01-16	make mli-doc fix	pboutill
2012-01-14	coq_micromega.ml: fix order of recursive calls to rconstant	glondu
2012-01-14	Add distclean back to test-suite/Makefile	glondu
2012-01-14	More newlines in debugging output of psatzl	glondu
2012-01-13	Added a Btauto plugin, that solves boolean tautologies.	ppedrot
2012-01-13	Added the decidability of (<=) on nat.	ppedrot
2012-01-12	Fix typo	glondu
2012-01-10	Fix printing of instances, generalized arguments.	msozeau
2012-01-07	Fix typo	glondu
2012-01-06	Fixed the itarget of the previous commit...	ppedrot
2012-01-06	Added a typeclass-based system to reason on decidable propositions.	ppedrot
2012-01-06	Forbids (as it has always been the behaviour) to have two different open	aspiwack