coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot	2004-11-16
*	* empty log message *	gregoire	2004-11-12
*	Changement dans les boxed values .	gregoire	2004-11-12
*	Prise en compte des notations récursives dans l'option 'format'	herbelin	2004-11-08
*	Non affichage des notations réduites à une variable	herbelin	2004-10-27
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	Semble raisonnable de distinguer les noms aussi dans cant_apply	herbelin	2004-10-17
*	option -no-hash-consing pour supprimmer le hash-consing	filliatr	2004-10-12
*	Suppression IsConjecture redondant avec Conjectural	herbelin	2004-10-11
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	hiding the meta_map in evar_defs	barras	2004-09-15
*	deplacement de clenv vers pretyping	barras	2004-09-03
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	Bug List.hd vs list_last	herbelin	2004-09-03
*	MAJ options coqtop et coqc	herbelin	2004-09-03
*	Pas de notation v7 si purement en v8	herbelin	2004-08-23
*	Correction bug #830 : les noms des implicites temporaires étaient inconnus a...	herbelin	2004-08-23
*	Amélioration message d'erreur objet de récursion de type non inductif	herbelin	2004-08-06
*	"Print Setoids" command added.	sacerdot	2004-07-23
*	Backtrack sur l'utilisation de pa_macro car n'existait pas en 3.06	herbelin	2004-07-17
*	Abstraction vis à vis du type loc pour compatibilité ocaml 3.08	herbelin	2004-07-16
*	Branchement sur pa_macro, pa_ifdef devenant obsolete en 3.08	herbelin	2004-07-16
*	Nouvelle en-tête	herbelin	2004-07-16
*	bug #780: compilation of several units in the same coqtop process	barras	2004-07-13
*	bug #790: better error_not_clean	barras	2004-07-13
*	updated printing of evar context (may loop ?)	corbinea	2004-06-30
*	Correction bug #776	herbelin	2004-06-28
*	correspondance des records et noms de champs de records entre un module et sa...	letouzey	2004-06-25
*	Recherche de la source à partir de la gauche pour gérer des cas comme 'Coer...	herbelin	2004-06-02
*	Affichage de la date de checkout même si pas dans le répertoire de compilation	herbelin	2004-05-26
*	Correction bug 'Time Load foo'	herbelin	2004-05-25
*	test de conversion laissait echapper exception NotConvertible	barras	2004-05-14
*	pb facto des Fixpoint + erreur avec -dump-glob et Load	barras	2004-04-17
*	Export de l'information si un inductive est un record ou non (pour xml)	herbelin	2004-03-31
*	Distinction entre declarations internes (p.ex. _subproof) et declarations uti...	herbelin	2004-03-30
*	Distinction entre declarations internes (p.ex. _subproof) et declarations uti...	herbelin	2004-03-30
*	Nom qualifié pour option -top	herbelin	2004-03-28
*	Ajout option -top pour changer le nom 'Top' du toplevel	herbelin	2004-03-28
*	Gestion maintenant purement fonctionnelle des implicites des point-fixes; ajo...	herbelin	2004-03-27
*	Ajout entree pour exporter les debuts et fins de compilation en mode -xml	herbelin	2004-03-26
*	Amelioration affichage des notations	herbelin	2004-03-17
*	Mise en place de motifs récursifs dans Notation; quelques simplifications au...	herbelin	2004-03-17
*	Adaptation a la v7 du message d'erreur Match_failure	herbelin	2004-03-16
*	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras	2004-03-05
*	ide: silent behavior better, save icon, -byte works	marche	2004-03-03
*	Traduction 'Cases' en pattern-matching	herbelin	2004-02-28
*	Eviter la stricte redondance de regles de grammaires v7	herbelin	2004-02-28
*	Keep structure information for Fixpoint declaration and Fix terms	bertot	2004-02-26
*	- fixed the Assert_failure error in kernel/modops	barras	2004-02-18
*	Ajout de lconstr, constr et binder_constr dans Print Grammar constr	herbelin	2004-02-17