coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Add translations for many tactics but a dozen are still remaining	bertot	2003-01-25
*	Un type "standardisé" pour new_hyp	herbelin	2003-01-25
*	Inspect does not work for pcoq and there is no simple fix because inspect	bertot	2003-01-24
*	on cree toujours le sous-repertoire tactics/	filliatr	2003-01-24
*	The data constructed when detecting an error in a list of commands must	bertot	2003-01-24
*	Corrects the way conjunctions, existential quantifications, and arrows are	bertot	2003-01-24
*	maj	filliatr	2003-01-24
*	Make sure proof by pointing works.	bertot	2003-01-23
*	reparation des contribs: lors de l'unification, reduire les beta redexes	barras	2003-01-23
*	Ajout de LinearIntuition; Ajout de New(Tauto\|Intuition\|LinearIntuition).	corbinea	2003-01-23
*	Make proof by pointing work for the new notations of existential quantification.	bertot	2003-01-23
*	oubli des add_recursors singleton logiques	letouzey	2003-01-23
*	status de l'extraction	letouzey	2003-01-23
*	maj V7.4	letouzey	2003-01-23
*	MAJ	herbelin	2003-01-22
*	Mauvais environnement d'évaluation pour les globaux	herbelin	2003-01-22
*	* empty log message *	barras	2003-01-22
*	modified the unification algorithm to try first order unification before	barras	2003-01-22
*	Documentation du contenu de REALS	desmettr	2003-01-22
*	ajout de whd_state dans l'interface	barras	2003-01-22
*	Changements dans REALS	desmettr	2003-01-22
*	removes all references to ctast.ml the Makefile has been updated accordingly.	bertot	2003-01-22
*	Modifications dans SeqProp	desmettr	2003-01-22
*	Renommages dans Rtrigo_def	desmettr	2003-01-22
*	I changed the interface to make sure SearchAbout is defined according to	bertot	2003-01-22
*	Commentaires	desmettr	2003-01-22
*	Renommages nombreux	desmettr	2003-01-22
*	Commentaires	desmettr	2003-01-22
*	Correction bug réecriture à la racine pour le sétoide Prop.	clrenard	2003-01-22
*	Renommage f_pos -> IVT (Intermediate Value Theorem	desmettr	2003-01-22
*	Suppression d'un Import R_scope probablement oublie	desmettr	2003-01-22
*	Commentaires	desmettr	2003-01-22
*	Renommages dans RList	desmettr	2003-01-22
*	MAJ pour renommage Rcomplet	desmettr	2003-01-22
*	Renommages dans Rcomplete	desmettr	2003-01-22
*	Renommage Rcomplet.v -> Rcomplete.v	desmettr	2003-01-22
*	Suppression de lemmes superflus	desmettr	2003-01-22
*	Commentaires	desmettr	2003-01-22
*	Renommages dans PartSum	desmettr	2003-01-22
*	Bug 'with Module' corrige	coq	2003-01-22
*	Bug precedence	herbelin	2003-01-22
*	petit bug pp haskell	letouzey	2003-01-22
*	maj	filliatr	2003-01-22
*	Extraction des modules, enfin !	letouzey	2003-01-22
*	id_of_msid en plus	letouzey	2003-01-22
*	Adaptation à la nouvelle sémantique plus uniforme de "Match term"	herbelin	2003-01-21
*	Plus du tout de backtracking dans "Match term"; vrai Exit dans débogueur	herbelin	2003-01-21
*	portabilite	doligez	2003-01-21
*	Renommage dans MVT	desmettr	2003-01-21
*	MAJ dans Exp_prop	desmettr	2003-01-21