coq - The formal proof system

Age	Commit message (Expand)	Author
2005-11-08	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin
2005-11-08	- debugging og "Show Intros": no line breaking + fresh ids	coq
2005-11-04	Point-virgule manquant ligne 914 détecté par nouveau warning X de ocaml 3.09	herbelin
2005-11-02	Types inductifs parametriques	mohring
2005-05-26	No parentheses around f in 'f \subst{...}'	herbelin
2005-05-26	Utilisation du module Buffer; encodage plus rigoureux des symboles en uri	herbelin
2005-05-26	Patch to avoid Whelp bug removed.	sacerdot
2005-05-20	New command: "Print Ltac qualid" to print user defined tactics.	sacerdot
2005-05-20	Interface vers outil de recherche Whelp	herbelin
2005-05-17	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...	herbelin
2005-05-15	Globalisation des Tactic Notation	herbelin
2005-04-20	Implementation of a new backtracking system, that allow to go back	coq
2005-03-11	Ajout récursif du répertoire COQLIB/user-contrib au chemin de chargement	herbelin
2005-03-01	Code mort	herbelin
2005-02-20	Keep ClosedSection marker for reset	herbelin
2005-02-18	Renaming Print Canonical Structure into Print Canonical Projections	herbelin
2005-02-18	Moving centralised discharge into dispatched discharge_function; required to ...	herbelin
2005-02-18	Moving centralised discharge into dispatched discharge_function; required to ...	herbelin
2005-02-18	Moving centralised discharge into dispatched discharge_function; required to ...	herbelin
2005-02-18	Moving centralised discharge into dispatched discharge_function; required to ...	herbelin
2005-02-12	Ajout Print Canonical Structures	herbelin
2005-02-06	Nettoyage et documentation de Library	herbelin
2005-01-21	Compatibilité ocamlweb pour cible doc	herbelin
2005-01-21	Compatibilité ocamlweb pour cible doc	herbelin
2005-01-14	Ajout de la syntaxe du reset label: "BackTo n".	coq
2005-01-14	Affichage numéro de l'état de la commande courante pour mode emacs	herbelin
2005-01-06	- Module/Declare Module syntax made more uniform:	sacerdot
2005-01-03	HUGE COMMIT	sacerdot
2005-01-02	Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...	herbelin
2005-01-02	Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...	herbelin
2005-01-02	Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...	herbelin
2004-12-30	Rétablissement d'un vrai Eval sous le contexte des définitions, pas un qui ...	herbelin
2004-12-09	Amélioration message localisation constructions et modules	herbelin
2004-12-06	Bug (cf #892)	herbelin
2004-12-03	Amélioration message d'erreur v8	herbelin
2004-11-29	Complétion commit précédent	herbelin
2004-11-26	Réduire pour trouver l'arité d'une classe	herbelin
2004-11-22	Correction bug Notation: il faut re-déclarer les règles de parsing des nota...	herbelin
2004-11-22	compatibility with POWERPC	gregoire
2004-11-19	Fusion OBJDEF et OBJDEF1 et renommage en CANONICAL-STRUCTUIRE	herbelin
2004-11-17	New command "Print Rewrite HindDb dbname".	sacerdot
2004-11-17	Ajout 'Locate Module'	herbelin
2004-11-16	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot
2004-11-12	* empty log message *	gregoire
2004-11-12	Changement dans les boxed values .	gregoire
2004-11-08	Prise en compte des notations récursives dans l'option 'format'	herbelin
2004-10-27	Non affichage des notations réduites à une variable	herbelin
2004-10-20	COMMITED BYTECODE COMPILER	barras
2004-10-17	Semble raisonnable de distinguer les noms aussi dans cant_apply	herbelin
2004-10-12	option -no-hash-consing pour supprimmer le hash-consing	filliatr