diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-03-13 11:02:38 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-03-13 11:02:38 +0000 |
| commit | 5c46f0c4ba077bb6e21edbc32f5f23230c45380b (patch) | |
| tree | b42330865cbdebfb2c688572ff629e11f944fd8e /driver | |
| parent | 8fb2eba8404a1355d8867e0cfa0028ea941fcdaf (diff) | |
More global initialization work done and proved in Coq.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1603 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
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. *) |