coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	* empty log message *	courant	2003-01-31
*	MAJ syntaxe modules + nouveau fichier mod_decl qui explique tout	coq	2003-01-31
*	Pour satisfaire ProofGeneral	coq	2003-01-31
*	maj	filliatr	2003-01-31
*	Pb de parenthèse dans "Check (S (plus O O))"	herbelin	2003-01-30
*	Adds a possibility to construct a term as if it had been parsed through	bertot	2003-01-30
*	Make sure the parser is compiled in native mode.	bertot	2003-01-30
*	Ajoute les directives pour créer aussi bin/coq-interface.opt	bertot	2003-01-30
*	Auto with zarith essaye Abstract Omega sur un but False	filliatr	2003-01-30
*	changement de place du Initial State (maintenant apres l'analyse de la ligne ...	filliatr	2003-01-30
*	pas de Xml.vo	filliatr	2003-01-30
*	fignolage	letouzey	2003-01-30
*	pb d'hier resolu. Recommit	letouzey	2003-01-30
*	apres le backtrack precedent, remise de trois points precis et surs	letouzey	2003-01-29
*	Ca a tout pété -> Bactrack a la version d'hier	letouzey	2003-01-29
*	affichage module et module type	letouzey	2003-01-29
*	affichage module et module type	letouzey	2003-01-29
*	affichage module et module type	letouzey	2003-01-29
*	workaround en attendant traitement reel des modules types	letouzey	2003-01-28
*	amelioration du pretty-print des modules	letouzey	2003-01-28
*	nouvelle gestion des constantes de type	letouzey	2003-01-28
*	MAJ pour Reg	desmettr	2003-01-28
*	Deux p\'tits trucs ;)	coq	2003-01-27
*	all tactics should be covered now: remains	bertot	2003-01-26
*	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