aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-05-29Introduction de syntaxe convivial +,*,<=,<,>=herbelin
2002-05-29Double Induction prend maintenant des noms d'hyppthèsesherbelin
2002-05-29Utilisation d'Infix/Distfix autant que possibleherbelin
2002-05-29Contournement des My_special_variableherbelin
2002-05-29Ajout Hurkens.v, ProofIrrelevances.v et l'indiscernabilite dans Classical_Prop.vherbelin
2002-05-16Ajout Peano_dec et Compare_decherbelin
2002-05-16suppression de inf_decidable dans ZArith_dec (pour SeachPattern)filliatr
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-24 05:34:43 +0000