diff options
Diffstat (limited to 'theories/FSets/FMapWeakInterface.v')
| -rw-r--r-- | theories/FSets/FMapWeakInterface.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/FSets/FMapWeakInterface.v b/theories/FSets/FMapWeakInterface.v index 22ff07c1ff..078d58d500 100644 --- a/theories/FSets/FMapWeakInterface.v +++ b/theories/FSets/FMapWeakInterface.v @@ -150,7 +150,7 @@ Module Type S. MapsTo x e m -> InA eq_key_elt (x,e) (elements m). Parameter elements_2 : InA eq_key_elt (x,e) (elements m) -> MapsTo x e m. - Parameter elements_3 : noredunA eq_key (elements m). + Parameter elements_3 : NoDupA eq_key (elements m). (** Specification of [fold] *) Parameter fold_1 : |