coq - The formal proof system

Age	Commit message (Expand)	Author
2009-05-13	minor bugfixes. CoqIde development will resume soon now ...	vgross
2009-05-11	micromega: proof compression bugfix	fbesson
2009-05-10	- Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: it	herbelin
2009-05-09	- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence	herbelin
2009-05-09	fix a bug in canonical structures (bug found and fixed by Cyril)	barras
2009-05-07	adds a theorem to reason at the level of Z	bertot
2009-05-05	Improvements in typeclasses eauto and generalized rewriting:	msozeau
2009-04-30	Fix a small notation/scope bug:	vsiles
2009-04-28	More efficient handling of evars in Program Fixpoint commands.	msozeau
2009-04-28	Fixes for bugs in r12110:	msozeau
2009-04-28	_tags: lexer.ml4 now uses pa_macro	letouzey
2009-04-28	Backporting 12112 from v8.2 branch to trunk (fixing documentation bugs	herbelin
2009-04-27	Cleanup old eauto code.	msozeau
2009-04-27	- Implementation of a new typeclasses eauto procedure based on success	msozeau
2009-04-27	- Fixed a little bug in previous commit (bad failure in case of unknown entry).	herbelin
2009-04-27	- Cleaning (unification of ML names, removal of obsolete code,	herbelin
2009-04-25	- Fixing #2090 (occur check missing when trying to solve evar-evar equation).	herbelin
2009-04-24	Report de la révision #12104 (Maj lien site web de Coq)	notin
2009-04-24	Backporting 12080 (fixing bug #2091 on bad rollback in the "where"	herbelin
2009-04-24	Fixing bug #2308 ("instantiate" tactic did not comply with	herbelin
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