coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- Un peu de doc, préparation du CHANGES pour la release.	herbelin	2008-04-15
*	Fix setoid tests, use red for a Setoid_Theory lemma, and Parametric	msozeau	2008-04-14
*	Bugs, nettoyage, et améliorations diverses	herbelin	2008-04-13
*	Correction problème de compil (blast.ml)	herbelin	2008-04-04
*	Chgts mineurs:	herbelin	2008-04-03
*	Minor fixes. Use expanded type in class_tactics for Morphism search, to	msozeau	2008-04-02
*	Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient	herbelin	2008-04-01
*	Fix test-suite files, change conflicting notation "->rel" and the others	msozeau	2008-03-29
*	Improve error handling and messages for typeclasses.	msozeau	2008-03-28
*	- Second pass on implementation of let pattern. Parse "let ' par [as x]?	msozeau	2008-03-28
*	Correction du bug 1816 (ajout d'un lemme dans Znat) et suppression	notin	2008-03-28
*	Diverses petites modifs dans la test-suite:	notin	2008-03-26
*	Correction de bugs relatifs a la compostion des substitutions	soubiran	2008-03-25
*	Add the possibility of specifying constants to unfold for typeclass	msozeau	2008-03-17
*	Using the "relation" constant made some unifications fail in the new	msozeau	2008-03-16
*	Misc: Add test for bug 1704, now closed. Add usual syntax for lists in	msozeau	2008-03-16
*	Forgot the test file.	msozeau	2008-03-15
*	Backtrack sur le test censé discriminer entre une erreur d'evar non	herbelin	2008-03-15
*	Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)	herbelin	2008-03-10
*	New implementation of Add Relation as a DefaultRelation instance	msozeau	2008-03-08
*	Fix bugs that were reopened due to the change of setoid	msozeau	2008-03-08
*	f_equal, revert, specialize in ML, contradict in better Ltac (+doc)	letouzey	2008-03-07
*	Plug the new setoid implemtation in, leaving the original one commented	msozeau	2008-03-06
*	Correction d'un bug "ancestral": apply ne savait pas unifier ?n=?n	herbelin	2008-03-06
*	Correction d'une typo restant du commit 10557 et cause d'échec de contribs	herbelin	2008-03-05
*	congruence now knows about _ -> _	corbinea	2008-02-21
*	added products and sorts as possible heads for canonical structures	corbinea	2008-02-19
*	Added default canonical structures (see example in test-suite)	corbinea	2008-02-14
*	Backtrack changes on eauto, move specialized version of eauto in	msozeau	2008-02-14
*	Correction d'un bug de clear	notin	2008-02-11
*	Backport code from command.ml to subtac_command.ml for definining	msozeau	2008-02-08
*	Correction d'un bug à l'interprétation de "change" (on exigeait que	herbelin	2008-02-06
*	Ajout d'un test pour le bug #1787	notin	2008-02-05
*	Ajout de 2 tests	notin	2008-02-01
*	Beaoucoup de changements dans la representation interne des modules.	soubiran	2008-02-01
*	Unification de TacLetRecIn et TacLetIn. En particulier, on peut	herbelin	2008-02-01
*	Debug implementation of dependent induction/dependent destruction and documen...	msozeau	2008-01-31
*	Work on dependent induction tactic and friends, finish the test-suite example	msozeau	2008-01-30
*	Fermeture du bug #1754	notin	2008-01-24
*	Ajout d'un test pour le bug #1779	notin	2008-01-23
*	Ajout d'un test pour le mode déclaratif + test pour le bug #1776	notin	2008-01-23
*	Ajout de sauts de ligne dans l'affichage des scripts (cf commit 10445)	notin	2008-01-22
*	Correction du bug #1754	notin	2008-01-21
*	Better resolution of implicit parameters in typeclass binders, add extensiona...	msozeau	2008-01-02
*	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau	2007-12-31
*	Ajouts de quelques tests sur les bugs	notin	2007-12-21
*	Ajout d'un test pour le bug #1100	notin	2007-12-12
*	Test pour le bug #1754	notin	2007-12-11
*	Quelques exemples à méditer sur le polymorphisme d'universe des inductifs	herbelin	2007-10-24
*	Vérification que "rewrite in" se comporte comme "rewrite" et échoue	herbelin	2007-10-16