coq - The formal proof system

Age	Commit message (Expand)	Author
2008-12-17	Better compatibility after commit 11693 by adding an alias OrderedTypeFacts.e...	letouzey
2008-12-17	FSet/OrderedType now includes an eq_dec, and hence become an extension of Dec...	letouzey
2008-12-17	Sequel of 11697: repair coqtop.byte when contribs are statically linked (+min...	letouzey
2008-12-16	Extraction Blacklist : a new command for avoiding conflicts with existing files	letouzey
2008-12-16	Extraction: also comply to Set Printing Width when producing external files	letouzey
2008-12-16	Take advantage of natdynlink when available: almost all contribs become loada...	letouzey
2008-12-16	Move FunctionalExtensionality to Logic/ (someone please check that the	msozeau
2008-12-16	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-15	Add some unicode symbols from japanese CJC (request by Y. Regis-Gianas)	letouzey
2008-12-14	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-12	- 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-11	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-10	Bug in 11662 (did not notice that dp_zenon.mll should be modified instead of	herbelin
2008-12-09	About "apply in":	herbelin
2008-12-08	Fix handling of [inverse] in setoid_rewrite, with an hopefully complete	msozeau
2008-12-06	Fix exponential behaviour of the typeclasses persistent objects. Drop	puech
2008-12-04	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-03	improved simpl	barras
2008-12-02	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-11-28	another bug with simpl	barras
2008-11-28	Inductive parameters: nicer doc examples and error message	letouzey
2008-11-27	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-26	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-25	correction bug 1997.	soubiran
2008-11-24	eventually fixing r11612	barras
2008-11-24	amelioration mineur du comportement de Function	jforest
2008-11-23	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-22	Fixed bug in VernacExtend printing + missing vernacular printing rules +	herbelin