diff --git a/modures/cmra.v b/modures/cmra.v index 44d02b4313445dece25da12ad8f822913ba06e66..326f8b490bc583e9af63d475cecb46dc3ca7919b 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 98fc986a47bf2434128d004928c617440e70b6b9..bab5b05d0f1387e3db3e6097895db3f063bd9ac7 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 {_} _.