aboutsummaryrefslogtreecommitdiff
path: root/theories/NArith
diff options
context:
space:
mode:
authorJPR2019-05-23 23:28:55 +0200
committerJPR2019-05-23 23:28:55 +0200
commitd306f5428db0d034aea55d3f0699c67c1f296cc1 (patch)
tree540bcc09ec46c8a360cda9ed7fafa9ab631d3716 /theories/NArith
parent5cfdc20560392c2125dbcee31cfd308d5346b428 (diff)
Fixing typos - Part 3
Diffstat (limited to 'theories/NArith')
-rw-r--r--theories/NArith/BinNatDef.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index be12fffaaf..3e5987127a 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -25,7 +25,7 @@ Module N.
Definition t := N.
-(** ** Nicer name [N.pos] for contructor [Npos] *)
+(** ** Nicer name [N.pos] for constructor [Npos] *)
Notation pos := Npos.