Had to split Nativelambda in two files because of Retroknowledge

dependencies.

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;