coq - The formal proof system

Age	Commit message (Expand)	Author
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
2008-11-22	- Fixed minor bug #1994 in the tactic chapter of the manual [doc]	herbelin
2008-11-21	fixed problem with r11612	barras
2008-11-21	fixed exponential behavior of evar unif (ground case)	barras
2008-11-20	correction of bug #2002	jforest
2008-11-19	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-17	integrate suggestions by B. Baydemir (see #1930)	letouzey
2008-11-16	Univ: two < instead of a Pervasives.compare on int (as suggested by X. Leroy)	letouzey
2008-11-15	Correct display of constraints for Print Universes "dumpfile"	letouzey
2008-11-14	Amélioration du README.doc et de l'installation de la doc	notin
2008-11-14	Restores behaviour of v8.1 for unification problems which fail (backport of 1...	letouzey
2008-11-14	Faster comparison of universes	letouzey
2008-11-14	make doc ne compilait plus la doc de stdlib (bug #1996)	notin