diff options
Diffstat (limited to 'theories/FSets/FMapWeakList.v')
| -rw-r--r-- | theories/FSets/FMapWeakList.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v index e29bde236..38ed172b8 100644 --- a/theories/FSets/FMapWeakList.v +++ b/theories/FSets/FMapWeakList.v @@ -455,13 +455,13 @@ Variable elt':Type. (** * [map] and [mapi] *) -Fixpoint map (f:elt -> elt') (m:t elt) {struct m} : t elt' := +Fixpoint map (f:elt -> elt') (m:t elt) : t elt' := match m with | nil => nil | (k,e)::m' => (k,f e) :: map f m' end. -Fixpoint mapi (f: key -> elt -> elt') (m:t elt) {struct m} : t elt' := +Fixpoint mapi (f: key -> elt -> elt') (m:t elt) : t elt' := match m with | nil => nil | (k,e)::m' => (k,f k e) :: mapi f m' |