diff options
Diffstat (limited to 'contrib/ring/Ring_abstract.v')
| -rw-r--r-- | contrib/ring/Ring_abstract.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v index 574c24421..28de54e65 100644 --- a/contrib/ring/Ring_abstract.v +++ b/contrib/ring/Ring_abstract.v @@ -8,7 +8,7 @@ (* $Id$ *) -Require Import Ring_theory. +Require Import LegacyRing_theory. Require Import Quote. Require Import Ring_normalize. |