aboutsummaryrefslogtreecommitdiffstats
path: root/extraction
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-01-28 13:59:55 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-01-28 13:59:55 +0100
commit5412aea57eafe2868244a514471d480b83fc51bd (patch)
tree1fcca72f850293171c49ad9560001ce9e89f1354 /extraction
parent47bcd22f7e1febf10bd0629c1774b7ab39fac872 (diff)
downloadcompcert-kvx-5412aea57eafe2868244a514471d480b83fc51bd.tar.gz
compcert-kvx-5412aea57eafe2868244a514471d480b83fc51bd.zip
connected (just a silly problem)
Diffstat (limited to 'extraction')
-rw-r--r--extraction/extraction.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 521c0cdd..4635f5a2 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -108,6 +108,8 @@ Extract Constant Compopts.optim_constprop =>
"fun _ -> !Clflags.option_fconstprop".
Extract Constant Compopts.optim_CSE =>
"fun _ -> !Clflags.option_fcse".
+Extract Constant Compopts.optim_CSE2 =>
+ "fun _ -> !Clflags.option_fcse2".
Extract Constant Compopts.optim_redundancy =>
"fun _ -> !Clflags.option_fredundancy".
Extract Constant Compopts.thumb =>