diff options
Diffstat (limited to 'kernel/retroknowledge.ml')
| -rw-r--r-- | kernel/retroknowledge.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index 34f62defb8..0d1bb1e586 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -53,7 +53,7 @@ type int31_field = | Int31Lxor type field = - | KInt31 of string*int31_field + | KInt31 of int31_field (* record representing all the flags of the internal state of the kernel *) |