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 23bac0b27..23bac0b27 100644 --- a/kernel/machops.ml +++ b/kernel/typeops.ml diff --git a/kernel/machops.mli b/kernel/typeops.mli index 1a3b729c2..1a3b729c2 100644 --- a/kernel/machops.mli +++ b/kernel/typeops.mli diff --git a/kernel/mach.ml b/kernel/typing.ml index 2311fb999..2311fb999 100644 --- a/kernel/mach.ml +++ b/kernel/typing.ml diff --git a/kernel/mach.mli b/kernel/typing.mli index 9e37c4c79..9e37c4c79 100644 --- a/kernel/mach.mli +++ b/kernel/typing.mli |