From e4f1b5c2b52421c4812d959c7852c214c1af6f0a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 30 Jan 2017 16:34:36 +0100
Subject: [PATCH] A bunch of missing Params instances.

---
 theories/algebra/agree.v |  7 +++----
 theories/algebra/csum.v  | 10 +++++++---
 theories/algebra/excl.v  |  3 +++
 theories/prelude/base.v  |  2 ++
 4 files changed, 15 insertions(+), 7 deletions(-)

diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 6dbb677f2..3a38ffa34 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -193,7 +193,7 @@ Section list_theory.
     Context `(R' : relation B) (f : A → B) {Hf: Proper (R ==> R') f}.
     Collection Hyps := Type Hf.
     Local Set Default Proof Using "Hyps".
-    
+
     Global Instance list_setincl_fmap :
       Proper (list_setincl R ==> list_setincl R') (fmap f).
     Proof using Hf.
@@ -201,7 +201,7 @@ Section list_theory.
       destruct (Hab _ Ha) as (b & Hb & HR). exists (f b).
       split; first eapply elem_of_list_fmap; eauto.
     Qed.
-    
+
     Global Instance list_setequiv_fmap :
       Proper (list_setequiv R ==> list_setequiv R') (fmap f).
     Proof using Hf. intros ?? [??]. split; apply list_setincl_fmap; done. Qed.
@@ -213,9 +213,7 @@ Section list_theory.
       intros (a & -> & Ha)%elem_of_list_fmap (b & -> & Hb)%elem_of_list_fmap.
       apply Hf. exact: Hl.
     Qed.
-      
   End fmap.
-
 End list_theory.
 
 Section agree.
@@ -408,6 +406,7 @@ Lemma agree_validI {M} x y : ✓ (x ⋅ y) ⊢ (x ≡ y : uPred M).
 Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_invN. Qed.
 End agree.
 
+Instance: Params (@to_agree) 1.
 Arguments agreeC : clear implicits.
 Arguments agreeR : clear implicits.
 
diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index a2a508433..4fb69bd32 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -10,13 +10,17 @@ Local Arguments cmra_validN _ _ !_ /.
 Local Arguments cmra_valid _  !_ /.
 
 Inductive csum (A B : Type) :=
-| Cinl : A → csum A B
-| Cinr : B → csum A B
-| CsumBot : csum A B.
+  | Cinl : A → csum A B
+  | Cinr : B → csum A B
+  | CsumBot : csum A B.
 Arguments Cinl {_ _} _.
 Arguments Cinr {_ _} _.
 Arguments CsumBot {_ _}.
 
+Instance: Params (@Cinl) 2.
+Instance: Params (@Cinr) 2.
+Instance: Params (@CsumBot) 2.
+
 Instance maybe_Cinl {A B} : Maybe (@Cinl A B) := λ x,
   match x with Cinl a => Some a | _ => None end.
 Instance maybe_Cinr {A B} : Maybe (@Cinr A B) := λ x,
diff --git a/theories/algebra/excl.v b/theories/algebra/excl.v
index ca8757a07..70b6e3a44 100644
--- a/theories/algebra/excl.v
+++ b/theories/algebra/excl.v
@@ -10,6 +10,9 @@ Inductive excl (A : Type) :=
 Arguments Excl {_} _.
 Arguments ExclBot {_}.
 
+Instance: Params (@Excl) 1.
+Instance: Params (@ExclBot) 1.
+
 Notation excl' A := (option (excl A)).
 Notation Excl' x := (Some (Excl x)).
 Notation ExclBot' := (Some ExclBot).
diff --git a/theories/prelude/base.v b/theories/prelude/base.v
index ccd304237..65233ddfe 100644
--- a/theories/prelude/base.v
+++ b/theories/prelude/base.v
@@ -422,6 +422,8 @@ 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.
+Instance: Params (@fst) 2.
+Instance: Params (@snd) 2.
 
 Notation curry := prod_curry.
 Notation uncurry := prod_uncurry.
-- 
GitLab