aboutsummaryrefslogtreecommitdiffstats
path: root/src/extraction
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-02-22 18:41:33 +0000
committerYann Herklotz <git@yannherklotz.com>2021-02-22 18:41:33 +0000
commit91b62a7100ccb1f8910422bc4566bc57ade8f7e7 (patch)
tree5987436a23f446a42672061b7d8740b3a2775403 /src/extraction
parenta5ae227155f09822207c49d75fdbb6e4b7652936 (diff)
downloadvericert-91b62a7100ccb1f8910422bc4566bc57ade8f7e7.tar.gz
vericert-91b62a7100ccb1f8910422bc4566bc57ade8f7e7.zip
Add RTLPar printing
Diffstat (limited to 'src/extraction')
-rw-r--r--src/extraction/Extraction.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index 8aec96e..5c1dac5 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -141,6 +141,7 @@ Extract Constant Compiler.print_Cminor => "PrintCminor.print_if".
Extract Constant driver.Compiler.print_RTL => "PrintRTL.print_if".
Extract Constant Compiler.print_RTL => "PrintRTL.print_if".
Extract Constant Compiler.print_RTLBlock => "PrintRTLBlock.print_if".
+Extract Constant Compiler.print_RTLPar => "PrintRTLPar.print_if".
Extract Constant Compiler.print_HTL => "PrintHTL.print_if".
Extract Constant Compiler.print_LTL => "PrintLTL.print_if".
Extract Constant Compiler.print_Mach => "PrintMach.print_if".