coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Ajout "at next level" dans Notation	herbelin	2003-04-17
*	commentaires	herbelin	2003-04-17
*	Ooops	letouzey	2003-04-17
*	temporaire	letouzey	2003-04-17
*	BIG MAJ Extraction:	letouzey	2003-04-16
*	Ajout option 'Local' à Infix et Notation	herbelin	2003-04-11
*	Explicitation arguments de eq	herbelin	2003-04-11
*	Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"	herbelin	2003-04-09
*	Alignement du comportement des implicites d'inductif en sortie de section sur...	herbelin	2003-04-09
*	Réorganisation de Impargs + mise en place d'une infrastructure	herbelin	2003-04-09
*	Mauvaise resolution conflit dans commit precedent	herbelin	2003-04-07
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	Légères simplifications code de Field; message d'erreur si pas égalité	herbelin	2003-04-03
*	remplace == par = dans la tactique field pour que le debugger marche a nouvea...	narboux	2003-04-01
*	Fail 1 pour traverser le match	herbelin	2003-04-01
*	Noms absolus	herbelin	2003-03-31
*	Plus de eqT; message Fail	herbelin	2003-03-31
*	Ajout d'un message à FailTac	herbelin	2003-03-31
*	Correcting a bug occuring when the mimicked function had a	courtieu	2003-03-31