Make discrete_cmra_discrete global.

f82111d2 · Robbert Krebbers · cbad1f38 · f82111d2
Commit f82111d2 authored Feb 26, 2016 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 1 deletion

algebra/cmra.v algebra/cmra.v +1 -1

No files found.
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -516,7 +516,7 @@ Section discrete.
      apply (timeless _), dist_le with n; auto with lia.
  Qed.
  Definition discreteRA : cmraT := CMRAT (cofe_mixin A) discrete_cmra_mixin.
-  Instance discrete_cmra_discrete : CMRADiscrete discreteRA.
+  Global Instance discrete_cmra_discrete : CMRADiscrete discreteRA.
  Proof. split. change (Discrete A); apply _. by intros x ?. Qed.
 End discrete.