diff options
| author | Maxime Dénès | 2015-10-27 23:27:50 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2015-10-28 16:57:55 +0100 |
| commit | 9ce6802ea563437b15e45198f4d8d0f716a576bb (patch) | |
| tree | 48dda29cb53de4d0eaf8258ee24bf2357d6ff071 /kernel | |
| parent | 95669265239c4da7f5cfcf134825f6801e52391f (diff) | |
Fix minor typo in native compiler.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/nativevalues.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index e4a7799933..40bef4bc67 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -10,7 +10,7 @@ open Names open Errors open Util -(** This modules defines the representation of values internally used by +(** This module defines the representation of values internally used by the native compiler *) type t = t -> t |