coq - The formal proof system

Age	Commit message (Expand)	Author
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
2004-03-02	maj	filliatr
2004-03-01	ne pas échouer si but inchangé pour préserver la compatibilité de 'replace'	herbelin
2004-03-01	code mort	herbelin
2004-03-01	Correction sur commit précédent : Tactics.cut réduisait de manière inappr...	herbelin
2004-03-01	Ajout 'replace in'	herbelin
2004-03-01	Ajout IntroPattern comme type d'argument générique	herbelin
2004-03-01	Déplacement définition intro_pattern_expr dans Genarg	herbelin
2004-03-01	Généralisation du type ltac Identifier en IntroPattern; prise en compte des...	herbelin
2004-03-01	Déplacement définition intro_pattern_expr dans Genarg	herbelin
2004-03-01	Protection d'un 'clear' qui peut etre dependant	herbelin
2004-03-01	ocaml 3.07 -> 3.06	filliatr
2004-03-01	maj	filliatr