coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Fix in evarutil: add a conversion problem for ?x ts = ?x us only if ts and us...	msozeau	2012-02-15
*	In [reflexivity], [symmetry] etc, use the type found by looking at the relati...	msozeau	2012-02-14
*	- Fix dependency computation in eterm to not consider filtered variables.	msozeau	2012-02-14
*	Arguments supports extra notation scopes	gareuselesinge	2012-02-14
*	Additional comment on Focus Conditions.	aspiwack	2012-02-07
*	Documentation for Grab Existential Variables.	aspiwack	2012-02-07
*	A "Grab Existential Variables" to transform the unresolved evars at the end o...	aspiwack	2012-02-07
*	Typo in comments.	aspiwack	2012-02-07
*	correcting inversion in list of generated tcc of Function	letouzey	2012-02-03
*	More information returned by coqtop about its internal state. Hopefully we'll...	ppedrot	2012-02-02
*	Fix unblocking code in dependent destruction due to zeta being used in unfold...	msozeau	2012-02-01
*	Corrected a careless cut-and-paste in Gallina description which dated back to...	ppedrot	2012-02-01
*	Debugger vs tracer: Two different behaviors wrt printing: The debugger	herbelin	2012-02-01
*	Improved synchronisation of stdlib index page with current library state.	herbelin	2012-02-01
*	Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...	msozeau	2012-01-31
*	index-list.html.template: add missing files	pboutill	2012-01-31
*	Fix consequence of pp bugfix in testsuite	pboutill	2012-01-31
*	Makefile.build: add targets install-devfiles and install-ide-devfiles	pboutill	2012-01-31
*	Bug #2041: unfold at betaiotaZETA normalize like unfold	pboutill	2012-01-31
*	Fix camlp4 compilation	pboutill	2012-01-31
*	Added an pattern / occurence syntax for vm_compute.	ppedrot	2012-01-30
*	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-28
*	Printing bugs with match patterns:	herbelin	2012-01-27
*	Fail: discard the effects of a successful command (fix #2682)	letouzey	2012-01-26
*	Add support for plugin initialization function	gareuselesinge	2012-01-26
*	Check for unresolved evars in textual order of the params and fields declarat...	msozeau	2012-01-25
*	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-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