coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Autres suppressions de composantes du traducteur	herbelin	2005-12-27
*	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-26
*	Changement de stratégie vis à vis du positionnement du module Top en mode b...	herbelin	2005-12-24
*	Simplifification de vernac_expr li l'abandon du traducteur	herbelin	2005-12-23
*	Correction printer des Tactic Notation	herbelin	2005-12-23
*	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-22
*	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-21
*	Abandon gestion des extensions de syntaxe de la v7 et du traducteur dans meta...	herbelin	2005-12-20
*	Suppression de la mise en boite automatique si format utilisateur	herbelin	2005-12-19
*	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-17
*	Changement des named_context	gregoire	2005-12-02
*	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-23
*	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-08
*	Point-virgule manquant ligne 914 détecté par nouveau warning X de ocaml 3.09	herbelin	2005-11-04
*	Types inductifs parametriques	mohring	2005-11-02
*	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-26
*	New command: "Print Ltac qualid" to print user defined tactics.	sacerdot	2005-05-20
*	Interface vers outil de recherche Whelp	herbelin	2005-05-20
*	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...	herbelin	2005-05-17
*	Globalisation des Tactic Notation	herbelin	2005-05-15
*	Implementation of a new backtracking system, that allow to go back	coq	2005-04-20
*	Ajout récursif du répertoire COQLIB/user-contrib au chemin de chargement	herbelin	2005-03-11
*	Code mort	herbelin	2005-03-01
*	Keep ClosedSection marker for reset	herbelin	2005-02-20
*	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-18
*	Ajout Print Canonical Structures	herbelin	2005-02-12
*	Nettoyage et documentation de Library	herbelin	2005-02-06
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
*	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-14
*	- Module/Declare Module syntax made more uniform:	sacerdot	2005-01-06
*	HUGE COMMIT	sacerdot	2005-01-03
*	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	2005-01-02