coq - The formal proof system

Age	Commit message (Expand)	Author
2006-05-30	Correction bug #990 (LoadPath et option -R de coqide	notin
2006-05-28	Ajout array_fold_map2Ã'	herbelin
2006-04-28	r8931@thot: notin \| 2006-04-28 16:19:38 +0200	notin
2006-04-27	Standardisation nom option_app en option_map	herbelin
2006-04-27	Modification of emacs output: Pp.warning and al now output warning	courtieu
2006-04-27	Modification of emacs output: Pp.warning and al now output warning	courtieu
2006-04-14	Si un fixpoint a plusieurs arguments, mais un seul de type inductif,	letouzey
2006-03-29	Ajout array_fold_map', list_fold_map' et list_remove_first	herbelin
2006-03-18	Documentation	herbelin
2006-02-07	Ajout plural	herbelin
2006-01-24	Suppression de la dépendance en Map.fold de ocaml dont la sémantique a	herbelin
2006-01-21	Déplacement de pr_arg et pr_opt de Ppconstr vers Util	herbelin
2006-01-03	Modification pour que l'ordre des éléments respecte l'ordre dans lequel ils...	herbelin
2005-12-28	Remplacement Pp.qs par Pptactic.qsnew	herbelin
2005-12-26	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des G_*...	herbelin
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin
2005-12-02	Changement des named_context	gregoire
2005-11-23	bug de coqide sous windows (bad file descriptor)	barras
2005-11-08	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin
2005-11-02	Types inductifs parametriques	mohring
2005-08-19	pas besoin de List.length pour savoir si une liste est vide	letouzey
2005-08-19	Sur le conseil de X.Leroy: x=[\|\|] devient Array.length x=0	letouzey
2005-05-26	New environment variable COQREMOTEBROWSER to set the command used by Coq	sacerdot
2005-05-19	Déplacement de fonctionnalités unix et browser de ide vers lib	herbelin
2005-05-17	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...	herbelin
2005-04-20	Implementation of a new backtracking system, that allow to go back	coq
2005-02-04	Bug synchronisation fonction connect	herbelin
2005-02-04	Ajout d'un processus de communication entre Coq et un outil externe	herbelin
2005-01-21	Compatibilité ocamlweb pour cible doc	herbelin
2005-01-21	Compatibilité ocamlweb pour cible doc	herbelin
2005-01-14	Code redondant (cf Printer)	herbelin
2004-12-24	Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...	herbelin
2004-11-12	Changement dans les boxed values .	gregoire
2004-10-20	COMMITED BYTECODE COMPILER	barras
2004-10-12	option -no-hash-consing pour supprimmer le hash-consing	filliatr
2004-09-06	optimized the non-backtracking case	barras
2004-07-29	Protection unloc	herbelin
2004-07-29	Bug join_loc	herbelin
2004-07-27	Utilisation de la variable camlp4 OCAML_308 plutôt que d'en reconstruire un...	herbelin
2004-07-17	Backtrack sur l'utilisation de pa_macro car n'existait pas en 3.06	herbelin
2004-07-16	Mise en place mécanisme de compatibilité ocaml 3.08	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2004-05-08	un argument booleen inutilisé dans expand_macros	letouzey
2004-03-05	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras
2004-02-16	Erreur dépendance en Util lui-même	herbelin
2004-02-13	Ajout array_map_left and co	herbelin
2004-02-12	Localisation des erreurs d'internalisation des notations de tactiques	herbelin
2004-01-29	Ajout option raw_print (Set Printing All) pour desactiver toute fonctionnalit...	herbelin
2003-12-31	* empty log message *	barras
2003-11-26	Export string_index_from	herbelin