diff options
| author | letouzey | 2011-01-28 13:20:41 +0000 |
|---|---|---|
| committer | letouzey | 2011-01-28 13:20:41 +0000 |
| commit | f19a9d9d3a410fda982b2cf9154da5774f9ec84f (patch) | |
| tree | 23e166d4564ec1382afb60ec0d03e976dcaff377 /kernel/cbytegen.ml | |
| parent | c7fb97fd915a732e1d91ca59fd635c95235052ce (diff) | |
Remove the "Boxed" syntaxes and the const_entry_boxed field
According to B. Gregoire, this stuff is obsolete. Fine control
on when to launch the VM in conversion problems is now provided
by VMcast. We were already almost never boxing definitions anymore
in stdlib files.
"(Un)Boxed Definition foo" will now trigger a parsing error,
same with Fixpoint. The option "(Un)Set Boxed Definitions"
aren't there anymore, but tolerated (as no-ops), since unknown
options raise a warning instead of an error by default.
Some more cleaning could be done in the vm.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13806 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/cbytegen.ml')
| -rw-r--r-- | kernel/cbytegen.ml | 11 |
1 files changed, 3 insertions, 8 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 9c00af5dff..337b907512 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -714,18 +714,13 @@ let compile env c = Format.print_flush(); *) init_code,!fun_code, Array.of_list fv -let compile_constant_body env body opaque boxed = +let compile_constant_body env body opaque = if opaque then BCconstant else match body with | None -> BCconstant | Some sb -> let body = Declarations.force sb in - if boxed then - let res = compile env body in - let to_patch = to_memory res in - BCdefined(true, to_patch) - else - match kind_of_term body with + match kind_of_term body with | Const kn' -> (* we use the canonical name of the constant*) let con= constant_of_kn (canonical_con kn') in @@ -733,7 +728,7 @@ let compile_constant_body env body opaque boxed = | _ -> let res = compile env body in let to_patch = to_memory res in - BCdefined (false, to_patch) + BCdefined to_patch (* spiwack: additional function which allow different part of compilation of the |