diff options
| author | barras | 2006-10-29 21:53:30 +0000 |
|---|---|---|
| committer | barras | 2006-10-29 21:53:30 +0000 |
| commit | 7cae78ffc70a9097beb6d0f1a0e9f741f483e591 (patch) | |
| tree | 3908b81ac623f7910578365a4fe4b18b607de3d5 /contrib/setoid_ring | |
| parent | dfe97724fb6034fc06b3ef693f6a3ed94733adbc (diff) | |
Exports manquants dans ring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9315 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/setoid_ring')
| -rw-r--r-- | contrib/setoid_ring/ArithRing.v | 4 | ||||
| -rw-r--r-- | contrib/setoid_ring/NArithRing.v | 3 | ||||
| -rw-r--r-- | contrib/setoid_ring/ZArithRing.v | 1 |
3 files changed, 3 insertions, 5 deletions
diff --git a/contrib/setoid_ring/ArithRing.v b/contrib/setoid_ring/ArithRing.v index ac65f826e2..5060bc69b8 100644 --- a/contrib/setoid_ring/ArithRing.v +++ b/contrib/setoid_ring/ArithRing.v @@ -7,10 +7,8 @@ (************************************************************************) Require Import Mult. -Require Import Ring_base. +Require Export Ring. Set Implicit Arguments. -Require Import InitialRing. -Export Ring_tac. Ltac isnatcst t := let t := eval hnf in t in diff --git a/contrib/setoid_ring/NArithRing.v b/contrib/setoid_ring/NArithRing.v index 92c23e4a58..33e3cb4ec7 100644 --- a/contrib/setoid_ring/NArithRing.v +++ b/contrib/setoid_ring/NArithRing.v @@ -6,8 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +Require Export Ring. Require Import BinPos BinNat. -Require Import Ring_base InitialRing. +Import InitialRing. Set Implicit Arguments. diff --git a/contrib/setoid_ring/ZArithRing.v b/contrib/setoid_ring/ZArithRing.v index 5220c3a9c6..4f47fff05b 100644 --- a/contrib/setoid_ring/ZArithRing.v +++ b/contrib/setoid_ring/ZArithRing.v @@ -9,7 +9,6 @@ Require Export Ring. Require Import ZArith_base. Import InitialRing. -Export Ring_tac. Set Implicit Arguments. |