diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/typeops.ml (renamed from kernel/machops.ml) | 0 | ||||
| -rw-r--r-- | kernel/typeops.mli (renamed from kernel/machops.mli) | 0 | ||||
| -rw-r--r-- | kernel/typing.ml (renamed from kernel/mach.ml) | 0 | ||||
| -rw-r--r-- | kernel/typing.mli (renamed from kernel/mach.mli) | 0 |
4 files changed, 0 insertions, 0 deletions
diff --git a/kernel/machops.ml b/kernel/typeops.ml index 23bac0b277..23bac0b277 100644 --- a/kernel/machops.ml +++ b/kernel/typeops.ml diff --git a/kernel/machops.mli b/kernel/typeops.mli index 1a3b729c29..1a3b729c29 100644 --- a/kernel/machops.mli +++ b/kernel/typeops.mli diff --git a/kernel/mach.ml b/kernel/typing.ml index 2311fb9992..2311fb9992 100644 --- a/kernel/mach.ml +++ b/kernel/typing.ml diff --git a/kernel/mach.mli b/kernel/typing.mli index 9e37c4c798..9e37c4c798 100644 --- a/kernel/mach.mli +++ b/kernel/typing.mli |