diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-22 08:08:21 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-22 08:08:21 +0200 |
| commit | f5da5188171962d13b9f3eac04845dd19d0aa931 (patch) | |
| tree | f33a9ff6a347fdea43f6fa6f48c540c67abd418d /backend | |
| parent | 25547c7d1f6a0fb75ff1d8e7287d9305e0dbf293 (diff) | |
| download | compcert-kvx-f5da5188171962d13b9f3eac04845dd19d0aa931.tar.gz compcert-kvx-f5da5188171962d13b9f3eac04845dd19d0aa931.zip | |
automated writing Compiler.v
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Allocationproof.v (renamed from backend/Allocproof.v) | 0 | ||||
| -rw-r--r-- | backend/Tunneling.v | 2 | ||||
| -rw-r--r-- | backend/Tunnelingproof.v | 2 |
3 files changed, 2 insertions, 2 deletions
diff --git a/backend/Allocproof.v b/backend/Allocationproof.v index 3c7df58a..3c7df58a 100644 --- a/backend/Allocproof.v +++ b/backend/Allocationproof.v diff --git a/backend/Tunneling.v b/backend/Tunneling.v index a4c4a195..78458582 100644 --- a/backend/Tunneling.v +++ b/backend/Tunneling.v @@ -101,5 +101,5 @@ Definition tunnel_function (f: LTL.function) : LTL.function := Definition tunnel_fundef (f: LTL.fundef) : LTL.fundef := transf_fundef tunnel_function f. -Definition tunnel_program (p: LTL.program) : LTL.program := +Definition transf_program (p: LTL.program) : LTL.program := transform_program tunnel_fundef p. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index d3b8a9f0..cdf6c800 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -22,7 +22,7 @@ Definition match_prog (p tp: program) := match_program (fun ctx f tf => tf = tunnel_fundef f) eq p tp. Lemma transf_program_match: - forall p, match_prog p (tunnel_program p). + forall p, match_prog p (transf_program p). Proof. intros. eapply match_transform_program; eauto. Qed. |