diff options
Diffstat (limited to 'kernel/nativelambda.mli')
| -rw-r--r-- | kernel/nativelambda.mli | 32 |
1 files changed, 1 insertions, 31 deletions
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 751f11978..d4be2279d 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -9,40 +9,10 @@ open Names open Term open Pre_env open Nativevalues +open Nativeinstr (** This file defines the lambda code generation phase of the native compiler *) -type lambda = - | Lrel of name * int - | Lvar of identifier - | Lmeta of metavariable * lambda (* type *) - | Levar of existential * lambda (* type *) - | Lprod of lambda * lambda - | Llam of name array * 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 *) - | Lif of lambda * lambda * lambda - | Lfix of (int array * int) * fix_decl - | Lcofix of int * fix_decl - | Lmakeblock of string * constructor * int * lambda array - (* prefix, constructor name, constructor tag, arguments *) - (* A fully applied constructor *) - | Lconstruct of string * constructor (* prefix, constructor name *) - (* A partially applied constructor *) - | Luint of Uint31.t - | Lval of Nativevalues.t - | Lsort of sorts - | Lind of string * inductive (* prefix, inductive name *) - | Llazy - | Lforce - -and lam_branches = (constructor * name array * lambda) array - -and fix_decl = name array * lambda array * lambda array - type evars = { evars_val : existential -> constr option; evars_typ : existential -> types; |