diff options
Diffstat (limited to 'contrib/ring/Setoid_ring.v')
| -rw-r--r-- | contrib/ring/Setoid_ring.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/ring/Setoid_ring.v b/contrib/ring/Setoid_ring.v index 567517e984..6c33032a27 100644 --- a/contrib/ring/Setoid_ring.v +++ b/contrib/ring/Setoid_ring.v @@ -10,4 +10,4 @@ Require Export Setoid_ring_theory. Require Export Quote. -Require Export Setoid_ring_normalize. +Require Export Setoid_ring_normalize.
\ No newline at end of file |