coq - The formal proof system

Age	Commit message (Expand)	Author
2003-11-29	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin
2003-11-29	Deplacement des fichiers ancienne syntaxe dans theories7, contrib7 et states7	herbelin
2003-11-29	Notation locale pour Rpower	herbelin
2003-11-29	Ajout lemmes, simplification preuve de SeqProp	herbelin
2003-11-29	MAJ	herbelin
2003-11-29	ground->firstorder, cc-> congruence, CC final commit	corbinea
2003-11-29	Renommages de variables dans RIneq	herbelin
2003-11-29	Utilisation nom dans message d'erreur implicite pas trouve	herbelin
2003-11-29	Utilisation du total_order non constructif	herbelin
2003-11-29	Report de lemmes de Znumtheory dans Zabs ou BinInt	herbelin
2003-11-29	Renommages discrets dans RIneq et Znumtheory	herbelin
2003-11-28	Protection contre les renommages; redondances	herbelin
2003-11-28	commands renomme en queries, command goto a la place de forward to backwardt o	marche
2003-11-28	Simplest Demo on modules	coq
2003-11-28	MAJ	herbelin
2003-11-28	maj	filliatr
2003-11-27	Suite commit precedent	herbelin
2003-11-27	Retour des _eq en v8	herbelin
2003-11-27	Qualification des noms utilisateurs en cas de collision avec un nom nouveau	herbelin
2003-11-27	Monstrueuse inefficacite due a l'innocence du redacteur de la ligne vis a vis...	herbelin
2003-11-27	Hint Destruct mal affiche	barras
2003-11-27	* empty log message *	barras
2003-11-27	Reparation bug compil	mohring
2003-11-27	maj	filliatr
2003-11-27	maj	filliatr
2003-11-27	Ajout ne_string	herbelin
2003-11-26	Traduction de @; simplification traduction des ident	herbelin
2003-11-26	Renommage de tactiques ltac coincidant avec certaines tactiques primitives	herbelin
2003-11-26	Protection contre les notations vides	herbelin
2003-11-26	Remplacement de l'indicateur de date "@" par 'at'	herbelin
2003-11-26	Export string_index_from	herbelin
2003-11-26	Traduction de tactic:constrarg en constr:constr pour les arguments de Tactic ...	herbelin
2003-11-26	just forgot something in previous commit	corbinea
2003-11-26	removal of CC.v lemata in cc (deprecated)	corbinea
2003-11-26	maj	filliatr
2003-11-25	Garder 'destruct using' a l'affichage ?	herbelin
2003-11-25	modif lexer: ident peut commencer par _	barras
2003-11-25	Version preliminaire pour la V8	herbelin
2003-11-25	Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...	herbelin
2003-11-25	Traduction Print Proof	herbelin
2003-11-25	CC: added injection theory	corbinea
2003-11-25	textes	marche
2003-11-25	maj	filliatr
2003-11-25	maj	filliatr
2003-11-24	about	marche
2003-11-24	MAJ	herbelin
2003-11-24	tentative de completion ESC-/ a la emacs	letouzey
2003-11-24	Prise en compte des defs syntaxiques dans is_global et global_reference qui p...	herbelin
2003-11-24	Renoncement de la compatibilite des noms qualifies au profit de la compatibil...	herbelin
2003-11-24	maj	filliatr