coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- 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
*	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin	2007-10-03
*	Amendement à la révision 10124 : déplacement de apprec_nohdbeta entre	herbelin	2007-10-01
*	Correction bug 1711	herbelin	2007-09-28
*	Complément aux commits 10124 et 10125 sur l'inférence de type (correction	herbelin	2007-09-26
*	Suppression de tous les alias de la forme x:=x dans la compilation du filtrage.	herbelin	2007-09-25
*	Petit complément au commit 10131.	herbelin	2007-09-21
*	- Fixing bug 1703 ("intros until n" falls back on the variable name when	herbelin	2007-09-21
*	Correction de bugs lié au commit 10124 (décalage des indices de Bruijn)	herbelin	2007-09-18
*	Raffinement de l'algorithme d'inférence de type	herbelin	2007-09-17
*	Réponse à une incompatibilité introduite dans 10114 (calcul du nombre	herbelin	2007-09-16
*	Uniformisation politique de nommage evd/isevars (evd si evar_defs,	herbelin	2007-09-06
*	Itération sur les sous-termes dans la vérification de la condition de garde	herbelin	2007-09-06
*	Utilisation d'un nouvel algorithme plus raffiné pour prendre en compte les	herbelin	2007-09-04
*	Suite commit 10103 (expansion des défs locales triviales dans l'étape	herbelin	2007-09-01
*	Prise en compte des redéfinitions de variables (définitions locales	herbelin	2007-08-29
*	- Débogueur: positionnement de set_detype_anonymous pour ne pas	herbelin	2007-08-29
*	Suppression des type_app et body_of_type qui alourdissent inutilement le code	herbelin	2007-08-27
*	Extension et documentation de real_clean/evar_define dans evarutil.ml:	herbelin	2007-08-25
*	- Correction d'un bug de de Bruijn dans abstract_predicate (lié au	herbelin	2007-08-10
*	Modification de control_only_guard, qui utilise maintenant	notin	2007-08-09
*	If a fixpoint is not written with an explicit { struct ... }, then	letouzey	2007-07-07
*	Correction bug sur factorisation affichage paramètres (cf r9918)	herbelin	2007-06-30
*	Factorisation des types dans l'affichage des paramètres des (Co)Inductif/Record	herbelin	2007-06-30
*	- Ajout de la possibilité d'utiliser la notation Record pour les	herbelin	2007-06-30
*	Various Program fixes, multiple pattern matches, aliases. Fix bug in coercion...	msozeau	2007-06-09
*	Unification des types + clause filtrage manquante + uniformisation locale	herbelin	2007-06-07
*	Toujours l'unification de apply : nouveau raffinement pour ne tester	herbelin	2007-06-06
*	Amélioration de la complexité de auto (l'utilisation des types dans	herbelin	2007-06-05
*	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
*	Unification suite: petits affinements pour préserver la compatibilité	herbelin	2007-05-24
*	Tentative d'insertion de coercions avant unification si le type de la	herbelin	2007-05-23
*	Suite restructuration unification et division des problèmes	herbelin	2007-05-23
*	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin	2007-05-22
*	Essai d'une nouvelle heuristique pour clenv_unique_resolver : si le	herbelin	2007-05-21
*	Protection d'un warning par if_verbose	herbelin	2007-05-21
*	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin	2007-05-20
*	Nettoyage et standardisation des messages d'erreurs.	herbelin	2007-05-17
*	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack	2007-05-11
*	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
*	Suite du commit 9760 : l'uniformisation du comportement de one_step_reduce,	herbelin	2007-04-14
*	Correction bug #1491	herbelin	2007-04-13
*	Nettoyage des tactiques basées sur "simpl" (delta-réduction cachant	herbelin	2007-04-13
*	Modification de la vm:	notin	2007-03-27
*	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
*	Ajout fonction clenv_conv_leq pour résoudre les pbs de la forme	herbelin	2007-02-22