coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Ground update	corbinea	2003-06-22
*	Ground update	corbinea	2003-06-20
*	Ground Update.	corbinea	2003-06-20
*	Ajout 'Symmetry in Hyp'	herbelin	2003-06-19
*	Ground update	corbinea	2003-06-16
*	ground update	corbinea	2003-06-16
*	Ground major update ... mmm, sounds exciting !	corbinea	2003-06-15
*	ground update	corbinea	2003-06-14
*	Major Ground update, may break semantics	corbinea	2003-06-14
*	Ajout option Local à Hint, Hints et HintDestruct	herbelin	2003-06-14
*	Ground update	corbinea	2003-06-13
*	Ground update, new files.	corbinea	2003-06-13
*	Utilisation de intro_pattern dans NewDestruct/NewInduction	herbelin	2003-06-13
*	Ground update.	corbinea	2003-06-13
*	enieme correction du nommage modulaire	letouzey	2003-06-12
*	fin de l'affichage des signatures de modules dans les *.ml	letouzey	2003-06-12
*	Typo	herbelin	2003-06-10
*	Ajout notation c.(f) en v8 pour les projections de Record	herbelin	2003-06-10
*	Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur de...	herbelin	2003-06-10
*	Ajout notation c.(f) en v8 pour les projections de Record	herbelin	2003-06-10
*	Globalisation de ce qui n'etait pas encore globalise	herbelin	2003-06-10
*	interaction entre fun/case permut et assert false	letouzey	2003-06-08
*	bugfix for Ground ( merci JC )	corbinea	2003-06-04
*	Ground update + some bugfix	corbinea	2003-06-04
*	oups	letouzey	2003-05-30
*	Ground daily update	corbinea	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
*	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
*	Ground and CCsolve updates	corbinea	2003-05-25
*	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
*	MAJ	herbelin	2003-05-21
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	Major Ground tactic update, sensible performance improvement	corbinea	2003-05-16
*	Notations arithmetiques	herbelin	2003-05-13
*	bugfixes in Ground.	corbinea	2003-05-08
*	Enhancement of the Ground tactic, addition of GTauto and GIntuition.	corbinea	2003-05-07
*	Localisation erreurs TacAlias; Globalisation moins tolérante dans les	herbelin	2003-04-28
*	bug concernant les projecteurs de Record avec args logiques	letouzey	2003-04-28
*	adaptation a Acc_iter	letouzey	2003-04-28
*	bugfix in Ground tactic	corbinea	2003-04-26
*	Added the Ground tactic.	corbinea	2003-04-25
*	Divers	herbelin	2003-04-17