coq - The formal proof system

Age	Commit message (Expand)	Author
2001-07-05	Débogage discharge des coercions; nettoyage	herbelin
2001-07-04	ajout Show Intro(s)	letouzey
2001-05-29	Retablissement de minicoq	coq
2001-05-29	Facilites pour le debogguage des univers.	coq
2001-05-28	Pretty -> Prettyp	filliatr
2001-05-28	option -quality	filliatr
2001-05-23	amelioration des messages d'erreurs vis a vis des evars	barras
2001-05-11	application patch Claudio	filliatr
2001-05-03	Changement de la structure des points fixes	barras
2001-04-25	ligne vide lors de l'affichage des messages d'erreur a toplevel entre	barras
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