coq - The formal proof system

Age	Commit message (Expand)	Author
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
2007-02-13	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin
2007-01-31	Correction d'un bug dans check_and_clear_in_constr + simplification de	notin
2007-01-30	Nouvelle implantation de clear_hyps	notin
2007-01-26	correction d'un bug d'efficacite dans le printer	jforest
2007-01-22	Correction du bug #1315:	notin
2007-01-22	Correction d'un bug d'unification-pattern dans l'algo d'unification	herbelin
2007-01-22	Correction pour le rapport de bug #1325 par rétablissement du	herbelin
2007-01-19	Protection contre les warnings 'unused variable' de ocaml 3.09	herbelin
2007-01-02	Rework subtac pattern matching equalities generation.	msozeau
2006-12-29	Protection contre une source possible de liaison de lambda anonyme	herbelin
2006-12-14	Confusion sur le paramètre à donner à concrete_name lors du commit 9450	herbelin
2006-12-13	Alignement de la politique de renommage de rename_bound_var (utilisé pour	herbelin
2006-12-12	Correction du bug #1273, deuxième version (avec des shémas d'elimination pl...	notin
2006-12-12	Correction du bug #1273 (problème avec les paramètres non récursivement un...	notin
2006-12-12	Backtrack sur suppression des vars anonymes des contextes d'evars (echec Case...	herbelin
2006-12-12	Correction bug #1041 (double cause : non évitement des noms existants en	herbelin
2006-12-09	Évitement des noms de constructeurs dans les motifs de filtrage de "match"	herbelin
2006-11-29	correction du bug : VM value extraction error (PR#1290)	bgregoir
2006-11-22	Code mort découvert par Matthieu	herbelin
2006-11-19	Dépendance inutile en Tacexpr, de proofs, qui se compile en principe après	herbelin
2006-11-19	Raffinement de l'unification de "apply": mémorisation de certains	herbelin
2006-11-18	Code mort (duplication de code dans reductionops.ml)	herbelin
2006-11-03	Suppression source de complexité polynomiale introduite par le polymorphisme	herbelin