coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Petites corrections ici et la	coq	2002-08-13
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pour	herbelin	2002-07-11
*	Ajout de FNL ou utilisation de msgnl	herbelin	2002-06-07
*	Intgration uniforme de coercions dans les dclarations (Variable and co) et re...	herbelin	2002-06-03
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	Plusieurs arguments autorisés pour Require et Read Module	herbelin	2002-01-18
*	Ajout syntaxe 'Canonical Structure' en remplacement de @Definition + suppress...	herbelin	2001-12-16
*	compat ocaml 3.03	filliatr	2001-12-13
*	- condition de garde (suite)	barras	2001-12-10
*	reparation de Locate	barras	2001-11-29
*	nouvel algo de conversion plus uniforme	barras	2001-11-29
*	Diverses petites simplications de la machine de preuves.	clrenard	2001-11-19
*	Choucroute entre les tables de synchronisation, les options -silent et les et...	letouzey	2001-11-08
*	GROS COMMIT:	barras	2001-11-05
*	Reorganisation de Goption. Passage des options l'utilisant en synchrone	letouzey	2001-10-30
*	Abstraction de l'immplementation de dirpath et implementation dans l'autre se...	herbelin	2001-10-17
*	Amélioration mise en page Print ML Module et Print ML Module	herbelin	2001-10-17
*	Suppression option immediate_discharge; nettoyage de Declare et conséquences	herbelin	2001-10-11
*	Réparation des options Set Printing and co	herbelin	2001-09-21
*	Mise en place globalisation optionnelle pour Infix/Distfix	herbelin	2001-09-21
*	Protection contre Not_found	herbelin	2001-09-21
*	Correction bug affichage Infix/Distfix	herbelin	2001-09-20
*	Transparent	barras	2001-09-20
*	Blindage de Show Intro	letouzey	2001-09-17
*	Suppression des library roots, on teste si un nom est absolu autrement	herbelin	2001-09-07
*	Parsing	herbelin	2001-08-10
*	ajout Show Intro(s)	letouzey	2001-07-04
*	Facilites pour le debogguage des univers.	coq	2001-05-29
*	Pretty -> Prettyp	filliatr	2001-05-28
*	amelioration des messages d'erreurs vis a vis des evars	barras	2001-05-23
*	Retire commenatires obsoletes	mohring	2001-04-20
*	un typage sûr pour Goal et Check	filliatr	2001-04-20
*	Cd est silencieux si -silent	filliatr	2001-04-19
*	Uniformisation des 'Save def_tok id'	herbelin	2001-04-09
*	Add a Comments command, that does nothing, but is quite useful to to have	bertot	2001-04-04
*	utilisation de Options.if_verbose	filliatr	2001-04-03
*	amelioration de la structure des univers	barras	2001-03-28
*	entetes	filliatr	2001-03-15
*	protection contre certaines exceptions levees par marshal_{in,out}	barras	2001-03-09
*	Déplacement de qualid dans Nametab, hors du noyau	herbelin	2001-03-01
*	ident au lieu de string pour le nom de base de qualid	herbelin	2001-02-16
*	Prise en compte noms longs dans Implicits	herbelin	2001-02-16
*	Theoreme opaques	mohring	2001-02-12
*	Scratch par defaut si rien n'est specifier dans Add LoadPath	herbelin	2001-02-08
*	Meilleure approche du conflit path/freeze/library_root en séquentialisant la...	herbelin	2001-02-07
*	Reparation du pretty-print pour les tactiques	delahaye	2001-02-07
*	Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dir	herbelin	2001-02-07
*	Ajout d'une commande pour afficher chaque coercion à la demandeparsing/g_bas...	herbelin	2001-02-06
*	Ajout option Set/Unset/Test Printing Coercions	herbelin	2001-01-31