coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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
*	factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )	corbinea	2003-03-31
*	minus a changé d'emplacement -> omega pas content	letouzey	2003-03-31
*	eq fusionne avec eqT et devient par défaut sur Type,	herbelin	2003-03-29
*	Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)	herbelin	2003-03-29
*	Extract Constant marche avec les axiomes schémas de types	letouzey	2003-03-25
*	Bugfix pour Linear.	corbinea	2003-03-24
*	Fin de la résurrection de Linear.	corbinea	2003-03-21
*	* empty log message *	barras	2003-03-12
*	* Ajout du traducteur nouvelle syntaxe *	barras	2003-03-12
*	pour coq-ide	letouzey	2003-03-11
*	pour ocamlweb	letouzey	2003-03-11