aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativelambda.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/nativelambda.mli')
-rw-r--r--kernel/nativelambda.mli2
1 files changed, 0 insertions, 2 deletions
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index ada63ebb4..997efd969 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -20,13 +20,11 @@ type lambda =
| Lvar of identifier
| Lprod of lambda * lambda
| Llam of name array * lambda
- | Lrec of name * lambda
| Llet of name * lambda * lambda
| Lapp of lambda * lambda array
| Lconst of string * constant (* prefix, constant name *)
| Lcase of annot_sw * lambda * lambda * lam_branches
(* annotations, term being matched, accu, branches *)
- | Lareint of lambda array
| Lif of lambda * lambda * lambda
| Lfix of (int array * int) * fix_decl
| Lcofix of int * fix_decl