coq - The formal proof system

Age	Commit message (Expand)	Author
2002-07-11	Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pour	herbelin
2002-06-07	Ajout de FNL ou utilisation de msgnl	herbelin
2002-06-03	Intgration uniforme de coercions dans les dclarations (Variable and co) et re...	herbelin
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2002-01-18	Plusieurs arguments autorisés pour Require et Read Module	herbelin
2001-12-16	Ajout syntaxe 'Canonical Structure' en remplacement de @Definition + suppress...	herbelin
2001-12-13	compat ocaml 3.03	filliatr
2001-12-10	- condition de garde (suite)	barras
2001-11-29	reparation de Locate	barras
2001-11-29	nouvel algo de conversion plus uniforme	barras
2001-11-19	Diverses petites simplications de la machine de preuves.	clrenard
2001-11-08	Choucroute entre les tables de synchronisation, les options -silent et les et...	letouzey
2001-11-05	GROS COMMIT:	barras
2001-10-30	Reorganisation de Goption. Passage des options l'utilisant en synchrone	letouzey
2001-10-17	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-11	Suppression option immediate_discharge; nettoyage de Declare et conséquences	herbelin
2001-09-21	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-20	Correction bug affichage Infix/Distfix	herbelin
2001-09-20	Transparent	barras
2001-09-17	Blindage de Show Intro	letouzey
2001-09-07	Suppression des library roots, on teste si un nom est absolu autrement	herbelin
2001-08-10	Parsing	herbelin
2001-07-04	ajout Show Intro(s)	letouzey
2001-05-29	Facilites pour le debogguage des univers.	coq
2001-05-28	Pretty -> Prettyp	filliatr
2001-05-23	amelioration des messages d'erreurs vis a vis des evars	barras
2001-04-20	Retire commenatires obsoletes	mohring
2001-04-20	un typage sûr pour Goal et Check	filliatr
2001-04-19	Cd est silencieux si -silent	filliatr
2001-04-09	Uniformisation des 'Save def_tok id'	herbelin
2001-04-04	Add a Comments command, that does nothing, but is quite useful to to have	bertot
2001-04-03	utilisation de Options.if_verbose	filliatr
2001-03-28	amelioration de la structure des univers	barras
2001-03-15	entetes	filliatr
2001-03-09	protection contre certaines exceptions levees par marshal_{in,out}	barras
2001-03-01	Déplacement de qualid dans Nametab, hors du noyau	herbelin
2001-02-16	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-12	Theoreme opaques	mohring
2001-02-08	Scratch par defaut si rien n'est specifier dans Add LoadPath	herbelin
2001-02-07	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-06	Ajout d'une commande pour afficher chaque coercion à la demandeparsing/g_bas...	herbelin
2001-01-31	Ajout option Set/Unset/Test Printing Coercions	herbelin
2001-01-30	Branchement sur Objdef	herbelin
2001-01-29	pas de warning avec Opaque quand is_silent	filliatr