diff options
Diffstat (limited to 'driver/Compiler.v')
| -rw-r--r-- | driver/Compiler.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/Compiler.v b/driver/Compiler.v index dd752aca..5ced13e1 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -80,7 +80,7 @@ Parameter print_RTL: Z -> RTL.program -> unit. Parameter print_LTL: LTL.program -> unit. Parameter print_Mach: Mach.program -> unit. -Open Local Scope string_scope. +Local Open Scope string_scope. (** * Composing the translation passes *) |