coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Prise en compte des notations "alias" dans la globalisation des coercions.	herbelin	2007-11-08
*	Réparation d'une inefficacité bêtement introduite dans la révision	herbelin	2007-10-27
*	Bugfix in abstract_generalize	msozeau	2007-10-24
*	- Préservation des appels récursifs de tête dans ltac (réponse au "wish"	herbelin	2007-10-12
*	Uniformisation du comportement de rewrite et rewrite in : quand le	herbelin	2007-10-12
*	Allowing setoid_reflexivity_in to work on quantified hypothesis (bug #1710)	letouzey	2007-10-10
*	Added the automatic generation of the boolean equality if possible and the	vsiles	2007-10-05
*	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin	2007-10-03
*	Correcting error message when adding Setoid, Relation or morphism (bug #1626)	jforest	2007-10-02
*	Suite de 10157	herbelin	2007-09-30
*	Ajout infos de débogage de "universe inconsistency" quand option Set	herbelin	2007-09-30
*	On empêche "fresh" d'engendrer un mot-clé.	herbelin	2007-09-28
*	Découpage de Setoid.v	notin	2007-09-27
*	- Fixing bug 1703 ("intros until n" falls back on the variable name when	herbelin	2007-09-21
*	Raffinement de l'algorithme d'inférence de type	herbelin	2007-09-17
*	Uniformisation politique de nommage evd/isevars (evd si evar_defs,	herbelin	2007-09-06
*	Correction du bug #1634 + ajout de bugs dans la test-suite	notin	2007-08-22
*	Correction du bug #1322	notin	2007-08-16
*	Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;	notin	2007-08-16
*	Add a new tactic to generalize an instantiated inductive predicate adding equ...	msozeau	2007-08-07
*	Declarative language: fixed the generation of fixpoints for induction proofs.	corbinea	2007-07-24
*	Raffinement de interp_ident pour que l'ident interprété soit au choix	herbelin	2007-07-18
*	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