diff options
Diffstat (limited to 'contrib/ring/Setoid_ring.v')
| -rw-r--r-- | contrib/ring/Setoid_ring.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/contrib/ring/Setoid_ring.v b/contrib/ring/Setoid_ring.v index b5cd6b1d0c..93b9bc7cf5 100644 --- a/contrib/ring/Setoid_ring.v +++ b/contrib/ring/Setoid_ring.v @@ -10,4 +10,5 @@ Require Export Setoid_ring_theory. Require Export Quote. -Require Export Setoid_ring_normalize.
\ No newline at end of file +Require Export Setoid_ring_normalize. +Declare ML Module "ring_plugin". |