coq - The formal proof system

Age	Commit message (Expand)	Author
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
2002-01-31	changement generation de schema d'elimination, False_rec est primitif, Constr...	mohring
2002-01-31	extraction des CoInductives via les Lazy d'ocaml	letouzey
2002-01-30	cosmetique	herbelin
2002-01-30	ajout list_split3, pr_semicolon et pr_bar	herbelin
2002-01-30	Reparation erreur de syntaxe	mohring
2002-01-29	modification de la definition des def inductives unitaires et autorisation d'...	mohring
2002-01-29	condition de positivite moins stricte vis-a-vis des parametres (cf bug de Edu...	barras
2002-01-25	Test affichage O de nat dans une expression sur Z	herbelin
2002-01-25	Bug affichage de O (de nat) dans une expression sur Z	herbelin
2002-01-25	* empty log message *	herbelin
2002-01-25	Zdiv et Zmod dans Zcomplements	filliatr
2002-01-25	patch Omega (bug 129)	filliatr
2002-01-25	Correction bug 'Check [b]if b then O else O'	herbelin
2002-01-25	Remplacement cut_intro par true_cut_anon pour Inversion	herbelin
2002-01-25	Bug calcul de la signature incorrecte en présence de letin	herbelin