coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Réparation bug Inversion (#212)	herbelin	2002-10-14
*	Meilleure analyse de si une règle de grammaire/syntaxe existent déjà ou pas	herbelin	2002-10-14
*	Ajout optino_iter	herbelin	2002-10-14
*	Parenthèses forcées autour des arguments d'une application pour parser	herbelin	2002-10-14
*	La règle pour parser "(1)", "(2)", ... entre en conflit avec les expressions	herbelin	2002-10-14
*	Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'une	herbelin	2002-10-14
*	coqdep bogué, retour sur version 1.75	herbelin	2002-10-14
*	maj	filliatr	2002-10-14
*	Bug affichage du chiffre 0	herbelin	2002-10-13
*	MAJ	herbelin	2002-10-13
*	Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...	herbelin	2002-10-13
*	Moins de restriction sur le commit précédent	herbelin	2002-10-13
*	Ajout map_rawconstr	herbelin	2002-10-13
*	Mise en place d'ensembles de notations symboliques pour nat, Z et R	herbelin	2002-10-13
*	Nettoyage	herbelin	2002-10-13
*	Déplacement de + et * aux niveaux de précédence 7 et 6	herbelin	2002-10-13
*	Déplacement de + et * aux niveaux de précédence 7 et 6	herbelin	2002-10-13
*	Première proposition d'un type ML exprimant la syntaxe de constr; nettoyage	herbelin	2002-10-13
*	Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...	herbelin	2002-10-13
*	réparation de la protection contre les clauses indiscernables de TACTIC EXTE...	herbelin	2002-10-12
*	Notation 2:Check et 2:Eval	herbelin	2002-10-12
*	Restriction sur la forme des Syntactic Definition et re-localisation en fonct...	herbelin	2002-10-12
*	Nettoyage	herbelin	2002-10-12
*	Forcer la réouverture d'un fichier explicitement requis même si le	herbelin	2002-10-12
*	maj	filliatr	2002-10-11
*	Ajout ClassicalFacts	herbelin	2002-10-10
*	gestion coherente de l'option -R et des Require A.B.C.	barras	2002-10-10
*	Nametab permet de definir le meme truc la deuxieme fois	coq	2002-10-10
*	retour en arriere concernant la recherche d'occurence modulo expansion des le...	barras	2002-10-09
*	Preuve du lemme de Rolle	desmettr	2002-10-09
*	MAJ pour modification dans Rcomplet	desmettr	2002-10-09
*	Suppression d'un lemme redondant	desmettr	2002-10-09
*	Proof of Heine's theorem	desmettr	2002-10-09
*	maj	filliatr	2002-10-09
*	Subst ne fait pas clear sur x:=e	filliatr	2002-10-08
*	maj	filliatr	2002-10-08
*	Une fonction de moins dans .mli	coq	2002-10-07
*	Lazy manuelles dans le code	coq	2002-10-07
*	* empty log message *	desmettr	2002-10-07
*	* empty log message *	courant	2002-10-07
*	Quelques resultats complementaires	desmettr	2002-10-07
*	Affaiblissement des hypotheses dans TAF_gen	desmettr	2002-10-07
*	Make sure that bin/parser exists when checking that it works	bertot	2002-10-07
*	maj	filliatr	2002-10-07
*	correcting the treatment of many tactics that use quant_hyp in file xlate.ml	bertot	2002-10-06
*	Lazy experimentale temporaire...	coq	2002-10-05
*	pretty s'appellait prettyp mais il est revenu sous son ancien nom	herbelin	2002-10-05
*	Ajout du lemme derivable_pt_lim_power	desmettr	2002-10-04
*	Preuve de Bolzano-Weierstrass	desmettr	2002-10-04
*	Re-introduce the treatement of Tacticals that Hugo had already done in	bertot	2002-10-04