coq - The formal proof system

Age	Commit message (Expand)	Author
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
2002-02-19	typage du produit: type_judgment appele avec contexte incorrect	barras
2002-02-19	meilleur message d'erreur lorsqu'on type une evar qui n'existe pas	barras
2002-02-19	Le type des evars transformees en meta n'etait pas normalise, et des Evars	barras
2002-02-19	Uniformisation des theoremes dans Set et Type (def. de Acc_rect et	barras
2002-02-19	Elim dependente n'appelait pas la bonne fonction pour calculer le predicat	barras
2002-02-18	bug #134: on appelait solve_simple_eqn avec une evar qui etait resolue	barras
2002-02-18	but de CutRewrite <- (assert false)	barras
2002-02-15	petits changements cosmetiques sur les tactiques	barras
2002-02-15	suite et fin (?) de haskell: gestion des modules, mise en place du'un test	letouzey
2002-02-15	bootstrap consistent avec les options de la ligne de commande	filliatr
2002-02-15	debut de gestion des open pour extraction modulaire	letouzey
2002-02-14	qq inline manuels (sigS_rec ...) + utilisation de library_part	letouzey
2002-02-14	- Reforme de la gestion des args recursifs (via arbres reguliers)	barras
2002-02-14	option -dump-glob pour coqdoc	filliatr
2002-02-14	Syntaxe IF then else au lieu de either and_then or_else	barras
2002-02-12	Raffinement library_part	herbelin
2002-02-12	petite modif pour ne pas expanser trop de let pendant l'unification	barras
2002-02-12	suppression de la condition de la permutation case/fun	letouzey
2002-02-12	pretty print	letouzey
2002-02-12	Test & correction de la production de code Haskell	letouzey
2002-02-12	Ajout library_part	herbelin