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
---
 lib/flags.ml  | 6 ++++++
 lib/flags.mli | 6 ++++++
 2 files changed, 12 insertions(+)

(limited to 'lib')

diff --git a/lib/flags.ml b/lib/flags.ml
index ffb324d535..765574cb4b 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 f529dd5df0..6b26c50d9e 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
-- 
cgit v1.2.3