coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	refined the conversion oracle	barras	2008-05-21
*	Léger backtrack sur commit coqide précédent (si la commande à annuler	herbelin	2008-05-20
*	- Fix bug related to indices of fixpoints.	msozeau	2008-05-13
*	MAJ et bricoles diverses	herbelin	2008-05-12
*	- Cleanup parsing of binders, reducing to a single production for all	msozeau	2008-05-11
*	Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ]	herbelin	2008-05-09
*	Mise en place d'un algorithme d'inversion des contraintes de type lors	herbelin	2008-05-05
*	Réutilisation de l'infrastructure pour le polymorphisme d'univers des	herbelin	2008-04-30
*	Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la	herbelin	2008-04-29
*	- Backtrack sur option with_types suite à confusion sur l'utilisation	herbelin	2008-04-27
*	- Backtrack sur extension de syntaxe pour pose qui rentre en conflit avec	herbelin	2008-04-26
*	Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour	herbelin	2008-04-26
*	Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve	herbelin	2008-04-25
*	Change default eauto depth to 100 in setoid_rewrite, bump necessary	msozeau	2008-04-23
*	Bug squashing day !	msozeau	2008-04-17
*	Mises à jour bugs, CHANGES, code mort	herbelin	2008-04-15
*	Document CHANGES in setoid rewrite, move DefaultRelation to	msozeau	2008-04-15
*	- Un peu de doc, préparation du CHANGES pour la release.	herbelin	2008-04-15
*	Bugs, nettoyage, et améliorations diverses	herbelin	2008-04-13
*	Suite 10760	herbelin	2008-04-05
*	Mise en place d'une extension de apply pour que celui-ci sache	herbelin	2008-04-04
*	Quelques améliorations des intro patterns:	herbelin	2008-04-04
*	Ajout "simple apply" et "simple eapply" pour apply sans unfold	herbelin	2008-04-01
*	Ajout d'abbréviations/notations paramétriques	herbelin	2008-03-30
*	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