diff options
| author | Vincent Laporte | 2018-09-07 11:18:28 +0200 |
|---|---|---|
| committer | Vincent Laporte | 2018-09-14 07:51:12 +0000 |
| commit | 4be2dd481c783bed7c09086b647d860e42b7ea9f (patch) | |
| tree | dfd9a32619175eedb084915ed53d56c356d55174 /kernel/retroknowledge.ml | |
| parent | 38be62b56799933cdfc783d4e538963c3aa59fef (diff) | |
Retroknowledge.KInt31: remove the (unused) group parameter
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 *) |