diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-28 19:08:42 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-28 19:08:42 +0100 |
| commit | 1f994be34eac3ca0d938c213c58a36b3a57bad8c (patch) | |
| tree | c38c5268c3db1fb00a7d37889f1c32f0a8fd8624 /driver | |
| parent | 3bdfc2288714f1c238a5b59586aa1409f4eda056 (diff) | |
| download | compcert-kvx-1f994be34eac3ca0d938c213c58a36b3a57bad8c.tar.gz compcert-kvx-1f994be34eac3ca0d938c213c58a36b3a57bad8c.zip | |
forgot a "in *"
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Compiler.v | 21 |
1 files changed, 1 insertions, 20 deletions
diff --git a/driver/Compiler.v b/driver/Compiler.v index 33e31057..0dd413f5 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -289,26 +289,7 @@ Proof. set (p10 := total_if optim_constprop Constprop.transf_program p9) in *. set (p11 := total_if optim_constprop Renumber.transf_program p10) in *. destruct (partial_if optim_CSE CSE.transf_program p11) as [p12|e] eqn:P12; simpl in T; try discriminate. - set (p12bis := @total_if RTL.program optim_CSE2 CSE2.transf_program p12). - change (@eq (res Asm.program) - (apply_partial Mach.program Asm.program - (apply_partial Linear.program Mach.program - (apply_partial Linear.program Linear.program - (apply_total Linear.program Linear.program - (apply_partial LTL.program Linear.program - (apply_total LTL.program LTL.program - (apply_partial RTL.program LTL.program - (apply_partial RTL.program RTL.program - (@partial_if RTL.program optim_redundancy - Deadcode.transf_program - p12bis) - Unusedglob.transform_program) - Allocation.transf_program) - Tunneling.tunnel_program) Linearize.transf_program) - CleanupLabels.transf_program) - (@partial_if Linear.program debug Debugvar.transf_program)) - Stacking.transf_program) Asmgen.transf_program) - (@OK Asm.program tp)) in T. + set (p12bis := @total_if RTL.program optim_CSE2 CSE2.transf_program p12) in *. destruct (partial_if optim_redundancy Deadcode.transf_program p12bis) as [p13|e] eqn:P13; simpl in T; try discriminate. destruct (Unusedglob.transform_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. destruct (Allocation.transf_program p14) as [p15|e] eqn:P15; simpl in T; try discriminate. |