coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	correction d'un stack overflow possible (PR#320)	letouzey	2003-08-28
*	Traducteur de correctness	herbelin	2003-08-14
*	code mort	herbelin	2003-08-14
*	Traduction mlnames	herbelin	2003-08-14
*	Notation access au dessous du niveau applicatif (2eme)	herbelin	2003-08-14
*	Notation access au dessous du niveau applicatif	herbelin	2003-08-13
*	Nouvelle mouture du traducteur v7->v8	herbelin	2003-08-11
*	Ground bugfix	corbinea	2003-07-11
*	bug typage du cases/identity: optim off si inductif avec vars	letouzey	2003-07-10
*	renommage des modules 1er niveau en monolithique	letouzey	2003-07-10
*	Ground update	corbinea	2003-07-08
*	bug match match	letouzey	2003-07-08
*	Ground bugfix	corbinea	2003-07-04
*	switching back to old tauto	corbinea	2003-07-03
*	modification ground	corbinea	2003-07-03
*	addition of Auto hints in Ground	corbinea	2003-07-03
*	added hints into Ground	corbinea	2003-07-02
*	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