coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	coqide: blaster 2	monate	2003-05-23
*	maj	filliatr	2003-05-23
*	V8Notation	herbelin	2003-05-22
*	Ajout V8Notation	herbelin	2003-05-22
*	Réparation d'un bug de backtracking qui lui-même succédait à une ineffica...	herbelin	2003-05-22
*	Test backtracking	herbelin	2003-05-22
*	Ajout V8Notation	herbelin	2003-05-22
*	Preservation affichage des ?n en V7	herbelin	2003-05-22
*	coqide: blaster V1	monate	2003-05-22
*	Ocaml 3.00 a existe'	herbelin	2003-05-22
*	compat windows	filliatr	2003-05-22
*	maj	filliatr	2003-05-22
*	Suppression définitive de lmatch et or_metanum dans tacinterp	herbelin	2003-05-21
*	Suppression définitive de lmatch et or_metanum dans tacinterp	herbelin	2003-05-21
*	Mise en conformite de la precedence du '-' unaire avec celle de Notations (su...	herbelin	2003-05-21
*	Mise en conformite de la precedence du '-' unaire avec celle de Notations	herbelin	2003-05-21
*	Mise en conformite de la precedence du '-' unaire avec celle de Notations	herbelin	2003-05-21
*	Concentration des notations officielles dans Init/Notations; restructuration ...	herbelin	2003-05-21
*	Nouveaux tests	herbelin	2003-05-21
*	MAJ	herbelin	2003-05-21
*	Notations	herbelin	2003-05-21
*	Bug	herbelin	2003-05-21
*	Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...	herbelin	2003-05-21
*	MAJ	herbelin	2003-05-21
*	Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...	herbelin	2003-05-21
*	Possibilité de syntaxe conjointement à la définition des inductifs et des ...	herbelin	2003-05-21
*	maj	filliatr	2003-05-21
*	CoqIde: externals	monate	2003-05-20
*	Prise en compte notation dans Inductif pour traducteur	herbelin	2003-05-20
*	command_windows fix	monate	2003-05-20
*	Extension renommage	herbelin	2003-05-20
*	maj	filliatr	2003-05-20
*	Affichage META	herbelin	2003-05-19
*	Restructutation Hipattern Pattern	herbelin	2003-05-19
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	Restructuration des procédures de filtrage	herbelin	2003-05-19
*	* empty log message *	monate	2003-05-19