coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	fixed CBV strategy: it was too eager on terms like	barras	2009-04-21
*	Rename [Morphism] into [Proper] and [respect] into [proper] to comply	msozeau	2009-04-21
*	Fix test output mentionning an existential number that changed.	msozeau	2009-04-20
*	Fix wrong pattern in Morphisms. Fix bug scripts to reflect the fact that	msozeau	2009-04-20
*	Just export RelationClasses for [Equivalence] through Setoid.	msozeau	2009-04-18
*	Only export the notations of Morphism as well as Equivalence through	msozeau	2009-04-17
*	- Fix handling of clauses in setoid_rewrite to rewrite under binders	msozeau	2009-04-17
*	comparison functions on lists and arrays	barras	2009-04-16
*	Fix bug #2089: correctly dealing with parameters and real arguments in	msozeau	2009-04-16
*	Better Requires in Classes. Fix bug #2093: the code does not require	msozeau	2009-04-16
*	nouvelle version de la tactique groebner proposee par Loic:	barras	2009-04-16
*	Rewrite autorewrite to use a dnet indexed by the left-hand sides (or	msozeau	2009-04-14
*	Add a combinator for rewriting given a list of terms and fix the	msozeau	2009-04-14
*	Correction du patch -rectypes pour ocaml 3.10	vsiles	2009-04-14
*	Some additions in Max and Zmax. Unifiying list of statements and names	herbelin	2009-04-14
*	Fix and actually beautify the bug script to adapt to the new measure	msozeau	2009-04-14
*	Rewrite of setoid_rewrite to modularize it based on proof-producing	msozeau	2009-04-13
*	Fix premature optimisation in dependent induction: even variable args need	msozeau	2009-04-10
*	Fix tauto no longer failing after commit 12077; appropriate error	herbelin	2009-04-10
*	Turning tauto into a classical tautology prover as soon as classical	herbelin	2009-04-09
*	Backtrack on 12061 (type checking for bug #2084 too strong as soon as we use	herbelin	2009-04-09
*	ocamlbuild: right symlink for csdpcert	letouzey	2009-04-08
*	Take formatted into account in rules for dot.	msozeau	2009-04-08
*	Experimental support for automatic destruction of recursive calls and	msozeau	2009-04-08
*	Fix bug #2083 for good: verify that the measure and relation are	msozeau	2009-04-08
*	Some dead code removal + cleanups	letouzey	2009-04-08
*	ocamlbuild: tags for new file tactics/rewrite.ml4	letouzey	2009-04-08
*	Change HTML paragraph output to avoid too much space after bulleted	msozeau	2009-04-08
*	Backport of Eric Le Lay's patch (bug report #2078) from v8.2 branch	herbelin	2009-04-08
*	- Fixing bug #2084 (unification not checking sort constraints), hoping	herbelin	2009-04-08
*	A first pearl found by the Oug analyzer: there were two list_map_i in Util	letouzey	2009-04-08
*	- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixing	herbelin	2009-04-08
*	Fixes in Program:	msozeau	2009-04-07
*	Move setoid_rewrite to its own module and do some clean up in	msozeau	2009-04-07
*	Fix behavior on newlines with parse-comments and also do [] escaping as	msozeau	2009-04-06
*	correction bug 2085	soubiran	2009-04-06
*	Display the content of the list instead of "<list>" when an idtac	herbelin	2009-04-05
*	Fix obvious bug in evars_of_named_context.	msozeau	2009-04-03
*	Ocamlbuild: option for (not) building coqide, better log messages	letouzey	2009-04-03
*	Makefile: ocamlbuild's _build is not traversed by find, and removed by make c...	letouzey	2009-04-03
*	Ocamlbuild: improvements suggested by N. Pouillard	letouzey	2009-04-03
*	Fix auto so that Extern tactics associated to no patterns can apply to	msozeau	2009-03-31
*	Committed patch sent by Samuel Bronson on Mar 14 2009 to take care of	herbelin	2009-03-31
*	Complementary fix to have ocamlopt_shared_os5fix.sh working correctly	herbelin	2009-03-31
*	Fix the fix script for ocamlopt -shared in MacOS 10.5 (remarks by Hugo)	letouzey	2009-03-30
*	Update CHANGES	glondu	2009-03-30
*	Document new quote construction	glondu	2009-03-30
*	Add tests for quote	glondu	2009-03-30
*	Add a more general quote construction	glondu	2009-03-30
*	Fix some typos and spaces	glondu	2009-03-30