From e821c6db95196ff8e2c075ab81dcf647f25a5b39 Mon Sep 17 00:00:00 2001 From: Thomas Sewell Date: Fri, 18 Aug 2023 17:16:25 +0100 Subject: [PATCH] CN: deactivate inlining of proxies for now There are various issues with this, and it leads to a more problematic error in the page table example anyway, so leave this disabled for now. --- backend/cn/main.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/backend/cn/main.ml b/backend/cn/main.ml index eeaaec540..45d7d6e56 100644 --- a/backend/cn/main.ml +++ b/backend/cn/main.ml @@ -61,7 +61,7 @@ let frontend incl_dirs incl_files astprints filename state_file = Cerb_global.set_cerb_conf "Cn" false Random false Basic false false false false false; Ocaml_implementation.set Ocaml_implementation.HafniumImpl.impl; Switches.set ["inner_arg_temps"; "at_magic_comments"; "warn_mismatched_magic_comments"]; - Core_peval.config_unfold_stdlib := Sym.has_id_with Setup.unfold_stdlib_name; +(* Core_peval.config_unfold_stdlib := Sym.has_id_with Setup.unfold_stdlib_name; *) let@ stdlib = load_core_stdlib () in let@ impl = load_core_impl stdlib impl_name in let conf = Setup.conf incl_dirs incl_files astprints in