diff options
| author | letouzey | 2006-04-25 22:52:18 +0000 |
|---|---|---|
| committer | letouzey | 2006-04-25 22:52:18 +0000 |
| commit | b2e0ec34cdd95017ce9ecec99b3431494b452d6c (patch) | |
| tree | ccbc1c35da20152063cc5d094cc2e1b256fa4cf0 /theories/IntMap/Mapc.v | |
| parent | 0274e797162cd62fe9145436a66027a61d727d64 (diff) | |
Un gros coup de lifting pour IntMap:
* le type ad des adresses est maintenant un alias vers
le N de NArith, qui lui est isomorphe.
* toutes les operations sur ces adresses (p.ex. un xor
bit a bit) sont maintenant dans de nouveaux fichiers du
repertoire NArith.
* Intmap utilise maintenant le meme type option que le
reste du monde
* etc etc...
Tout ceci ne preserve pas forcement la compatibilite. Les 4 contribs
utilisant Intmap sont adaptees en consequence. Me demander si besoin
ma moulinette d'adaptation (incomplete).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8733 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/IntMap/Mapc.v')
| -rw-r--r-- | theories/IntMap/Mapc.v | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/theories/IntMap/Mapc.v b/theories/IntMap/Mapc.v index 739339f9e3..d6a9aad477 100644 --- a/theories/IntMap/Mapc.v +++ b/theories/IntMap/Mapc.v @@ -10,10 +10,7 @@ Require Import Bool. Require Import Sumbool. Require Import Arith. -Require Import ZArith. -Require Import Addr. -Require Import Adist. -Require Import Addec. +Require Import NArith. Require Import Map. Require Import Mapaxioms. Require Import Fset. |