aboutsummaryrefslogtreecommitdiff
path: root/theories/ZArith/Zsyntax.v
AgeCommit message (Expand)Author
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...herbelin
2003-11-12Restructuration ZArithherbelin
2003-11-05Restructuration ZArith et déport de la partie sur 'positive' dans NArith, de...herbelin
2003-11-01Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...herbelin
2003-10-22reorganisation des niveaux (ex: = est a 70)barras
2003-10-16Suppression des surcharge de regles de grammaire en v7herbelin
2003-09-30'_ = _ = _' maintenant predefini, meme en V7herbelin
2003-09-19Mise en place des V8Notation et V8Infix pour declarer des notations en v8 mem...herbelin
2003-09-12Bind et Delimit pour positive et Z (hors section)herbelin
2003-07-18Coq.Init.Logic.eq au lieu de eqfilliatr
2003-05-29niveau 49 devient nextherbelin
2003-05-07coqide: toolbar/autosavemonate
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"herbelin
2003-03-28notations <>, Assumption avec existentiel, replace termmohring
2003-03-21*** empty log message ***barras
2003-03-12*** empty log message ***barras
2003-01-22Bug precedenceherbelin
2002-12-28Re-installation nombres dans les motifs sur Zherbelin
2002-12-15Ajout syntaxe '>'herbelin
2002-12-02Z_scope doit annuler l'affichage de = entreherbelin
2002-11-26Correction affichage entiers en cas d'échecherbelin
2002-11-25Rétablissement affichage des entiers de natherbelin
2002-11-24Traitement des parenthèses de nat au niveau du printerherbelin
2002-11-24Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...herbelin
2002-10-23Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pourherbelin
2002-10-22Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;...herbelin
2002-10-13Mise en place d'ensembles de notations symboliques pour nat, Z et Rherbelin
2002-06-06Correction non reconnaissance des variables de section dans les afficheurs de...herbelin
2002-05-29Contournement des My_special_variableherbelin
2002-04-17Quelques bugs avec inject_natherbelin
2002-04-17Uniformisation (Qed/Save et Implicits Arguments)herbelin
2002-03-22Bug d'affichage des réels dû à une collision entre les APPLINSIDETAIL de Z...herbelin
2002-02-14option -dump-glob pour coqdocfilliatr
2002-01-25Bug affichage de O (de nat) dans une expression sur Zherbelin
2001-09-12Rustine pour gérer inject_natherbelin
2001-04-23Minor layout adjustments for Library doccoq
2001-04-20Library doc adjustments (until page 140)coq
2001-04-19remplace Zarith par ZArithmohring
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 05:32:01 +0000