coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Prise en compte noms longs dans Implicits	herbelin	2001-02-16
*	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-14
*	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-13
*	Bug nombres en chiffres décimaux dans les Cases	herbelin	2001-02-12
*	Theoreme opaques	mohring	2001-02-12
*	All errors were not well reported before. In particular syntax errors were	bertot	2001-02-10
*	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-09
*	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-08
*	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	2001-02-07
*	Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dir	herbelin	2001-02-07
*	Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dir	herbelin	2001-02-07
*	Message d'erreur absolute_reference	herbelin	2001-02-07
*	Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref	herbelin	2001-02-07
*	Chgt signature de type_of_existential	herbelin	2001-02-07