diff options
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/CSEproof.v | 4 | ||||
| -rw-r--r-- | backend/Cminor.v | 2 | ||||
| -rw-r--r-- | backend/Constpropproof.v | 4 | ||||
| -rw-r--r-- | backend/LTL.v | 2 | ||||
| -rw-r--r-- | backend/Linear.v | 2 | ||||
| -rw-r--r-- | backend/Linearizeproof.v | 6 | ||||
| -rw-r--r-- | backend/Mach.v | 2 | ||||
| -rw-r--r-- | backend/PPC.v | 2 | ||||
| -rw-r--r-- | backend/RTL.v | 2 | ||||
| -rw-r--r-- | backend/RTLtyping.v | 4 | ||||
| -rw-r--r-- | backend/Tunnelingproof.v | 6 |
11 files changed, 18 insertions, 18 deletions
diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 4420269..79657c5 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -765,13 +765,13 @@ Lemma functions_translated: forall (v: val) (f: RTL.fundef), Genv.find_funct ge v = Some f -> Genv.find_funct tge v = Some (transf_fundef f). -Proof (@Genv.find_funct_transf _ _ transf_fundef prog). +Proof (@Genv.find_funct_transf _ _ _ transf_fundef prog). Lemma funct_ptr_translated: forall (b: block) (f: RTL.fundef), Genv.find_funct_ptr ge b = Some f -> Genv.find_funct_ptr tge b = Some (transf_fundef f). -Proof (@Genv.find_funct_ptr_transf _ _ transf_fundef prog). +Proof (@Genv.find_funct_ptr_transf _ _ _ transf_fundef prog). Lemma sig_translated: forall (f: RTL.fundef), diff --git a/backend/Cminor.v b/backend/Cminor.v index 9eed009..6fdf602 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -80,7 +80,7 @@ Record function : Set := mkfunction { }. Definition fundef := AST.fundef function. -Definition program := AST.program fundef. +Definition program := AST.program fundef unit. Definition funsig (fd: fundef) := match fd with diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 38ba38b..ee24187 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -653,13 +653,13 @@ Lemma functions_translated: forall (v: val) (f: RTL.fundef), Genv.find_funct ge v = Some f -> Genv.find_funct tge v = Some (transf_fundef f). -Proof (@Genv.find_funct_transf _ _ transf_fundef prog). +Proof (@Genv.find_funct_transf _ _ _ transf_fundef prog). Lemma function_ptr_translated: forall (v: block) (f: RTL.fundef), Genv.find_funct_ptr ge v = Some f -> Genv.find_funct_ptr tge v = Some (transf_fundef f). -Proof (@Genv.find_funct_ptr_transf _ _ transf_fundef prog). +Proof (@Genv.find_funct_ptr_transf _ _ _ transf_fundef prog). Lemma sig_translated: forall (f: RTL.fundef), diff --git a/backend/LTL.v b/backend/LTL.v index f20ba3f..0dc9702 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -64,7 +64,7 @@ Record function: Set := mkfunction { Definition fundef := AST.fundef function. -Definition program := AST.program fundef. +Definition program := AST.program fundef unit. Definition funsig (fd: fundef) := match fd with diff --git a/backend/Linear.v b/backend/Linear.v index 2520f5b..0f1a31f 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -54,7 +54,7 @@ Record function: Set := mkfunction { Definition fundef := AST.fundef function. -Definition program := AST.program fundef. +Definition program := AST.program fundef unit. Definition funsig (fd: fundef) := match fd with diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index 22bf19c..5937fc3 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -27,18 +27,18 @@ Lemma functions_translated: forall v f, Genv.find_funct ge v = Some f -> Genv.find_funct tge v = Some (transf_fundef f). -Proof (@Genv.find_funct_transf _ _ transf_fundef prog). +Proof (@Genv.find_funct_transf _ _ _ transf_fundef prog). Lemma function_ptr_translated: forall v f, Genv.find_funct_ptr ge v = Some f -> Genv.find_funct_ptr tge v = Some (transf_fundef f). -Proof (@Genv.find_funct_ptr_transf _ _ transf_fundef prog). +Proof (@Genv.find_funct_ptr_transf _ _ _ transf_fundef prog). Lemma symbols_preserved: forall id, Genv.find_symbol tge id = Genv.find_symbol ge id. -Proof (@Genv.find_symbol_transf _ _ transf_fundef prog). +Proof (@Genv.find_symbol_transf _ _ _ transf_fundef prog). Lemma sig_preserved: forall f, funsig (transf_fundef f) = LTL.funsig f. diff --git a/backend/Mach.v b/backend/Mach.v index 1a9a94a..75b5baa 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -61,7 +61,7 @@ Record function: Set := mkfunction Definition fundef := AST.fundef function. -Definition program := AST.program fundef. +Definition program := AST.program fundef unit. Definition funsig (fd: fundef) := match fd with diff --git a/backend/PPC.v b/backend/PPC.v index 37f882b..3aa4ec4 100644 --- a/backend/PPC.v +++ b/backend/PPC.v @@ -286,7 +286,7 @@ lbl: .long 0x43300000, 0x00000000 Definition code := list instruction. Definition fundef := AST.fundef code. -Definition program := AST.program fundef. +Definition program := AST.program fundef unit. (** * Operational semantics *) diff --git a/backend/RTL.v b/backend/RTL.v index 4a3f8e8..8b46a7d 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -92,7 +92,7 @@ Record function: Set := mkfunction { Definition fundef := AST.fundef function. -Definition program := AST.program fundef. +Definition program := AST.program fundef unit. Definition funsig (fd: fundef) := match fd with diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index 33338d3..449e837 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -466,10 +466,10 @@ Proof. apply wt_regset_assign. auto. rewrite H11. rewrite <- H1. assert (wt_fundef f). destruct ros; simpl in H0. - pattern f. apply Genv.find_funct_prop with fundef p (rs#r). + pattern f. apply Genv.find_funct_prop with fundef unit p (rs#r). exact wt_p. exact H0. caseEq (Genv.find_symbol ge i); intros; rewrite H12 in H0. - pattern f. apply Genv.find_funct_ptr_prop with fundef p b. + pattern f. apply Genv.find_funct_ptr_prop with fundef unit p b. exact wt_p. exact H0. discriminate. eapply H3. auto. rewrite H1. rewrite <- H10. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 88547e7..eae53ca 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -84,18 +84,18 @@ Lemma functions_translated: forall v f, Genv.find_funct ge v = Some f -> Genv.find_funct tge v = Some (tunnel_fundef f). -Proof (@Genv.find_funct_transf _ _ tunnel_fundef p). +Proof (@Genv.find_funct_transf _ _ _ tunnel_fundef p). Lemma function_ptr_translated: forall v f, Genv.find_funct_ptr ge v = Some f -> Genv.find_funct_ptr tge v = Some (tunnel_fundef f). -Proof (@Genv.find_funct_ptr_transf _ _ tunnel_fundef p). +Proof (@Genv.find_funct_ptr_transf _ _ _ tunnel_fundef p). Lemma symbols_preserved: forall id, Genv.find_symbol tge id = Genv.find_symbol ge id. -Proof (@Genv.find_symbol_transf _ _ tunnel_fundef p). +Proof (@Genv.find_symbol_transf _ _ _ tunnel_fundef p). Lemma sig_preserved: forall f, funsig (tunnel_fundef f) = funsig f. |