coq - The formal proof system

Age	Commit message (Expand)	Author
2003-01-31	Ajout d'un filtrage d'application partielle	herbelin
2003-01-31	MAJ	herbelin
2003-01-31	MAJ	herbelin
2003-01-31	MAJ	herbelin
2003-01-31	Unification plus efficace vis à vis du LetIn	herbelin
2003-01-31	preparation pkg deb for 7.4	courant
2003-01-31	* 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-30	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-29	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-28	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-27	Deux p\'tits trucs ;)	coq
2003-01-26	all tactics should be covered now: remains	bertot
2003-01-25	Add translations for many tactics but a dozen are still remaining	bertot
2003-01-25	Un type "standardisé" pour new_hyp	herbelin
2003-01-24	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-23	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-22	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