coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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
*	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-02
*	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-02-01
*	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-31
*	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-30
*	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-29