diff options
Diffstat (limited to 'contrib/ring/LegacyRing.v')
| -rw-r--r-- | contrib/ring/LegacyRing.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/contrib/ring/LegacyRing.v b/contrib/ring/LegacyRing.v index ed1da9c56e..4ae85baf37 100644 --- a/contrib/ring/LegacyRing.v +++ b/contrib/ring/LegacyRing.v @@ -13,6 +13,7 @@ Require Export LegacyRing_theory. Require Export Quote. Require Export Ring_normalize. Require Export Ring_abstract. +Declare ML Module "ring_plugin". (* As an example, we provide an instantation for bool. *) (* Other instatiations are given in ArithRing and ZArithRing in the |