From ae2ce356b41649c222449050c5ea5bbd9b7d46a4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 17 Jul 2014 20:49:53 +0100
Subject: [PATCH] feat(library/hott): use new 'parameters' command

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 library/hott/logic.lean | 18 +++++-------------
 1 file changed, 5 insertions(+), 13 deletions(-)

diff --git a/library/hott/logic.lean b/library/hott/logic.lean
index 6883ab2ad..9a6cf85a3 100644
--- a/library/hott/logic.lean
+++ b/library/hott/logic.lean
@@ -78,14 +78,9 @@ theorem ap_refl {A : Type} {B : Type} (f : A → B) (a : A) : ap f (refl a) = re
 := refl (refl (f a))
 
 section
-  parameter {A : Type}
-  parameter {B : Type}
-  parameter {C : Type}
-  parameter f : A → B
-  parameter g : B → C
-  parameters x y z : A
-  parameter p : x = y
-  parameter q : y = z
+  parameters {A : Type} {B : Type} {C : Type}
+  parameters (f : A → B) (g : B → C)
+  parameters (x y z : A) (p : x = y) (q : y = z)
 
   theorem ap_trans_dist : ap f (p ⬝ q) = (ap f p) ⬝ (ap f q)
   := have e1 : ap f (p ⬝ refl y) = (ap f p) ⬝ (ap f (refl y)), from refl _,
@@ -105,9 +100,7 @@ section
 end
 
 section
-  parameter {A : Type}
-  parameter {B : A → Type}
-  parameter f : Π x, B x
+  parameters {A : Type} {B : A → Type} (f : Π x, B x)
   definition D [private] (x y : A) (p : x = y) := p*(f x) = f y
   definition d [private] (x : A) : D x x (refl x)
   := refl (f x)
@@ -129,8 +122,7 @@ notation `assume` binders `,` r:(scoped f, f) := r
 notation `take`   binders `,` r:(scoped f, f) := r
 
 section
-  parameter {A : Type}
-  parameter {B : Type}
+  parameters {A : Type} {B : Type}
 
   theorem hom_refl (f : A → B) : f ∼ f
   := take x, refl (f x)