coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Prise en compte de notations numérales définies au niveau utilisateur+ lég...	herbelin	2006-01-08
*	Réorganisation; suppression code mort; documentation	herbelin	2006-01-07
*	Achèvement du commit incomplet de la révision 1.110 (cvs log toplevel/metas...	herbelin	2006-01-04
*	Mini-restructuration	herbelin	2005-12-30
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin	2005-12-26
*	Simplifification de vernac_expr li l'abandon du traducteur	herbelin	2005-12-23
*	Correction printer des Tactic Notation	herbelin	2005-12-23
*	Double bug de interp_modifiers anciennement caché par un troisième que les ...	herbelin	2005-12-22
*	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
*	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin	2005-11-08
*	Point-virgule manquant ligne 914 détecté par nouveau warning X de ocaml 3.09	herbelin	2005-11-04
*	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
*	HUGE COMMIT	sacerdot	2005-01-03
*	Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...	herbelin	2005-01-02
*	Correction bug Notation: il faut re-déclarer les règles de parsing des nota...	herbelin	2004-11-22
*	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot	2004-11-16
*	Prise en compte des notations récursives dans l'option 'format'	herbelin	2004-11-08
*	Non affichage des notations réduites à une variable	herbelin	2004-10-27
*	Pas de notation v7 si purement en v8	herbelin	2004-08-23
*	Nouvelle en-tête	herbelin	2004-07-16
*	Correction bug #776	herbelin	2004-06-28
*	Gestion maintenant purement fonctionnelle des implicites des point-fixes; ajo...	herbelin	2004-03-27
*	Amelioration affichage des notations	herbelin	2004-03-17
*	Mise en place de motifs récursifs dans Notation; quelques simplifications au...	herbelin	2004-03-17
*	Eviter la stricte redondance de regles de grammaires v7	herbelin	2004-02-28
*	Ajout de lconstr, constr et binder_constr dans Print Grammar constr	herbelin	2004-02-17
*	Correction d'un pb '{ _ }' et uniformisation du comportement de Notation et R...	herbelin	2004-02-13
*	Localisation des erreurs d'internalisation des notations de tactiques	herbelin	2004-02-12
*	Décomposition automatique des règles d'analyse syntaxique pour les	herbelin	2004-02-12
*	Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :...	herbelin	2004-01-29
*	reparation de qqs bugs du traducteur	barras	2004-01-26
*	Export information des references de notations pour coqdoc	herbelin	2004-01-21
*	Defaut d'information affichage en cas de notation incompatible	herbelin	2004-01-05
*	Suppression de l'espace avant les notations commencant par un ident	herbelin	2003-12-19
*	Traitement plus clair, notamment pour Locate, de quand quoter les composantes...	herbelin	2003-11-22
*	MAJ format et doc	herbelin	2003-11-21
*	Bug v8 (regles connues etaient re-enregistrees) + tables dans egrammar	herbelin	2003-11-15
*	petits changements de syntaxe	barras	2003-11-12
*	Fusion de tuple_constr/tuple_pattern dans operconstr/pattern	herbelin	2003-11-08
*	Pas de defaut a 1 et LeftA pour les infixes v8; fusion de l'univers et du nom...	herbelin	2003-11-01
*	Ajout de Print Visibility	herbelin	2003-10-28
*	Bug des terminaux quotés	herbelin	2003-10-17
*	En v7 sans traducteur, une incoherence virtuelle de syntaxe V8 n'est pas une ...	herbelin	2003-10-14
*	Changement 'as notation' en 'where notation'	herbelin	2003-10-14
*	changement nouvelle syntaxe (pt fixes)	barras	2003-10-10
*	Nouveau format de l'option 'format'	herbelin	2003-10-09
*	Des abbreviations pour constrintern.ml	herbelin	2003-10-08
*	Correction du bug 335 et Export/Require Export dans un module	coq	2003-10-07