coq - The formal proof system

Age	Commit message (Expand)	Author
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-06	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-05	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-03	Résolution d'un bug de simplification	delahaye
2001-02-02	* empty log message *	mohring
2001-02-02	* empty log message *	mohring
2001-02-02	Ajout des credits version V6.3	mohring
2001-02-02	Retire le warning stat	mohring
2001-02-02	retablissement (provisoire) de l'ancien Ring a cause d'une explosion en temps...	filliatr
2001-02-02	Nouvelle beta	herbelin
2001-02-01	bug Variable + Record	filliatr
2001-02-01	application patch Cuit Alvarado : tclTHENSi et intros_until_n exportés	filliatr
2001-02-01	* empty log message *	mohring
2001-02-01	Reparation reduce_to_mind	mohring
2001-02-01	oubli de Closure.EvalConstRef	filliatr
2001-02-01	- coqc : option -image	filliatr
2001-01-31	Bug localisation des Syntactif Definition	herbelin
2001-01-31	MAJ	herbelin
2001-01-31	Mise en place de la possibilite d'unfolder des variables locales et des const...	filliatr
2001-01-31	Bug lié au discharge	herbelin
2001-01-31	MAJ	herbelin
2001-01-31	Ajout option Set/Unset/Test Printing Coercions	herbelin
2001-01-31	Ajout d'espace dans les règles d'affichage des infix si des lettres figurent...	herbelin