aboutsummaryrefslogtreecommitdiff
path: root/kernel/retroknowledge.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/retroknowledge.mli')
-rw-r--r--kernel/retroknowledge.mli1
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