summaryrefslogtreecommitdiff
path: root/kernel/retroknowledge.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/retroknowledge.ml')
-rw-r--r--kernel/retroknowledge.ml19
1 files changed, 0 insertions, 19 deletions
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index d76b05a8..34f62def 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -25,22 +25,6 @@ open Constr
(* aliased type for clarity purpose*)
type entry = Constr.t
-(* [field]-s are the roles the kernel can learn of. *)
-type nat_field =
- | NatType
- | NatPlus
- | NatTimes
-
-type n_field =
- | NPositive
- | NType
- | NTwice
- | NTwicePlusOne
- | NPhi
- | NPhiInv
- | NPlus
- | NTimes
-
type int31_field =
| Int31Bits
| Int31Type
@@ -69,9 +53,6 @@ type int31_field =
| Int31Lxor
type field =
- (* | KEq
- | KNat of nat_field
- | KN of n_field *)
| KInt31 of string*int31_field