aboutsummaryrefslogtreecommitdiffstats
path: root/extraction
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2020-10-09 15:21:20 +0200
committerCyril SIX <cyril.six@kalray.eu>2020-10-09 15:21:20 +0200
commit3009ec015ab7261323c9e318cb703eaabca07d47 (patch)
treebd4056fb300aebe9f6c339f62376539446056892 /extraction
parentf9220cdfa449a8bdd0d0e2447084197b1ec6253a (diff)
downloadcompcert-kvx-3009ec015ab7261323c9e318cb703eaabca07d47.tar.gz
compcert-kvx-3009ec015ab7261323c9e318cb703eaabca07d47.zip
Changing duplicate verifier to be non optional
Diffstat (limited to 'extraction')
-rw-r--r--extraction/extraction.v2
1 files changed, 0 insertions, 2 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v
index e43594fc..bd396cd8 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -111,8 +111,6 @@ Extract Constant Compopts.generate_float_constants =>
"fun _ -> !Clflags.option_ffloatconstprop >= 2".
Extract Constant Compopts.optim_tailcalls =>
"fun _ -> !Clflags.option_ftailcalls".
-Extract Constant Compopts.optim_duplicate =>
- "fun _ -> (if !Clflags.option_fduplicate = -1 then false else true)".
Extract Constant Compopts.optim_constprop =>
"fun _ -> !Clflags.option_fconstprop".
Extract Constant Compopts.optim_CSE =>