diff options
| author |  mdenes <mdenes@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-22 17:37:00 +0000 |
|---|---|---|
| committer | mdenes <mdenes@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-22 17:37:00 +0000 |
| commit | 6b908b5185a55a27a82c2b0fce4713812adde156 (patch) | |
| tree | c2857724d8b22ae3d7a91b3a683a57206caf9b54 /lib | |
| 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 'lib')
| -rw-r--r-- | lib/flags.ml | 6 | ||||
| -rw-r--r-- | lib/flags.mli | 6 |
2 files changed, 12 insertions, 0 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index ffb324d53..765574cb4 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -160,3 +160,9 @@ let default_inline_level = 100 let inline_level = ref default_inline_level let set_inline_level = (:=) inline_level let get_inline_level () = !inline_level + +(* Disabling native code compilation for conversion and normalization *) +let no_native_compiler = ref false + +(* Print the mod uid associated to a vo file by the native compiler *) +let print_mod_uid = ref false diff --git a/lib/flags.mli b/lib/flags.mli index f529dd5df..6b26c50d9 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -100,3 +100,9 @@ val camlp4bin : string ref val set_inline_level : int -> unit val get_inline_level : unit -> int val default_inline_level : int + +(* Disabling native code compilation for conversion and normalization *) +val no_native_compiler : bool ref + +(* Print the mod uid associated to a vo file by the native compiler *) +val print_mod_uid : bool ref |