coq - The formal proof system

Age	Commit message (Expand)	Author
2001-02-16	ident au lieu de string pour le nom de base de qualid	herbelin
2001-02-16	Tentative d'amélioration affichage decls locales	herbelin
2001-02-16	MAJ	herbelin
2001-02-16	Suppression sp_of_id	herbelin
2001-02-16	Prise en compte noms longs dans SuperAuto	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-14	Renommage des variables dans les schémas d'induction	herbelin
2001-02-14	Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...	herbelin
2001-02-14	Bug affichage	herbelin
2001-02-14	MAJ	herbelin
2001-02-14	mise a jour	filliatr
2001-02-14	Stdlib -> Coqlib, Stock disparait	herbelin
2001-02-14	Mise en place d'un système optionnel de discharge immédiat; prise en compte...	herbelin
2001-02-14	Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...	herbelin
2001-02-14	prise en compte des défs locales dans les arguments des inductifs; meilleure...	herbelin
2001-02-14	Restructuration	herbelin
2001-02-14	uniformisation avec constr des lieurs dans rawterm/pattern	herbelin
2001-02-14	Obsolète (cf Coqlib)	herbelin
2001-02-14	Test syntaxe avec motifs numériques	herbelin
2001-02-13	Absolute URL for DTDs introduced	sacerdot
2001-02-13	Bug nommage Stdlib	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	Bug nombres en chiffres décimaux dans les Cases	herbelin
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	Bug point final dans la syntaxe theorem_body	herbelin
2001-02-09	MAJ	herbelin
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-09	exported a few functions that are used in graphical interface pcoq.	bertot
2001-02-09	Several pairs of different functions actually had the same name, so	bertot
2001-02-08	modif de la syntax: assoc a droite pour Ring	mayero
2001-02-08	Simplifications	herbelin
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	simplification du make depend; fonctions de stat. util. memoire dans certains...	filliatr
2001-02-08	modifs mineures	filliatr
2001-02-08	exporting traverse_to and mutate: they are used in pcoq.	bertot
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	code mort	herbelin
2001-02-07	Ajout du Match Context	delahaye
2001-02-07	Reparation du pretty-print pour les tactiques	delahaye
2001-02-07	Modif pour les patterns de sous-termes	delahaye
2001-02-07	Probleme synchronisation roots / inputstate	herbelin