aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
Diffstat (limited to 'driver')
-rw-r--r--driver/Compiler.vexpand2
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand
index 80db9097..a751b232 100644
--- a/driver/Compiler.vexpand
+++ b/driver/Compiler.vexpand
@@ -54,7 +54,7 @@ Require Import Compopts.
Parameter print_Clight: Clight.program -> unit.
Parameter print_Cminor: Cminor.program -> unit.
Parameter print_RTL: Z -> RTL.program -> unit.
-Parameter print_LTL: LTL.program -> unit.
+Parameter print_LTL: Z -> LTL.program -> unit.
Parameter print_Mach: Mach.program -> unit.
Local Open Scope string_scope.