From fbe80d48dc88b9072d6622fac6997de76f03a640 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 13 Oct 2015 13:18:21 -0700
Subject: [PATCH] chore(library): remove "set_option pp.*" commands

---
 library/data/int/gcd.lean                  | 3 ---
 library/data/rat/basic.lean                | 1 -
 library/data/rat/order.lean                | 3 ---
 library/data/set/finite.lean               | 1 -
 library/theories/group_theory/finsubg.lean | 3 ---
 library/theories/number_theory/bezout.lean | 2 --
 6 files changed, 13 deletions(-)

diff --git a/library/data/int/gcd.lean b/library/data/int/gcd.lean
index 3c992691db..46237898c4 100644
--- a/library/data/int/gcd.lean
+++ b/library/data/int/gcd.lean
@@ -21,9 +21,6 @@ of_nat_nonneg (nat.gcd (nat_abs a) (nat_abs b))
 theorem gcd.comm (a b : ℤ) : gcd a b = gcd b a :=
 by rewrite [↑gcd, nat.gcd.comm]
 
-set_option pp.all true
-set_option pp.numerals false
-
 theorem gcd_zero_right (a : ℤ) : gcd a 0 = abs a :=
 by rewrite [↑gcd, nat_abs_zero, nat.gcd_zero_right, of_nat_nat_abs]
 
diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean
index ee2ac85360..4c82395060 100644
--- a/library/data/rat/basic.lean
+++ b/library/data/rat/basic.lean
@@ -299,7 +299,6 @@ begin
   intros, apply rfl
 end
 
-set_option pp.full_names true
 theorem reduce_equiv : ∀ a : prerat, reduce a ≡ a
 | (mk an ad adpos) :=
     decidable.by_cases
diff --git a/library/data/rat/order.lean b/library/data/rat/order.lean
index 615d94f62e..f2dbdf133b 100644
--- a/library/data/rat/order.lean
+++ b/library/data/rat/order.lean
@@ -360,9 +360,6 @@ eq_of_sub_eq_zero this
 section
   open int
 
-  set_option pp.numerals false
-  set_option pp.implicit true
-
   theorem num_nonneg_of_nonneg {q : ℚ} (H : q ≥ 0) : num q ≥ 0 :=
   have of_int (num q) ≥ of_int 0,
     begin
diff --git a/library/data/set/finite.lean b/library/data/set/finite.lean
index 00e452a4a4..dbfb8a66c2 100644
--- a/library/data/set/finite.lean
+++ b/library/data/set/finite.lean
@@ -127,7 +127,6 @@ by rewrite [-finset.to_set_upto n]; apply finite_finset
 theorem to_finset_upto (n : ℕ) : to_finset {i | i < n} = finset.upto n :=
 by apply (to_finset_eq_of_to_set_eq !finset.to_set_upto)
 
-set_option pp.notation false
 theorem finite_powerset (s : set A) [fins : finite s] : finite 𝒫 s :=
 assert H : 𝒫 s = finset.to_set '[finset.to_set (#finset 𝒫 (to_finset s))],
   from ext (take t, iff.intro
diff --git a/library/theories/group_theory/finsubg.lean b/library/theories/group_theory/finsubg.lean
index fac4b298ed..67dff70792 100644
--- a/library/theories/group_theory/finsubg.lean
+++ b/library/theories/group_theory/finsubg.lean
@@ -139,9 +139,6 @@ lemma fin_lcoset_subset {S : finset A} (Psub : S ⊆ H) : ∀ x, x ∈ H → fin
 lemma finsubg_lcoset_id {a : A} : a ∈ H → fin_lcoset H a = H :=
 by rewrite [eq_eq_to_set_eq, fin_lcoset_eq, mem_eq_mem_to_set]; apply subgroup_lcoset_id
 
-set_option pp.notation false
-set_option pp.full_names true
-
 lemma finsubg_inv_lcoset_eq_rcoset {a : A} :
   fin_inv (fin_lcoset H a) = fin_rcoset H a⁻¹ :=
 begin
diff --git a/library/theories/number_theory/bezout.lean b/library/theories/number_theory/bezout.lean
index 5b2cff6fb8..7d7f44a334 100644
--- a/library/theories/number_theory/bezout.lean
+++ b/library/theories/number_theory/bezout.lean
@@ -41,8 +41,6 @@ theorem egcd_succ (x y : ℕ) :
   egcd x (succ y) = prod.cases_on (egcd (succ y) (x mod succ y)) (egcd_rec_f (x div succ y)) :=
 well_founded.fix_eq egcd.F (x, succ y)
 
-set_option pp.coercions true
-
 theorem egcd_of_pos (x : ℕ) {y : ℕ} (ypos : y > 0) :
   let erec := egcd y (x mod y), u := pr₁ erec, v := pr₂ erec in
     egcd x y = (v, u - v * (x div y)) :=