From f25c301c985ac5cbabef0a8392cc82ca212bacc9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 12 May 2015 04:46:34 -0700
Subject: [PATCH] fix(library/data/rat): migrate for rat

---
 library/data/rat/basic.lean | 8 +++++---
 library/data/rat/order.lean | 4 +++-
 2 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean
index c8f27f066..2e6dfe3d8 100644
--- a/library/data/rat/basic.lean
+++ b/library/data/rat/basic.lean
@@ -392,8 +392,10 @@ section
     inv_zero         := inv_zero,
     has_decidable_eq := has_decidable_eq⦄
 
-  migrate from algebra with rat
-    replacing sub → rat.sub
-end
+  definition divide (a b : rat) := algebra.divide a b
+  definition dvd (a b : rat) := algebra.dvd a b
 
+  migrate from algebra with rat
+    replacing sub → rat.sub, divide → divide, dvd → dvd
+end
 end rat
diff --git a/library/data/rat/order.lean b/library/data/rat/order.lean
index 54c717d67..f4399d3df 100644
--- a/library/data/rat/order.lean
+++ b/library/data/rat/order.lean
@@ -222,6 +222,8 @@ section
 
   definition abs (n : rat) : rat := algebra.abs n
   definition sign (n : rat) : rat := algebra.sign n
-  migrate from algebra with rat replacing abs → abs, sign → sign
+
+  migrate from algebra with rat
+  replacing has_le.ge → ge, has_lt.gt → gt, sub → sub, abs → abs, sign → sign, dvd → dvd, divide → divide
 end
 end rat