diff options
Diffstat (limited to 'driver')
| -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 7849d64..b0dce15 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -176,7 +176,7 @@ Definition transf_c_program (p: Csyntax.program) : res Asm.program := (** Force [Initializers] to be extracted as well. *) -Definition transl_single_init := Initializers.transl_init_single. +Definition transl_init := Initializers.transl_init. (** The following lemmas help reason over compositions of passes. *) |