aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/names.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-05-29 21:01:23 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-06-04 19:25:22 +0200
commit62012e2d412d8586bd62b60beeb0b4005a66151f (patch)
tree53c3f21b2f972a383c4b603bcae11bd13d257a6f /kernel/names.ml
parentb91f5d1adbd039809e31b5311d06b376829de1fc (diff)
A few typos.
Diffstat (limited to 'kernel/names.ml')
-rw-r--r--kernel/names.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/names.ml b/kernel/names.ml
index ae3403335..d7c0a5e98 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -590,7 +590,7 @@ module Constant = KerPair
module Cmap = HMap.Make(Constant.CanOrd)
(** A map whose keys are constants (values of the {!Constant.t} type).
- Keys are ordered wrt. "cannonical form" of the constant. *)
+ Keys are ordered wrt. "canonical form" of the constant. *)
module Cmap_env = HMap.Make(Constant.UserOrd)
(** A map whose keys are constants (values of the {!Constant.t} type).