coq - The formal proof system

Age	Commit message (Expand)	Author
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
2001-01-30	Prise en compte du let-in dans lookup_*_as_renamed	herbelin
2001-01-30	MAJ	herbelin
2001-01-30	MAJ	herbelin
2001-01-30	Les Objdef introduisent une convertibilité avec les projections dans le test...	herbelin
2001-01-30	Branchement sur Objdef	herbelin
2001-01-30	Les Objdef introduisent une convertibilité avec les projections dans le test...	herbelin
2001-01-30	Bug fixed: the case [ id : ?1 -> ?2 \|- ?] was missing in tauto_main	sacerdot
2001-01-30	backtrack sur le lexeur de la V6	filliatr
2001-01-29	pas de warning avec Opaque quand is_silent	filliatr
2001-01-29	As an heuristic, now both in tauto and intuition we try to avoid the initial	sacerdot
2001-01-27	make doc	herbelin
2001-01-27	Ré-introduction des implicites à la volée dans la définition des inductifs	herbelin
2001-01-27	Simplification Impargs	herbelin
2001-01-27	Suppression du retrait du répertoire doc de l'archive tar-gzip-ée	herbelin
2001-01-27	Ajout alias mutual_inductive_path = section_path	herbelin