coq - The formal proof system

Age	Commit message (Expand)	Author
2007-10-01	Amendement à la révision 10124 : déplacement de apprec_nohdbeta entre	herbelin
2007-09-28	Correction bug 1711	herbelin
2007-09-26	Complément aux commits 10124 et 10125 sur l'inférence de type (correction	herbelin
2007-09-25	Suppression de tous les alias de la forme x:=x dans la compilation du filtrage.	herbelin
2007-09-21	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-18	Correction de bugs lié au commit 10124 (décalage des indices de Bruijn)	herbelin
2007-09-17	Raffinement de l'algorithme d'inférence de type	herbelin
2007-09-16	Réponse à une incompatibilité introduite dans 10114 (calcul du nombre	herbelin
2007-09-06	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-04	Utilisation d'un nouvel algorithme plus raffiné pour prendre en compte les	herbelin
2007-09-01	Suite commit 10103 (expansion des défs locales triviales dans l'étape	herbelin
2007-08-29	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-27	Suppression des type_app et body_of_type qui alourdissent inutilement le code	herbelin
2007-08-25	Extension et documentation de real_clean/evar_define dans evarutil.ml:	herbelin
2007-08-10	- Correction d'un bug de de Bruijn dans abstract_predicate (lié au	herbelin
2007-08-09	Modification de control_only_guard, qui utilise maintenant	notin
2007-07-07	If a fixpoint is not written with an explicit { struct ... }, then	letouzey
2007-06-30	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-09	Various Program fixes, multiple pattern matches, aliases. Fix bug in coercion...	msozeau
2007-06-07	Unification des types + clause filtrage manquante + uniformisation locale	herbelin
2007-06-06	Toujours l'unification de apply : nouveau raffinement pour ne tester	herbelin
2007-06-05	Amélioration de la complexité de auto (l'utilisation des types dans	herbelin
2007-05-29	Correction d'un bug dans l'affichage du message d'erreur real_clean	herbelin
2007-05-28	Contrôle de la compatibilité de apply via une information dans les	herbelin
2007-05-24	Unification suite: petits affinements pour préserver la compatibilité	herbelin
2007-05-23	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-22	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin
2007-05-21	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-20	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin
2007-05-17	Nettoyage et standardisation des messages d'erreurs.	herbelin
2007-05-11	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack
2007-04-28	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin
2007-04-18	- Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771	herbelin
2007-04-14	Suite du commit 9760 : l'uniformisation du comportement de one_step_reduce,	herbelin
2007-04-13	Correction bug #1491	herbelin
2007-04-13	Nettoyage des tactiques basées sur "simpl" (delta-réduction cachant	herbelin
2007-03-27	Modification de la vm:	notin
2007-03-19	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau
2007-03-15	Suppression argument pattern_source du case_info (code jamais utilisé)	herbelin
2007-02-22	Ajout fonction clenv_conv_leq pour résoudre les pbs de la forme	herbelin
2007-02-21	Utilisation de l'environnement pour l'affichage de certains messages d'erreurs	herbelin
2007-02-21	Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGES	herbelin
2007-02-16	Add functionality to permit printing terms with references to anonymous varia...	msozeau