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 75247f71..1cb5bd36 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -404,7 +404,7 @@ Ltac DestructM := eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Debugvarproof.transf_program_correct. eapply compose_forward_simulations. - eapply Stackingproof.transf_program_correct with (return_address_offset := Asmgenproof0.return_address_offset). + eapply Stackingproof.transf_program_correct with (return_address_offset := Asmgenproof.return_address_offset). exact Asmgenproof.return_address_exists. eassumption. eapply Asmgenproof.transf_program_correct; eassumption. |