aboutsummaryrefslogtreecommitdiff
path: root/theories/ZArith/Zsyntax.v
AgeCommit message (Collapse)Author
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ↵herbelin
par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Restructuration ZArithherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4879 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-05Restructuration ZArith et déport de la partie sur 'positive' dans NArith, ↵herbelin
de la partie Omega dans contrib/omega git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4801 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les ↵herbelin
entiers positifs soient parentheses en tant qu'arguments de fonction; tant pis, il faudra ecrire '-(-x)' au lieu de '--x' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4751 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22reorganisation des niveaux (ex: = est a 70)barras
Hint Destruct: syntaxe similaire aux autres hints... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4696 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16Suppression des surcharge de regles de grammaire en v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4650 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-30'_ = _ = _' maintenant predefini, meme en V7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4507 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-19Mise en place des V8Notation et V8Infix pour declarer des notations en v8 ↵herbelin
meme si incompatible avec la syntaxe v7 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4417 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Bind et Delimit pour positive et Z (hors section)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4368 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-07-18Coq.Init.Logic.eq au lieu de eqfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4239 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-29niveau 49 devient nextherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4089 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-07coqide: toolbar/autosavemonate
Hugo: Suppression du type dans les notations == et <> entre git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3992 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3881 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-28notations <>, Assumption avec existentiel, replace termmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3802 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-21*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3783 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22Bug precedenceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3572 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-28Re-installation nombres dans les motifs sur Zherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3483 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-15Ajout syntaxe '>'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3437 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-02Z_scope doit annuler l'affichage de = entreherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3349 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Correction affichage entiers en cas d'échecherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3291 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-25Rétablissement affichage des entiers de natherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3279 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-24Traitement des parenthèses de nat au niveau du printerherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3273 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-24Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; ↵herbelin
améliorations diverses de l'affichage; affinement de la syntaxe et des options de Notation; branchement de Syntactic Definition sur Notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3270 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-23Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pourherbelin
compatibilité avec la surcharge dans certains développements (p.e. Utrecht/ABP) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3176 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-22Redéplacement de + (sum) et * (prod) au niveau de + et * de ↵herbelin
l'arithmétique; ajout d'une option 'level' pour Notation; utilisation de Notation pour sumor et sumbool git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3173 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-13Mise en place d'ensembles de notations symboliques pour nat, Z et Rherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3125 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-06Correction non reconnaissance des variables de section dans les afficheurs ↵herbelin
de Z et R git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2760 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Contournement des My_special_variableherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2727 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-17Quelques bugs avec inject_natherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2653 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-17Uniformisation (Qed/Save et Implicits Arguments)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2650 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-22Bug d'affichage des réels dû à une collision entre les APPLINSIDETAIL de ↵herbelin
Zsyntax et de Rsyntax (dont les règles ne s'appliquent plus dans le même ordre depuis la modification de l'ordre de chargement des Require) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2564 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14option -dump-glob pour coqdocfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-25Bug affichage de O (de nat) dans une expression sur Zherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2439 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-12Rustine pour gérer inject_natherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1954 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23Minor layout adjustments for Library doccoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1672 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20Library doc adjustments (until page 140)coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1655 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19remplace Zarith par ZArithmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1623 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 21:19:37 +0000