From 7a07028003f0fc76b6a0c0b5559a5866f032ef67 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 8 Feb 2016 23:20:50 +0100
Subject: [PATCH] Params instances for iprod.

---
 algebra/iprod.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/algebra/iprod.v b/algebra/iprod.v
index 10d145a03..211f92f3d 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -4,7 +4,7 @@ Require Import algebra.functor.
 (** * Indexed product *)
 (** Need to put this in a definition to make canonical structures to work. *)
 Definition iprod {A} (B : A → cofeT) := ∀ x, B x.
-Definition iprod_insert `{∀ x x' : A, Decision (x = x')} {B : A → cofeT}
+Definition iprod_insert {A} {B : A → cofeT} `{∀ x x' : A, Decision (x = x')}
     (x : A) (y : B x) (f : iprod B) : iprod B := λ x',
   match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
 Global Instance iprod_empty {A} {B : A → cofeT}
@@ -12,6 +12,8 @@ Global Instance iprod_empty {A} {B : A → cofeT}
 Definition iprod_singleton {A} {B : A → cofeT} 
     `{∀ x x' : A, Decision (x = x'), ∀ x : A, Empty (B x)}
   (x : A) (y : B x) : iprod B := iprod_insert x y ∅.
+Instance: Params (@iprod_insert) 4.
+Instance: Params (@iprod_singleton) 5.
 
 Section iprod_cofe.
   Context {A} {B : A → cofeT}.
-- 
GitLab