coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Slight cleanup of refl_omega.ml : in particular it uses now list	letouzey	2007-07-11
*	Adding a syntax for "n-ary" rewrite:	letouzey	2007-07-06
*	extension of the rename tactic: the following is now allowed:	letouzey	2007-07-06
*	New intro pattern "@A", which generates a fresh name based on A.	glondu	2007-07-06
*	killing some more non-exhaustive patterns	letouzey	2007-06-26
*	ajout de head0 et tail0 en natif	bgregoir	2007-06-20
*	Correction d'un bug dans l'affichage du message d'erreur real_clean	herbelin	2007-05-29
*	Contrôle de la compatibilité de apply via une information dans les	herbelin	2007-05-28
*	Retour à un message d'erreur d'apply qui montre un échec sans sans réduction	herbelin	2007-05-28
*	A fix for bug #1397:	letouzey	2007-05-23
*	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin	2007-05-22
*	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin	2007-05-20
*	Backtrack sur l'effacement dans le contexte de but des lieurs	herbelin	2007-05-19
*	Interprétation des listes de VarArgType dans les notations faisant	herbelin	2007-05-18
*	Wish #1582 (3eme)	herbelin	2007-05-18
*	Quelques essais autour du wish implicite au rapport de bug #1582 (2eme)	herbelin	2007-05-18
*	Quelques essais autour du wish implicite au rapport de bug #1582	herbelin	2007-05-18
*	correction de bug dans Function et augmentation de la classe des fonctions su...	jforest	2007-05-17
*	Correction des bugs #1537 (anomalie sur signature incomplète) et #1536	herbelin	2007-05-17
*	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack	2007-05-11
*	Multiples changements autour des implicites :	herbelin	2007-04-29
*	Ajout de la possibilité de faire référence dans certains cas à un nom	herbelin	2007-04-28
*	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin	2007-04-28
*	fixed glitch in escape	corbinea	2007-04-27
*	fin des conclusions multiples	corbinea	2007-04-26
*	New keyword "Inline" for Parameters and Axioms for automatic	soubiran	2007-04-25
*	debug plus poussé induction dépendante	corbinea	2007-04-18
*	- Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771	herbelin	2007-04-18
*	Export de simplest_eapply, utilisé dans la contrib interface	notin	2007-04-16
*	fix bug with dependent inductive families	corbinea	2007-04-16
*	Suite unification apply et eapply (l'un et l'autre profite maintenant	herbelin	2007-04-16
*	Essai de partage de code entre apply et eapply	herbelin	2007-04-15
*	Proposition de correction pour le bug #1173 (ou du moins pour un	herbelin	2007-04-13
*	Nettoyage des tactiques basées sur "simpl" (delta-réduction cachant	herbelin	2007-04-13
*	Extension to the general sequence operator (tactical). Now in addition to ...	emakarov	2007-04-02
*	Changement mineur du comportement de 'rewrite .. in * \|-': si le	notin	2007-03-30
*	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau	2007-03-19
*	Suppression argument pattern_source du case_info (code jamais utilisé)	herbelin	2007-03-15
*	Correction bug #1439 (comportement de replace by)	notin	2007-03-13
*	Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...	herbelin	2007-02-24
*	Ajout fonction clenv_conv_leq pour résoudre les pbs de la forme	herbelin	2007-02-22
*	Correction typo liée au commit 8779 (levait une anomalie)	herbelin	2007-02-21
*	Réparation absence d'interprétation des liaisons vers listes	herbelin	2007-02-15
*	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin	2007-02-13
*	bugfix suffices	corbinea	2007-02-09
*	Report de la révision r9605 de la branche v8.1 vers le trunk (abstract récu...	notin	2007-02-09
*	Report de la révision 9599 de la v8.1 dans le trunk	notin	2007-02-06
*	Suppression de code mort	notin	2007-02-01
*	redirection of errors in coqide + dynamic warning printer (needed for tm_egg)	corbinea	2007-01-31
*	bugfix for suffices (support for open head)	corbinea	2007-01-29