coq - The formal proof system

Age	Commit message (Expand)	Author
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
2002-02-28	Generalisation de l'utilisation de l'unification d'ordre 2	barras
2002-02-28	Ajout andb_true_eq pour PolyList.list_beq	herbelin
2002-02-27	modifs des preambules d'extraction modulaire	letouzey
2002-02-27	-dump-glob dans le usage	filliatr
2002-02-25	pretty print des Cases devenant des let-in	letouzey
2002-02-22	Doc + ajout fold_symmetric et nth_In	herbelin
2002-02-22	Doc	herbelin
2002-02-22	suppression de pop_named	barras
2002-02-21	code mort dans tactinterp; plus de Debug On/Off dans Correctness	filliatr
2002-02-20	Changé le nom du module Errors (errors.mli, errors.ml) en Cerrors parce	ddr