diff options
| author | herbelin | 2003-11-05 14:04:40 +0000 |
|---|---|---|
| committer | herbelin | 2003-11-05 14:04:40 +0000 |
| commit | 1bb1ccb03f366c84c9562d7862ce28dbae709fce (patch) | |
| tree | 3f3f9541bc9740e698a4d2ef7f0493538a048b2d | |
| parent | bc07591c189e80d4010910d99547298bf11de264 (diff) | |
Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positifs et naturels
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4810 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/ring/NArithRing.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/contrib/ring/NArithRing.v b/contrib/ring/NArithRing.v index 27fd0f9938..63483e5b1c 100644 --- a/contrib/ring/NArithRing.v +++ b/contrib/ring/NArithRing.v @@ -10,8 +10,9 @@ (* Instantiation of the Ring tactic for the binary natural numbers *) -Require Export ArithRing. +Require Export Ring. Require Export ZArith_base. +Require NArith. Require Eqdep_dec. Definition Neq := [n,m:entier] |