diff options
| author | mdenes | 2013-01-22 17:37:00 +0000 |
|---|---|---|
| committer | mdenes | 2013-01-22 17:37:00 +0000 |
| commit | 6b908b5185a55a27a82c2b0fce4713812adde156 (patch) | |
| tree | c2857724d8b22ae3d7a91b3a683a57206caf9b54 /kernel/declarations.mli | |
| parent | 62ce65dadb0afb8815b26069246832662846c7ec (diff) | |
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
Diffstat (limited to 'kernel/declarations.mli')
| -rw-r--r-- | kernel/declarations.mli | 15 |
1 files changed, 14 insertions, 1 deletions
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 |