coq - The formal proof system

Age	Commit message (Expand)	Author
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
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