coq - The formal proof system

Age	Commit message (Expand)	Author
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin
2005-12-24	Changement de stratégie vis à vis du positionnement du module Top en mode b...	herbelin
2005-12-23	Simplifification de vernac_expr li l'abandon du traducteur	herbelin
2005-12-23	Correction printer des Tactic Notation	herbelin
2005-12-22	option '-top dir' now works also in batch mode (2ème)	herbelin
2005-12-22	option '-top dir' now works also in batch mode; it is even necessary to ensur...	herbelin
2005-12-22	Double bug de interp_modifiers anciennement caché par un troisième que les ...	herbelin
2005-12-21	Divers; restructuration des points d'entrée de Constrintern	herbelin
2005-12-21	Restructuration des points d'entrée de Pretyping et Constrintern	herbelin
2005-12-20	Abandon gestion des extensions de syntaxe de la v7 et du traducteur dans meta...	herbelin
2005-12-19	Suppression de la mise en boite automatique si format utilisateur	herbelin
2005-12-17	Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...	herbelin
2005-12-17	Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...	herbelin
2005-12-17	Orthographe de 'instantiate'	herbelin
2005-12-02	Changement des named_context	gregoire
2005-11-23	bug de coqide sous windows (bad file descriptor)	barras
2005-11-23	bug #909: Top n'est cree que si le contexte est vide	barras
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