coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Many fixes in unification:	msozeau	2009-05-20
*	- Fixing declarative mode in presence of high use of Change_evars nodes	herbelin	2009-05-20
*	Fix in canonical structure resolution: [check_conv_record] may return	msozeau	2009-05-19
*	Remove camlp4-specific exception handling	msozeau	2009-05-19
*	Minor unification changes:	msozeau	2009-05-18
*	- Allowing multiple calls to tactic fix with automatic generation of	herbelin	2009-05-17
*	(Tentative to) add Canonical Structure resolution to the regular	msozeau	2009-05-16
*	Minor fixes in typeclasses:	msozeau	2009-05-16
*	Support for definition hooks in subtac.	msozeau	2009-05-16
*	Fix to my last notation patch: now fixpoint are correctly handled	vsiles	2009-05-13
*	minor bugfixes. CoqIde development will resume soon now ...	vgross	2009-05-13
*	micromega: proof compression bugfix	fbesson	2009-05-11
*	- Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: it	herbelin	2009-05-10
*	- 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-09
*	adds a theorem to reason at the level of Z	bertot	2009-05-07
*	Improvements in typeclasses eauto and generalized rewriting:	msozeau	2009-05-05
*	Fix a small notation/scope bug:	vsiles	2009-04-30
*	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-28
*	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-27
*	- Fixing #2090 (occur check missing when trying to solve evar-evar equation).	herbelin	2009-04-25
*	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-24
*	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