coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Finish fix for the treatment of [inverse] in [setoid_rewrite], making a	msozeau	2008-12-16
*	Fix for syntax changes in test-suite scripts.	msozeau	2008-12-16
*	Add some unicode symbols from japanese CJC (request by Y. Regis-Gianas)	letouzey	2008-12-15
*	Fix looping class resolution bug discovered by B. Aydemir and use the	msozeau	2008-12-14
*	Fixes in the type classes documentation:	msozeau	2008-12-14
*	Generalized binding syntax overhaul: only two new binders: `() and `{},	msozeau	2008-12-14
*	- configure: do not strip coqtop on Darwin so as to support dynamic loading	herbelin	2008-12-12
*	Uniformity with the rest of the StdLib : _symm --> _sym	letouzey	2008-12-12
*	Fixed in bug in previous 11662 (incorrect with_evars flag in descend_conjunct...	herbelin	2008-12-12
*	Structural definition of PositiveMap.fold	glondu	2008-12-11
*	do not install coqchk cmi files	barras	2008-12-11
*	Make PositiveMap.xmapi structural	glondu	2008-12-11
*	Bug in 11662 (did not notice that dp_zenon.mll should be modified instead of	herbelin	2008-12-10
*	About "apply in":	herbelin	2008-12-09
*	Fix handling of [inverse] in setoid_rewrite, with an hopefully complete	msozeau	2008-12-08
*	Fix exponential behaviour of the typeclasses persistent objects. Drop	puech	2008-12-06
*	Do not catch _all_ exceptions in setoid unification.	msozeau	2008-12-04
*	Correct handling of defined methods (let-ins) in instance declarations.	msozeau	2008-12-04
*	Fix priority of the Leibniz Setoid instance to 10 (thanks to M. Lasson	msozeau	2008-12-04
*	Fixes for unification and substitution of metas under binders.	msozeau	2008-12-04
*	improved simpl	barras	2008-12-03
*	Add new directory for pre-compilation of files needed for further tests.	herbelin	2008-12-02
*	Miscellaneous fixes and improvements:	herbelin	2008-12-02
*	fixed kernel bug (de Bruijn) + test-suite	barras	2008-12-02
*	another bug with simpl	barras	2008-11-28
*	Inductive parameters: nicer doc examples and error message	letouzey	2008-11-28
*	Test case for previous commit.	msozeau	2008-11-27
*	Fix (?) a pattern matching compilation problem:	msozeau	2008-11-27
*	fixed non-exhaustive pattern matching	barras	2008-11-27
*	fixed bug 1791: simpl was performing eta expansion	barras	2008-11-27
*	added tests for hyps reordering	barras	2008-11-27
*	fixing problem with CompCert: reordering resulting from tac change was not cl...	barras	2008-11-27
*	closed bug 1898: fold x in x; added a reordering primitive tactic	barras	2008-11-26
*	closed bug 1898: fold x in x; added a reordering primitive tactic	barras	2008-11-26
*	correction bug 1997.	soubiran	2008-11-25
*	eventually fixing r11612	barras	2008-11-24
*	amelioration mineur du comportement de Function	jforest	2008-11-24
*	first attempt to allow Function to deal with dependent pattern matching. This...	jforest	2008-11-23
*	- Synchronized subst_object with load_object (load_and_subst_objects)	herbelin	2008-11-23
*	Fine-tuning rewriting from "eq_true b": using <- to rewrite true to b	herbelin	2008-11-23
*	Minor improvement to commit 11619	herbelin	2008-11-23
*	Fixed bug #2006 (type constraint on Record was not taken into account) +	herbelin	2008-11-23
*	Fixed bug in VernacExtend printing + missing vernacular printing rules +	herbelin	2008-11-22
*	- Fixed minor bug #1994 in the tactic chapter of the manual [doc]	herbelin	2008-11-22
*	fixed problem with r11612	barras	2008-11-21
*	fixed exponential behavior of evar unif (ground case)	barras	2008-11-21
*	correction of bug #2002	jforest	2008-11-20
*	Add implicit rules for native plugins (.cmxs)	glondu	2008-11-19
*	Execute #rectypes directive in embedded OCaml toplevel...	glondu	2008-11-19
*	Fix typo in omega doc	glondu	2008-11-19