diff options
| -rw-r--r-- | theories/FSets/FMapAVL.v | 2 | ||||
| -rw-r--r-- | theories/MSets/MSetAVL.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index f9dda51255..684291d7ce 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -270,7 +270,7 @@ Fixpoint elements_aux (acc : list (key*elt)) m : list (key*elt) := (** then [elements] is an instanciation with an empty [acc] *) -Definition elements := elements_aux nil. +Definition elements m := elements_aux nil m. (** * Fold *) diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index 349cdedf7b..fee3f5bcfc 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -328,7 +328,7 @@ Fixpoint elements_aux (acc : list X.t) (s : t) : list X.t := (** then [elements] is an instanciation with an empty [acc] *) -Definition elements := elements_aux nil. +Definition elements s := elements_aux nil s. (** ** Filter *) |