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

Remove unbound variable in type class instance for `multiset_solver`.

parent f6b14fe6
Branches
Tags
No related merge requests found
Pipeline #78816 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
stdpp/gmultiset.v
+ 1
− 1
View file @ edeef15e
...@@ -192,7 +192,7 @@ Section multiset_unfold. ...@@ -192,7 +192,7 @@ Section multiset_unfold.
Proof. done. Qed. Proof. done. Qed.
Global Instance multiset_unfold_empty x : MultisetUnfold x ∅ 0. Global Instance multiset_unfold_empty x : MultisetUnfold x ∅ 0.
Proof. constructor. by rewrite multiplicity_empty. Qed. Proof. constructor. by rewrite multiplicity_empty. Qed.
Global Instance multiset_unfold_singleton x y : Global Instance multiset_unfold_singleton x :
MultisetUnfold x {[+ x +]} 1. MultisetUnfold x {[+ x +]} 1.
Proof. constructor. by rewrite multiplicity_singleton. Qed. Proof. constructor. by rewrite multiplicity_singleton. Qed.
Global Instance multiset_unfold_union x X Y n m : Global Instance multiset_unfold_union x X Y n m :
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment