From 6b908b5185a55a27a82c2b0fce4713812adde156 Mon Sep 17 00:00:00 2001
From: mdenes
Date: Tue, 22 Jan 2013 17:37:00 +0000
Subject: New implementation of the conversion test, using normalization by
 evaluation to native OCaml code.

Warning: the "retroknowledge" mechanism has not been ported to the native
compiler, because integers and persistent arrays will ultimately be defined as
primitive constructions. Until then, computation on numbers may be faster using
the VM, since it takes advantage of machine integers.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/declarations.mli | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

(limited to 'kernel/declarations.mli')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 2595aae07c..5b5e1750c1 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -62,12 +62,20 @@ type constant_def =
   | Def of constr_substituted
   | OpaqueDef of lazy_constr
 
+type native_name =
+  | Linked of string
+  | LinkedLazy of string
+  | LinkedInteractive of string
+  | NotLinked
+
 type constant_body = {
     const_hyps : section_context; (** New: younger hyp at top *)
     const_body : constant_def;
     const_type : constant_type;
     const_body_code : to_patch_substituted;
-    const_constraints : constraints }
+    const_constraints : constraints;
+    const_native_name : native_name ref;
+    const_inline_code : bool }
 
 val subst_const_def : substitution -> constant_def -> constant_def
 val subst_const_body : substitution -> constant_body -> constant_body
@@ -181,6 +189,11 @@ type mutual_inductive_body = {
 
     mind_constraints : constraints;  (** Universes constraints enforced by the inductive declaration *)
 
+(** {8 Data for native compilation } *)
+
+    mind_native_name : native_name ref; (** status of the code (linked or not, and where) *)
+
+
   }
 
 val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body
-- 
cgit v1.2.3