coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau	2009-03-28
*	Many changes in the Makefile infrastructure + a beginning of ocamlbuild	letouzey	2009-03-20
*	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack	2009-02-19
*	pushed evar reduction in kernel	barras	2009-02-06
*	Fixing #2044 (bad printing of primitive notation at the head of	herbelin	2009-02-06
*	Fixing a bug in 11804 (support for _ in ident entry of notations).	herbelin	2009-01-20
*	- Structuring Numbers and fixing Setoid in stdlib's doc.	herbelin	2009-01-19
*	DISCLAIMER	puech	2009-01-17
*	Switched to "standardized" names for the properties of eq and	herbelin	2009-01-01
*	- Added support for subterm matching in SearchAbout.	herbelin	2008-12-29
*	Generalized binding syntax overhaul: only two new binders: `() and `{},	msozeau	2008-12-14
*	More factorization of inductive/record and typeclasses: move class	msozeau	2008-11-09
*	Move Record desugaring to constrintern and add ability to use notations	msozeau	2008-11-05
*	Correct enormous bug in interpretation of generalized binders: it simply	msozeau	2008-10-26
*	Open notation for declaring record instances.	msozeau	2008-10-23
*	Generalized implementation of generalization.	msozeau	2008-10-23
*	Fix bugs #1975 and #1976.	msozeau	2008-10-22
*	A much better implementation of implicit generalization:	msozeau	2008-10-22
*	Affichage des notations récursives:	herbelin	2008-10-22
*	- Export de pattern_ident vers les ARGUMENT EXTEND and co.	herbelin	2008-10-19
*	Dumpglob.dump_modref : fix an assert failure	letouzey	2008-10-14
*	Backporting 11445 from 8.2 to trunk (negative conditions in	herbelin	2008-10-11
*	Améliorations de l'affichage des coercions suggérées par Georges :	herbelin	2008-10-08
*	Fix bug #1943 and restrict the inference optimisation of Program to	msozeau	2008-09-15
*	Add enough information to correctly globalize recursive calls in inductive and	msozeau	2008-09-11
*	Better handling of the opacity of proof obligations, add the possibility of	msozeau	2008-09-07
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	Suite commit 11236	notin	2008-07-24
*	Stop glob messages to be printed by default on stdout	letouzey	2008-07-23
*	Correct implementation of discharging of implicit arguments and add new	msozeau	2008-07-22
*	Oubli lors du commit #11236	notin	2008-07-22
*	Suite commit 11236	notin	2008-07-21
*	Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...	notin	2008-07-18
*	Modification rapide du message d'erreur lorsqu'un _ ne peut être	herbelin	2008-07-18
*	Uniformisation du format des messages d'erreur (commencent par une	herbelin	2008-07-17
*	Autour du parsing:	herbelin	2008-07-15
*	Utilisation de try_locate_qualified_library au lieu de locate_qualified_libra...	notin	2008-07-07
*	- Improve [Context] vernacular to allow arbitrary binders, not just	msozeau	2008-07-07
*	Fixes in handling of implicit arguments:	msozeau	2008-07-04
*	Documentation Prop<=Set et Arguments Scope Global	herbelin	2008-07-01
*	Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...	notin	2008-06-25
*	Code cleanup in typeclasses, remove dead and duplicated code.	msozeau	2008-06-21
*	Correction bug 1878 (utilisation de extend_evar déplacée là où une	herbelin	2008-06-14
*	- Extension de "generalize" en "generalize c as id at occs".	herbelin	2008-06-08
*	Enhancements to coqdoc, better globalization of sections and modules.	msozeau	2008-06-06
*	Fix setoid_rewrite documentation examples.	msozeau	2008-06-03
*	Improvements on coqdoc by adding more information into .glob	msozeau	2008-05-30
*	Notation concise pour la valeur par défaut des cas reconnus comme	herbelin	2008-05-28
*	Ajout de la possibilité d'utiliser fix/cofix dans les notations.	herbelin	2008-05-24
*	Fix "not an applied typeclass" error for legitimate classes	msozeau	2008-05-12