coq - The formal proof system

Age	Commit message (Expand)	Author
2004-03-12	maj	filliatr
2004-03-12	maj	filliatr
2004-03-11	Test l'interprétation des scopes	herbelin
2004-03-11	Ajout exemple Inst	herbelin
2004-03-11	Ajout vieil exemple de coq-club	herbelin
2004-03-11	Ajout d'un vieil exemple de N. Magaud	herbelin
2004-03-11	Ooops ! bug in firstorder fixed (let's hope no one noticed)	corbinea
2004-03-11	code obsolete	herbelin
2004-03-11	Suppression de la distinction entre elimination de Type vers Type ou pas (Fal...	herbelin
2004-03-11	Branchement EmptyT, UnitT, IT vers leur equivalent dans Set	herbelin
2004-03-11	Ajout bug #540	herbelin
2004-03-11	reals: renamed type option into field_rel_option	marche
2004-03-11	maj	filliatr
2004-03-11	maj	filliatr
2004-03-10	MAJ	herbelin
2004-03-10	Ajout tactiques stepl et stepr de Nimègue	herbelin
2004-03-10	Correction bug internalisation 'context'	herbelin
2004-03-10	maj	filliatr
2004-03-09	bug de l'inversion (coq-bugs #529)	barras
2004-03-09	option -l de coqc non reconnue (coq-bugs #509)	barras
2004-03-09	bug affichage des cofix	barras
2004-03-09	maj	filliatr
2004-03-08	correction de bugs des points fixes	barras
2004-03-08	maj	filliatr
2004-03-06	the output the parser should produce now	bertot
2004-03-06	changed the test for obj_magic.v to be less sensitive to changes	bertot
2004-03-06	maj	filliatr
2004-03-05	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras
2004-03-05	Retablissement pour le traducteur d'une copie de pr_intro_pattern base sur la...	herbelin
2004-03-05	maj	filliatr
2004-03-05	maj	filliatr
2004-03-04	Reparation ROmega V8/Omega ZERO/POS/NEG	mohring
2004-03-04	ROmega	mohring
2004-03-04	maj	filliatr
2004-03-03	adaptation V8 version Pierre Cregut	mohring
2004-03-03	ide: silent behavior better, save icon, -byte works	marche
2004-03-03	Plus de noms d'entrees de grammaires qualifies dans 'Tactic Notation'	herbelin
2004-03-03	takes better account of the new possibility to pass a parametric count argument	bertot
2004-03-03	removes capital letters in two tactic names.	bertot
2004-03-03	make sure the implicit argument indications are in the right order	bertot
2004-03-03	maj	filliatr
2004-03-03	maj	filliatr
2004-03-02	Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...	herbelin
2004-03-02	Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...	herbelin
2004-03-02	Changement de natural en int_or_var pour 'do' et 'fail' pour paramétrisation...	herbelin
2004-03-02	Simplification preuve	herbelin
2004-03-02	Tactic Notation et with-names	herbelin
2004-03-02	Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...	herbelin
2004-03-02	Correction oubli du cas pas d'arguments implicites du tout	herbelin
2004-03-02	maj	filliatr