coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Interpret patterns for hypotheses types in match goal in type_scope (if not a	msozeau	2008-03-25
*	Une passe sur les réels:	herbelin	2008-03-23
*	migration of the old IntMap library from StdLib to a user contrib (Cachan/Int...	letouzey	2008-03-19
*	Forget to update the CHANGES file after the commit r10180	vsiles	2008-03-11
*	Fix bugs that were reopened due to the change of setoid	msozeau	2008-03-08
*	Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part	msozeau	2008-03-07
*	Application patch #1807 sur hypothèse inutile de Rpower_O	herbelin	2008-02-27
*	Essai de prise en compte de delta dans unify_0 (même sur termes non clos).	herbelin	2008-02-13
*	Documentation of CHANGES and refman doc for the implicit argument binder	msozeau	2008-02-08
*	Suite révision 10495	herbelin	2008-02-01
*	Add new LetPattern construct to replace dest. syntax: let\| pat := t in b is b...	msozeau	2008-01-17
*	Suite ajout raccourcis à compute et lazy pour réduire tout sauf	herbelin	2007-11-09
*	Cleanup attempt of Hints in *Interface.v files.	letouzey	2007-10-21
*	Révision de theories/Logic concernant les axiomes de descriptions.	herbelin	2007-10-03
*	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin	2007-10-03
*	Ajout infos de débogage de "universe inconsistency" quand option Set	herbelin	2007-09-30
*	Forget to update the CHANGES file	vsiles	2007-09-28
*	Reals: prod_f_SO inclut f(0) dans le produit et devient prod_f_R0	herbelin	2007-09-27
*	Petit complément au commit 10131.	herbelin	2007-09-21
*	Utilisation d'un nouvel algorithme plus raffiné pour prendre en compte les	herbelin	2007-09-04
*	New bootstrapping, improved, Makefile system	corbinea	2007-07-13
*	More natural notation for intro pattern: @a -> ?a	glondu	2007-07-09
*	If a fixpoint is not written with an explicit { struct ... }, then	letouzey	2007-07-07
*	a few works about my commits since February	letouzey	2007-07-06
*	Documentation for commit 9774.	glondu	2007-07-06
*	New intro pattern "@A", which generates a fresh name based on A.	glondu	2007-07-06
*	- Ajout de la possibilité d'utiliser la notation Record pour les	herbelin	2007-06-30
*	Réaffichage des Structure/Record sous la forme Record	herbelin	2007-05-28
*	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin	2007-05-22
*	Nouveaux changements autour des implicites (notamment suite à	herbelin	2007-05-06
*	Suite commit 9810	herbelin	2007-04-29
*	Ajout de la possibilité de faire référence dans certains cas à un nom	herbelin	2007-04-28
*	Déplacement des opérations sur bool dans l'état initial	herbelin	2007-04-28
*	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin	2007-04-28
*	- Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771	herbelin	2007-04-18
*	Added the option to set/unset the automatic generation of elimination schemes	vsiles	2007-04-17
*	Nettoyage des tactiques basées sur "simpl" (delta-réduction cachant	herbelin	2007-04-13
*	Nouveau déplacement de constr, cette fois au niveau 8. En fait, il y a	herbelin	2007-04-11
*	Remontée de constr de 1 à 5 (pour permettre des notations entre 1 et 5	herbelin	2007-04-10
*	Added back the tactics [apply -> ident], etc. to Tactics.v after	emakarov	2007-04-02
*	Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGES	herbelin	2007-02-21
*	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin	2007-02-13
*	MAJ ring	herbelin	2007-01-31
*	Nouvelle approche pour le discharge modulaire	herbelin	2007-01-10
*	gestion speciale du niveau 5 des ltac	barras	2006-11-02
*	fixed field_simplify + changed precedence of let and fun in ltac	barras	2006-10-30
*	MAJ	herbelin	2006-10-28
*	MAJ	herbelin	2006-10-06
*	avertissement a propos du commit 9211 dans CHANGES	letouzey	2006-10-05
*	Correction bug #1204 + maj CHANGES	notin	2006-10-04