coq - The formal proof system

Age	Commit message (Expand)	Author
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
2002-02-11	substitution et pattern modulo let	barras
2002-02-11	bad printing of Zeta reduction flags (was missing)	barras
2002-02-08	mauvais comportement de l'inversion vis-a-vis des lets	barras
2002-02-08	prterm -> prterm_env	filliatr
2002-02-08	affichages avec prterm_env et non prterm; deb_print pour vraiment ne rien fai...	filliatr
2002-02-07	erreur mineure dans le test des inductifs imbriques	barras
2002-02-07	petit nettoyage de kernel/inductive	barras
2002-02-07	suppression du retour chariot a la fin de print_pure_constr	barras
2002-02-07	un assert false de trop (MLexn peut avoir des args)	letouzey
2002-02-06	oubli	letouzey
2002-02-06	gros changement dans mlutil.ml: ajout d'une elimination globale des prop	letouzey
2002-02-06	affichage des messages d'erreur pour Stack_overflow, Out_of_memory, Break	barras
2002-02-05	evaluable_constant retournait vrai pour les constantes opaques, ce qui faisait	barras
2002-02-05	exclusion des rertoires de test de l'extraction	letouzey
2002-02-05	Ajout d'optimisations locales kill_prop	letouzey
2002-02-04	exceptionmal ratrappee	barras
2002-02-04	maj newsyntax	barras
2002-02-01	Ajout tactiques Rename et Pose; modifications pour Inversion	herbelin
2002-01-31	adaptation de l'extraction aux changements de Christine concernant rec/rect e...	letouzey