From d135b02a31b0ec84b61726a3d0aa7301b08a48ad Mon Sep 17 00:00:00 2001
From: mdenes
Date: Sat, 6 Jul 2013 23:55:57 +0000
Subject: Fixing a bug in the native compiler, introduced by r16363, leading to
 undefined variables in the generated code.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16619 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/declarations.mli | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'kernel/declarations.mli')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 24572da591..43b908e1fc 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -40,10 +40,12 @@ type constant_def =
   | Def of Lazyconstr.constr_substituted
   | OpaqueDef of Lazyconstr.lazy_constr
 
+(** Linking information for the native compiler. The boolean flag indicates if
+  the term is protected by a lazy tag *)
+
 type native_name =
-  | Linked of string
-  | LinkedLazy of string
-  | LinkedInteractive of string
+  | Linked of string * bool
+  | LinkedInteractive of string * bool
   | NotLinked
 
 type constant_body = {
-- 
cgit v1.2.3