From ac1e918f83beaa704405473ceace761b713a5816 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 30 May 2016 12:28:21 +0200
Subject: [PATCH] More prelude/base rearrangement.

---
 prelude/base.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/prelude/base.v b/prelude/base.v
index ff635a1a3..22752705f 100644
--- a/prelude/base.v
+++ b/prelude/base.v
@@ -316,7 +316,6 @@ Arguments compose _ _ _ _ _ _ /.
 Arguments flip _ _ _ _ _ _ /.
 Arguments const _ _ _ _ /.
 Typeclasses Transparent id compose flip const.
-Instance: Params (@pair) 2.
 
 Definition fun_map {A A' B B'} (f: A' → A) (g: B → B') (h : A → B) : A' → B' :=
   g ∘ h ∘ f.
@@ -402,6 +401,8 @@ Notation "(, y )" := (λ x, (x,y)) (only parsing) : C_scope.
 Notation "p .1" := (fst p) (at level 10, format "p .1").
 Notation "p .2" := (snd p) (at level 10, format "p .2").
 
+Instance: Params (@pair) 2.
+
 Notation curry := prod_curry.
 Notation uncurry := prod_uncurry.
 Definition curry3 {A B C D} (f : A → B → C → D) (p : A * B * C) : D :=
-- 
GitLab