aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2014-08-12 11:03:05 -0400
committerGravatar Pierre Boutillier <pierre.boutillier@pps.univ-paris-diderot.fr>2014-08-25 15:22:40 +0200
commit876b1b39a0304c93c2511ca8dd34353413e91c9d (patch)
tree348c5630f0b35edf53fe4010587b61e615df03af /theories/FSets
parenta061b4d11fc681182b5bb946aa84d17d0b812225 (diff)
instanciation is French, instantiation is English
Diffstat (limited to 'theories/FSets')
-rw-r--r--theories/FSets/FMapAVL.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index fa33c1bf4..fe08960ad 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) :=
| Node l x d r _ => elements_aux ((x,d) :: elements_aux acc r) l
end.
-(** then [elements] is an instanciation with an empty [acc] *)
+(** then [elements] is an instantiation with an empty [acc] *)
Definition elements := elements_aux nil.