aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/MSets
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-11-24 15:14:19 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-11-24 15:14:19 +0100
commita27ac0315dcbb99c64a260bac3988199a26b39cf (patch)
tree2cf20f9ee79494c190cbd0fb8658872dd785d30b /theories/MSets
parentb16de62d20790930589795c3d10fbb07185ec22c (diff)
Fix some documentation typos.
Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else.
Diffstat (limited to 'theories/MSets')
-rw-r--r--theories/MSets/MSetList.v2
-rw-r--r--theories/MSets/MSetWeakList.v2
2 files changed, 2 insertions, 2 deletions
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index fb0d1ad9d..05c20eb8f 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -8,7 +8,7 @@
(** * Finite sets library *)
-(** This file proposes an implementation of the non-dependant
+(** This file proposes an implementation of the non-dependent
interface [MSetInterface.S] using strictly ordered list. *)
Require Export MSetInterface OrdersFacts OrdersLists.
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
index 372acd56a..2ac57a932 100644
--- a/theories/MSets/MSetWeakList.v
+++ b/theories/MSets/MSetWeakList.v
@@ -8,7 +8,7 @@
(** * Finite sets library *)
-(** This file proposes an implementation of the non-dependant
+(** This file proposes an implementation of the non-dependent
interface [MSetWeakInterface.S] using lists without redundancy. *)
Require Import MSetInterface.