coq - The formal proof system

Age	Commit message (Expand)	Author
2009-04-24	- New cleaning phase for the entry points of pretyping.ml	herbelin
2009-04-21	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-20	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-18	Just export RelationClasses for [Equivalence] through Setoid.	msozeau
2009-04-17	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-16	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-14	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-13	Rewrite of setoid_rewrite to modularize it based on proof-producing	msozeau
2009-04-10	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-09	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-08	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-07	Fixes in Program:	msozeau
2009-04-07	Move setoid_rewrite to its own module and do some clean up in	msozeau
2009-04-06	Fix behavior on newlines with parse-comments and also do [] escaping as	msozeau
2009-04-06	correction bug 2085	soubiran
2009-04-05	Display the content of the list instead of "<list>" when an idtac	herbelin
2009-04-03	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-03-31	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-30	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