From fb144483e438411f0527897a42104d16bd51a558 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 3 Feb 2016 13:19:42 +0100
Subject: [PATCH] Fix implicit arguments indexed product.
---
modures/cmra.v | 2 +-
modures/cofe.v | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/modures/cmra.v b/modures/cmra.v
index 44d02b431..326f8b490 100644
--- a/modures/cmra.v
+++ b/modures/cmra.v
@@ -572,4 +572,4 @@ Section iprod_cmra.
CMRAT iprod_cofe_mixin iprod_cmra_mixin iprod_cmra_extend_mixin.
End iprod_cmra.
-Arguments iprodRA : clear implicits.
+Arguments iprodRA {_} _.
diff --git a/modures/cofe.v b/modures/cofe.v
index 98fc986a4..bab5b05d0 100644
--- a/modures/cofe.v
+++ b/modures/cofe.v
@@ -399,4 +399,4 @@ Section iprod_cofe.
Canonical Structure iprodC : cofeT := CofeT iprod_cofe_mixin.
End iprod_cofe.
-Arguments iprodC : clear implicits.
+Arguments iprodC {_} _.
--
GitLab