diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-11 20:42:52 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-11 20:42:52 +0000 |
| commit | b6c6e36afa8da16a62bf16191baa2531894c54fc (patch) | |
| tree | f60acb5c55ea378b50defc7cdd22b51da05d8a87 /theories/ZArith/BinInt.v | |
| parent | ae3a6c63018d5743c16ab388d3e1f9bfde0eb43d (diff) | |
- Changement du code de Zplus pour accomoder ring qui sinon prend une
complexité exponentielle dans la machine lazy depuis que l'algo de
compilation du filtrage évite systématiquement d'expanser quand le
filtrage n'est pas dépendant.
- Un peu plus de colorisation dans coqide.
- Utilisation de formats pour améliorer de l'affichage des notations Utf8.
- Systématisation paire Local/Global dans g_vernac.ml4 (même si le
défaut n'est pas toujours le même)
- Bug Makefile
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10918 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/BinInt.v')
| -rw-r--r-- | theories/ZArith/BinInt.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 46faafb23..610afd4d7 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -80,7 +80,8 @@ Close Local Scope positive_scope. Definition Zplus (x y:Z) := match x, y with | Z0, y => y - | x, Z0 => x + | Zpos x', Z0 => Zpos x' + | Zneg x', Z0 => Zneg x' | Zpos x', Zpos y' => Zpos (x' + y') | Zpos x', Zneg y' => match (x' ?= y')%positive Eq with |