coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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-23
*	Coqtop and coqc: cleaning description of options in RefMan and manpages.	pboutill	2012-01-21
*	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-20
*	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-19
*	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-17
*	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-16
*	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-14
*	Added a Btauto plugin, that solves boolean tautologies.	ppedrot	2012-01-13
*	Added the decidability of (<=) on nat.	ppedrot	2012-01-13
*	Fix typo	glondu	2012-01-12
*	Fix printing of instances, generalized arguments.	msozeau	2012-01-10
*	Fix typo	glondu	2012-01-07
*	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	2012-01-06
*	Fixes bug #2654 (tactic instantiate failing to update existential variables).	aspiwack	2012-01-06
*	Backtracking on r14876 (fix for bug #2267): extra scopes might be	herbelin	2012-01-05
*	Fixing Arguments Scope bug when too many scopes are given (bug #2667).	herbelin	2012-01-04
*	Type inference unification: fixed a 8.4 bug in the presence of unification	herbelin	2012-01-04
*	Makefile.doc: attempt to solve race condition for creating doc/refman/html.	herbelin	2012-01-03
*	Bug 2669 and more: make full-stdlib	pboutill	2011-12-27
*	Coqdoc: Fixing missing newline when using "Proof term."	herbelin	2011-12-26
*	Reference Manual: misc fixes (spelling, index, updating pre-8.0 syntax).	herbelin	2011-12-26
*	update CHANGES w.r.t. simpl	gareuselesinge	2011-12-26