aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/retroknowledge.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/retroknowledge.ml')
-rw-r--r--kernel/retroknowledge.ml6
1 files changed, 4 insertions, 2 deletions
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index f064cd8b9..b82556c78 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -58,11 +58,13 @@ type int31_field =
| Int31Div
| Int31AddMulDiv
| Int31Compare
+ | Int31Head0
+ | Int31Tail0
type field =
- | KEq
+ (* | KEq
| KNat of nat_field
- | KN of n_field
+ | KN of n_field *)
| KInt31 of string*int31_field