Skip to content
Snippets Groups Projects
Commit fd6905fa authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Export `Countable` in `gmultiset`, without that, the file is useless.

parent 6ee0e09e
No related branches found
No related tags found
1 merge request!167Add solver `multiset_solver` for multisets
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 0 deletions
theories/gmultiset.v
+ 1
− 0
View file @ fd6905fa
From stdpp Require Export countable.
From stdpp Require Import gmap.
Set Default Proof Using "Type".
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment