coq - The formal proof system

Age	Commit message (Expand)	Author
2008-12-14	Generalized binding syntax overhaul: only two new binders: `() and `{},	msozeau
2008-12-09	About "apply in":	herbelin
2008-12-04	Correct handling of defined methods (let-ins) in instance declarations.	msozeau
2008-11-28	Inductive parameters: nicer doc examples and error message	letouzey
2008-11-23	- Synchronized subst_object with load_object (load_and_subst_objects)	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-13	Tentative d'amélioration de la robustesse des Makefile générés par	notin
2008-11-10	Fix mixup between Record, Structure and Class by adding a new variant for	msozeau
2008-11-09	More factorization of inductive/record and typeclasses: move class	msozeau
2008-11-09	- Fixed bug 1968 (inversion failing due to a Not_found bug introduced in	herbelin
2008-11-07	Slight change of the semantics of user-given casts: they don't really	msozeau
2008-11-05	Fix in the unification algorithm using evars: unify types of evar	msozeau
2008-11-05	Move Record desugaring to constrintern and add ability to use notations	msozeau
2008-11-05	Petit bug dans le commit précédent.	aspiwack
2008-11-05	Nouvelle syntaxe pour écrire des records (co)inductifs :	aspiwack
2008-10-29	Remove calls to Dynlink.add_{interfaces,available_units} altogether	glondu
2008-10-28	Native "Declare ML Module" when possible	glondu
2008-10-28	11511 continued (bug in set.out + incohérence dans "Theorem with"	herbelin
2008-10-27	- Fixed many "Theorem with" bugs.	herbelin
2008-10-26	Fixes and refinements regarding occurrence selection:	herbelin
2008-10-26	- MAJ svn:ignore pour bin/coq-parser (anciennement bin/parser)	herbelin
2008-10-24	Raise informative errors instead of Failures or anomalies in case a meta	msozeau
2008-10-23	Open notation for declaring record instances.	msozeau
2008-10-23	Generalized implementation of generalization.	msozeau
2008-10-22	Fix bugs #1975 and #1976.	msozeau
2008-10-22	Affichage des notations récursives:	herbelin
2008-10-19	- Export de pattern_ident vers les ARGUMENT EXTEND and co.	herbelin
2008-10-11	Backporting 11445 from 8.2 to trunk (negative conditions in	herbelin
2008-10-08	Fix bug #1959 (remember: never use a partial functions mindlessly).	msozeau
2008-10-03	Minor fixes related to coqdoc and --interpolate and the dependent	msozeau
2008-09-15	Fix bug #1943 and restrict the inference optimisation of Program to	msozeau
2008-09-14	Add user syntax for creating hint databases [Create HintDb foo	msozeau
2008-09-14	In manual implicit arguments mode, do not enrich implicits	msozeau
2008-09-14	Fix bug #1936: uncaught exception due to undefinable exceptions.	msozeau
2008-09-14	Fix bug #1940: uncaught exception when searching for a type class.	msozeau
2008-09-11	Add enough information to correctly globalize recursive calls in inductive and	msozeau
2008-09-07	Add the ability to declare [Hint Extern]'s with no pattern.	msozeau
2008-09-07	Fixes in typeclasses resolution. Avoid reducing instances types before	msozeau
2008-09-02	Propagating commit 11343 from branch v8.2 to trunk (wish 1934 about	herbelin
2008-08-22	- New auto hints for transparency/opacity control, not bound to	msozeau
2008-08-21	Various fixes w.r.t typeclasses and subtac: resolve tcs properly inside	msozeau
2008-08-07	eviter redondance du message d'erreur (Error while reading / File)	barras
2008-08-05	Correction de bugs:	herbelin
2008-08-04	Report des commits 11297 et 11299 (nom Unnamed_theorem local caché par	herbelin
2008-08-04	Évolutions diverses et variées.	herbelin
2008-07-28	Fixes in generalize_eqs/dependent induction to allow the user to specify	msozeau
2008-07-26	- Pour CoRN, rétablissement notations Qgt/Qge (mais cette fois avec	herbelin