diff options
Diffstat (limited to 'theories/Sets/Multiset.v')
| -rwxr-xr-x | theories/Sets/Multiset.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index 9e79ee3a0..31d4c9430 100755 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -170,12 +170,12 @@ Apply multiset_twist2. Qed. -(* theory of minter to do similarly +(*i theory of minter to do similarly Require Min. (* multiset intersection *) Definition minter := [m1,m2:multiset] (Bag [a:A](min (multiplicity m1 a)(multiplicity m2 a))). -*) +i*) End multiset_defs. |