diff options
| author | Gaëtan Gilbert | 2020-11-23 15:49:44 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-11-23 15:49:44 +0100 |
| commit | 8c2caf0caee19fd8e67e52e05bfc4a8d9ca8d186 (patch) | |
| tree | 3e4d9b348c7ce7ab1d748af82d38dbe241f9370f /kernel/retroknowledge.mli | |
| parent | 94d579844817edcbb2454dd9dc79071b2cd1d12a (diff) | |
Remove unused retro_refl
Diffstat (limited to 'kernel/retroknowledge.mli')
| -rw-r--r-- | kernel/retroknowledge.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index fd412cdd0a..80c0baaf95 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -29,7 +29,6 @@ type retroknowledge = { (* PNormal, NNormal, PSubn, NSubn, PZero, NZero, PInf, NInf, NaN *) - retro_refl : constructor option } val empty : retroknowledge |