diff options
| -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] |