coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	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