From fd6905fa8a9d9be610a53c4b66360d4c489915de Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 25 Jun 2020 15:09:21 +0200
Subject: [PATCH] Export `Countable` in `gmultiset`, without that, the file is
 useless.

---
 theories/gmultiset.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 6940ba8e..afa505bc 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -1,3 +1,4 @@
+From stdpp Require Export countable.
 From stdpp Require Import gmap.
 Set Default Proof Using "Type".
 
-- 
GitLab