coq - The formal proof system

Age	Commit message (Expand)	Author
2003-06-10	Deplacement delimiteur T dans Notations	herbelin
2003-06-10	Module Bij inutilise	herbelin
2003-06-10	Ajout notation c.(f) en v8 pour les projections de Record	herbelin
2003-06-10	freshid -> fresh	herbelin
2003-06-10	Déplacement traducteur de nom dans Constrextern pour accès aux noms longs	herbelin
2003-06-10	Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur de...	herbelin
2003-06-10	Simplification case_info	herbelin
2003-06-10	Ajout notation c.(f) en v8 pour les projections de Record; raffinement divers	herbelin
2003-06-10	Raffinement divers	herbelin
2003-06-10	Globalisation des tactiques avant traduction pour capture des noms; affinemen...	herbelin
2003-06-10	Distinction mode v7 ou translate; conséquences du déplacement traducteur de...	herbelin
2003-06-10	Déplacement de code dans command; MAJ DebugOn	herbelin
2003-06-10	Mise en place structure pour des 'arguments scope' dirigés par une classe	herbelin
2003-06-10	Amélioration afficheur de Cases pour les constr_pattern	herbelin
2003-06-10	Passage des noms de tactiques à kernel_name pour compatibilité avec les fon...	herbelin
2003-06-10	Déplacement traducteur de nom dans Constrextern pour accès aux noms longs	herbelin
2003-06-10	Ajout notation c.(f) en v8 pour les projections de Record	herbelin
2003-06-10	Factorisation de detype_case pour utilisation par l'afficheur de pattern	herbelin
2003-06-10	Traducteur + passage des noms de tactiques à kernel_name pour compatibilité...	herbelin
2003-06-10	Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur de...	herbelin
2003-06-10	Amélioration afficheur de Cases pour les constr_pattern	herbelin
2003-06-10	Extension de Locate sur les symboles avec recherche de sous-chaînes; mise en...	herbelin
2003-06-10	Globalisation de ce qui n'etait pas encore globalise	herbelin
2003-06-10	code mort	herbelin
2003-06-10	Ajout fonctions de recherche de sous-chaines (merci a Jacek)	herbelin
2003-06-09	maj	filliatr
2003-06-08	interaction entre fun/case permut et assert false	letouzey
2003-06-08	Tables logarithmiques pour les coercions + nettoyage	herbelin
2003-06-06	coqide: compile sans activate repare	monate
2003-06-06	bug CoqIDE avec Goal	filliatr
2003-06-06	Added new syntax definition	barras
2003-06-04	bugfix for Ground ( merci JC )	corbinea
2003-06-04	Ground update + some bugfix	corbinea
2003-06-02	au lieu de make	monate
2003-05-30	oups	letouzey
2003-05-30	maj	filliatr
2003-05-29	Bug niveau	herbelin
2003-05-29	niveau 49 devient next	herbelin
2003-05-29	Ground daily update	corbinea
2003-05-29	niveau 49 devient next	herbelin
2003-05-29	Ne pas mettre d'associatif a droite au niveau 3 en V7	herbelin
2003-05-29	:= dans un record engendre un LetIn qui n'etait pas géré	letouzey
2003-05-28	gestion plus fine des beta-redex lineaires (cf nb_occur_match)	letouzey
2003-05-27	'only parsing' pour le passage de trucT a truc	herbelin
2003-05-27	maj	filliatr
2003-05-26	coqide: blaster interruptible	monate
2003-05-26	Bug	herbelin
2003-05-26	GIntuition now matches Intuition up to hyps renaming.	corbinea
2003-05-26	Added breakpoint in Ground tactic.	corbinea
2003-05-26	moved engine.ml4 to ground.ml4, added option 'Ground Depth'	corbinea