coq - The formal proof system

Age	Commit message (Expand)	Author
2001-04-02	parenthèses autour des types dans les arguments des constructeurs	filliatr
2001-04-02	underscores pour les variables représentant des propositions	filliatr
2001-04-02	inductifs vides	filliatr
2001-04-02	ml_pop au lieu de ml_lift dans betared_ast	filliatr
2001-04-02	à faire	filliatr
2001-04-02	bug Fix signalé par Alexandre (even/odd mal interprété)	filliatr
2001-03-30	branchement extraction (bytecode seulement)	filliatr
2001-03-30	Ajout de lemmes sur les booleens	mohring
2001-03-30	Introduction d'une preuve de False_rec	mohring
2001-03-30	extraction modulaire	filliatr
2001-03-30	extraction modulaire + environnement des Fix corrigé	filliatr
2001-03-30	repertoire pour les tests d'extraction	filliatr
2001-03-30	application avec bcp args	letouzey
2001-03-30	beta-reduction	filliatr
2001-03-29	mise en place de Correctness (ne compile pas encore)	filliatr
2001-03-29	deux fois $Id$	filliatr
2001-03-29	fichiers extraction	filliatr
2001-03-28	changement type_var et signature	filliatr
2001-03-28	amelioration de la structure des univers	barras
2001-03-27	Interprétation des qualidarg	herbelin
2001-03-27	conservation des arguments dans Prop (snif)	filliatr
2001-03-27	mise a jour	filliatr
2001-03-27	extraction recursive d'un morceau d'environnement	filliatr
2001-03-27	trace des inductifs sur Prop	letouzey
2001-03-26	Bibliotheque Num	mohring
2001-03-26	cache pour les constantes	filliatr
2001-03-25	ocaml 3.01 requis	herbelin
2001-03-25	Tag pour une beta3-ocaml3.01	herbelin
2001-03-23	MAJ	herbelin
2001-03-23	MAJ	herbelin
2001-03-23	Les règles d'affichage ajoutés dans le commit précédent avait le même no...	herbelin
2001-03-23	amelioration de la consommation memoire de la conversion en eta-expansant	barras
2001-03-23	mise a jour	filliatr
2001-03-23	eta-expansion des constructeurs si necessaire (a posteriori en miniML)	filliatr
2001-03-23	La strategie de recherche de lookup_eliminator etait insuffisante	herbelin
2001-03-23	suppression des param dans inductifs. suite du Cases	letouzey
2001-03-22	Règle de syntaxe pour CASTEDCOMMAND	herbelin
2001-03-22	Problèmes de NewInduction	herbelin
2001-03-22	Bug MUTCASE au lieu CASE	herbelin
2001-03-21	Reecriture du extract_type pour Prod et Lambda. Eta-expansion dans les branch...	letouzey
2001-03-21	option -verbose a coqc; option -i supprimée	filliatr
2001-03-20	affichage declarations fix + bug extraction sumbool_rec mis a jour	filliatr
2001-03-20	mlutil	filliatr
2001-03-20	extraction naive de fix et case	filliatr
2001-03-20	Extract_term_with_type. mise a jour & verification des commentaires	letouzey
2001-03-15	entetes	filliatr
2001-03-15	les options passées sont prioritaires sur les -I par défaut	filliatr
2001-03-14	MAJ	herbelin
2001-03-14	Alias suite + bugs divers et variés	herbelin
2001-03-14	Prise en compte des Let dans l'instance des evars	herbelin