coq - The formal proof system

Age	Commit message (Expand)	Author
2002-03-19	bug optimize_fix fait trop tot	letouzey
2002-03-19	suite bug Dglob constant	letouzey
2002-03-19	bug avec les MLglob vraiment constants	letouzey
2002-03-19	travail sur les stratégies de réduction	letouzey
2002-03-19	remplacement des deux constants prop/arity par une seule dummy + pretty-print...	letouzey
2002-03-19	Ajout de l'entrée ne_constrarg_list	delahaye
2002-03-19	Fix d'un bug sur le test des inverses	delahaye
2002-03-19	Exportation de SplitRmult et SplitAbsolu	delahaye
2002-03-18	Rétablissement de look_for_interp	delahaye
2002-03-17	Field ne fait maintenant que les reductions necessaires	delahaye
2002-03-17	Meilleure gestion de la reduction dans Field	delahaye
2002-03-15	epsilon	letouzey
2002-03-15	changements récents dans l'extraction	letouzey
2002-03-15	un peu de mise a jour de la doc extraction	letouzey
2002-03-15	evite les clash avec le type ocaml unit	letouzey
2002-03-15	Tauto est maintenant stable par "Intro" :	courant
2002-03-15	gros commit: principalement ajout des lambdas arity + leur optimisation en te...	letouzey
2002-03-14	reparation semi setoid ring	clrenard
2002-03-13	Ajout de lemmes	mohring
2002-03-13	cleanconfig efface ocamldebug-v7	filliatr
2002-03-13	* empty log message *	mohring
2002-03-12	Retablissement de interp_tab + injection id -> constr sans goal	delahaye
2002-03-12	Propagation du pb de conversion dans clenv_unify	herbelin
2002-03-12	* empty log message *	courant
2002-03-12	open Univ inutile	courant
2002-03-12	Makefile	courant
2002-03-11	Factorisation de la grammaire pour Extraction Language.	letouzey
2002-03-08	renommage de fonctions	barras
2002-03-07	* empty log message *	desmettr
2002-03-07	raccourci -l en plus de -load-vernac-source	letouzey
2002-03-07	Simplify_eq echouait sur des hypotheses trivial comme O=O	barras
2002-03-07	Clear ne substitue plus le corps dans le reste du but	barras
2002-03-05	* empty log message *	barras
2002-03-05	ajout d'une entree 'binaries' pour recompiler coq mais pas les theories	barras
2002-03-05	cas des constructeurs singletons. Messages d'erreur. Revision de test_extract...	letouzey
2002-03-05	assert failure avec Conditional Rewrite	barras
2002-03-05	petits changements afin de profiter du nouveau Rewrite/in	barras
2002-03-05	unification faite de gauche a droite (et non pas l'inverse) pour eviter que	barras
2002-03-05	suppression de code mort	barras
2002-03-04	* empty log message *	barras
2002-03-04	Big commit extraction:	letouzey
2002-03-04	Nouveau Rewrite-in plus economique	barras
2002-03-01	Nouveau comportement: Delta ne s'applique pas aux variables liées par un let	herbelin
2002-03-01	Prise en compte des corps de letin dans les hypothèses	herbelin
2002-03-01	labels appliques dans un ordre incorrect	barras
2002-03-01	convert_hyp a change de type	barras
2002-02-28	Uniformisation convert_hyp	herbelin
2002-02-28	Uniformisation convert_hyp; correction problème de dépendance dans letin_tac	herbelin
2002-02-28	* empty log message *	herbelin
2002-02-28	ajout option_compare	herbelin