From 86357b63200368c818bbade20f2d71a3ddbaacb5 Mon Sep 17 00:00:00 2001
From: mdenes
Date: Mon, 25 Mar 2013 14:41:06 +0000
Subject: Native compiler: hash-consing of generated code and values.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16363 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/nativelambda.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'kernel/nativelambda.mli')

diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index ada63ebb42..997efd969f 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 
-- 
cgit v1.2.3