coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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-10
*	maj	filliatr	2003-06-09
*	interaction entre fun/case permut et assert false	letouzey	2003-06-08
*	Tables logarithmiques pour les coercions + nettoyage	herbelin	2003-06-08
*	coqide: compile sans activate repare	monate	2003-06-06
*	bug CoqIDE avec Goal	filliatr	2003-06-06
*	Added new syntax definition	barras	2003-06-06
*	bugfix for Ground ( merci JC )	corbinea	2003-06-04
*	Ground update + some bugfix	corbinea	2003-06-04
*	au lieu de make	monate	2003-06-02
*	oups	letouzey	2003-05-30
*	maj	filliatr	2003-05-30
*	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-29
*	gestion plus fine des beta-redex lineaires (cf nb_occur_match)	letouzey	2003-05-28
*	'only parsing' pour le passage de trucT a truc	herbelin	2003-05-27
*	maj	filliatr	2003-05-27
*	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	2003-05-26
*	* empty log message *	monate	2003-05-26
*	configure pour CoqIde repare	monate	2003-05-26
*	Ground and CCsolve updates	corbinea	2003-05-25
*	"INZ" déplacé en V8 dans ZArith, juste syntaxique en V7 dans Reals	herbelin	2003-05-24
*	Amélioration affichage locations; prise en compte variables dans lettac; ajo...	herbelin	2003-05-24
*	Ajout FreshId	herbelin	2003-05-24
*	coqide: blaster 2	monate	2003-05-23
*	fabrication de ide/utf8.vo	letouzey	2003-05-23
*	Bug en mode translate	herbelin	2003-05-23
*	maj	filliatr	2003-05-23