aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2002-05-14petite erreur de syntaxebarras
2002-05-14ajout des theoremes eqT_rec_r et eqT_rect_r pour Rewritebarras
2002-05-14encore des lemmes sur Zdivfilliatr
2002-05-14nouveaux lemmes dans Zdiv (Claude Marche)filliatr
2002-05-07lemmes plus_O_n et plus_Sn_m (pour Yves)filliatr
2002-05-07lemmes plus_O_n et plus_Sn_m (pour Yves)filliatr
2002-05-06Cosmétiqueherbelin
2002-05-06Standardisationherbelin
2002-04-19lemmes sur Zdiv/Zmodfilliatr
2002-04-19un thm de plus dans Zdiv; un retour chariot apres un message de la tactique F...filliatr
2002-04-17*** empty log message ***werner
2002-04-17Quelques bugs avec inject_natherbelin
2002-04-17Uniformisation (Qed/Save et Implicits Arguments)herbelin
2002-04-08Zdiv -> Export ZArithfilliatr
2002-04-08syntaxe pour Zdiv et Zmodfilliatr
2002-04-05simplification preuvefilliatr
2002-04-05nouveau module Zdivfilliatr
2002-04-02Optimisationdesmettr
2002-04-02Suppression PI_lb et PI_ubdesmettr
2002-04-02Suppression Fielddesmettr
2002-03-29sans utiliser Fielddesmettr
2002-03-29Suppression des invocations a Fielddesmettr
2002-03-26Prise en compte des dependances dans la tactique Casemohring
2002-03-22*** empty log message ***werner
2002-03-22Bug d'affichage des réels dû à une collision entre les APPLINSIDETAIL de Z...herbelin
2002-03-21Intuition ne fait plus de Unfold des constantes (il faut les fairecourant
2002-03-20Intuition now takes an (optional) tactic as parameter. This tactic iscourant
2002-03-19Exportation de SplitRmult et SplitAbsoludelahaye
2002-03-17Field ne fait maintenant que les reductions necessairesdelahaye
2002-03-13Ajout de lemmesmohring
2002-03-07*** empty log message ***desmettr
2002-03-05petits changements afin de profiter du nouveau Rewrite/inbarras
2002-03-04Nouveau Rewrite-in plus economiquebarras
2002-02-28Ajout andb_true_eq pour PolyList.list_beqherbelin
2002-02-22Doc + ajout fold_symmetric et nth_Inherbelin
2002-02-22Docherbelin
2002-02-21code mort dans tactinterp; plus de Debug On/Off dans Correctnessfilliatr
2002-02-19Uniformisation des theoremes dans Set et Type (def. de Acc_rect etbarras
2002-02-14option -dump-glob pour coqdocfilliatr
2002-02-14Syntaxe IF then else au lieu de either and_then or_elsebarras
2002-01-31changement generation de schema d'elimination, False_rec est primitif, Constr...mohring
2002-01-29modification de la definition des def inductives unitaires et autorisation d'...mohring
2002-01-25Bug affichage de O (de nat) dans une expression sur Zherbelin
2002-01-25Zdiv et Zmod dans Zcomplementsfilliatr
2002-01-18Bug commentaire (*i i*)herbelin
2002-01-18amadouage de coqwebletouzey
2002-01-18ajouts provenant de Chinese dans ZArith + deplacements de 3 fichiers de contr...letouzey
2002-01-10Modifs incongrues dans le précédent commitherbelin
2002-01-09MAJ des Id pour coqwebherbelin
2002-01-07Ajout en-têteherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 08:25:42 +0000