coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref	herbelin	2001-02-07
*	mise en place extraction	filliatr	2001-02-06
*	mise a jour	filliatr	2001-02-06
*	Correction pour les Unfold/Fold dans Cbv	delahaye	2001-02-06
*	EqDecide	filliatr	2001-02-06
*	Ajout d'un exemple	delahaye	2001-02-06
*	MAJ	herbelin	2001-02-06
*	Ajout d'une commande pour afficher chaque coercion à la demande	herbelin	2001-02-06
*	Ajout d'une commande pour afficher chaque coercion à la demandeparsing/g_bas...	herbelin	2001-02-06
*	Extension coerce_to_var	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-02-05
*	Meilleur traitement des noms explicites dans la Nametab; Différentation du t...	herbelin	2001-02-05
*	Restructuration de classops; évolution en une version mieux intégrée au re...	herbelin	2001-02-05
*	Correction pour Time pour ne pas etre oblige de mettre deux points	delahaye	2001-02-05
*	calcul des dependances camlp4 et production directe ml4 -> cmo (avec Judicael)	filliatr	2001-02-05
*	D'autres exemples	delahaye	2001-02-05
*	Pas d'Apply dans Tauto	delahaye	2001-02-05
*	Ajout d'une heuristique pour les types dependants	delahaye	2001-02-05
*	Ajout du test de Tauto	delahaye	2001-02-05
*	Message d'erreur plus explicite pour Tauto	delahaye	2001-02-05
*	rétablissement patch Claudio	filliatr	2001-02-05
*	rétablissement nouveau Tauto	filliatr	2001-02-05
*	Résolution d'un bug de simplification	delahaye	2001-02-03
*	* empty log message *	mohring	2001-02-02
*	* empty log message *	mohring	2001-02-02
*	Ajout des credits version V6.3	mohring	2001-02-02