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.mli | |
| parent | 38be62b56799933cdfc783d4e538963c3aa59fef (diff) | |
Retroknowledge.KInt31: remove the (unused) group parameter
Diffstat (limited to 'kernel/retroknowledge.mli')
| -rw-r--r-- | kernel/retroknowledge.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 02d961d893..6b2c74e9df 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -46,7 +46,7 @@ type int31_field = | Int31Lxor type field = - | KInt31 of string*int31_field + | KInt31 of int31_field (** This type represent an atomic action of the retroknowledge. It is stored in the compiled libraries |