coq - The formal proof system

Age	Commit message (Expand)	Author
2001-04-25	Amelioration message args constructeur	herbelin
2001-04-24	Messages d'erreur Cases	herbelin
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-19	-boot n'implique plus -batch	filliatr
2001-04-19	* empty log message *	courant
2001-04-14	Reparation du bug de Try	delahaye
2001-04-13	Mise en place d'un test de clauses non utilisees	herbelin
2001-04-09	Interdiction des 'Save (thm_tok)? id' si thm pas ouvert par Goal	herbelin
2001-04-09	Uniformisation des 'Save def_tok id'	herbelin
2001-04-09	nettoyage d'entrees de grammaires inutiles	courant
2001-04-09	branchement extraction en standard (pas de Require)	filliatr
2001-04-06	bug Print Proof; usage coqtop/coqc	filliatr
2001-04-04	renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...	filliatr
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-23	amelioration de la consommation memoire de la conversion en eta-expansant	barras
2001-03-21	option -verbose a coqc; option -i supprimée	filliatr
2001-03-15	entetes	filliatr
2001-03-11	Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisation	herbelin
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-28	Typo message Scheme	herbelin
2001-02-28	bug Reset et Sections	filliatr
2001-02-22	Stringmap -> Idmap	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-14	Erreur sur commit	herbelin
2001-02-14	Mise en place d'un système optionnel de discharge immédiat; prise en compte...	herbelin
2001-02-13	export a function that is needed in pcoq.	bertot
2001-02-13	Make sure the initial state used in a protected loop is the state chose exactly	bertot
2001-02-12	Theoreme opaques	mohring
2001-02-10	All errors were not well reported before. In particular syntax errors were	bertot
2001-02-09	Two pairs of parentheses were missing.	bertot
2001-02-09	option -m (utilisation memoire)	filliatr
2001-02-09	exported several functions that are used in the graphical interface pcoq.	bertot
2001-02-09	changed the design to have command groups executed in a protected manner	bertot
2001-02-08	Scratch par defaut si rien n'est specifier dans Add LoadPath	herbelin
2001-02-08	Suppression warning no .coqrc	herbelin
2001-02-08	export a function that can be used to retrieve the context corresponding	bertot
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-07	Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref	herbelin
2001-02-06	Ajout d'une commande pour afficher chaque coercion à la demandeparsing/g_bas...	herbelin
2001-02-05	Restructuration de classops; évolution en une version mieux intégrée au re...	herbelin
2001-02-05	Restructuration de classops; évolution en une version mieux intégrée au re...	herbelin
2001-01-31	Bug lié au discharge	herbelin