From 9e29a351fd0928130fa0b67dc47b67cdf989e4b7 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 24 Jun 2020 17:53:36 +0100 Subject: Fixes to make develop compile --- src/translation/HTLgen.v | 2 +- src/translation/HTLgenproof.v | 2 +- src/translation/HTLgenspec.v | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) (limited to 'src/translation') diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 66170bc..eb2ddda 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -559,7 +559,7 @@ Definition transl_program (p: RTL.program) : Errors.res HTL.program := (fun i v => Errors.OK v) p. *) -Definition main_is_internal {A B : Type} (p : AST.program A B) : bool := +Definition main_is_internal (p : RTL.program) : bool := let ge := Globalenvs.Genv.globalenv p in match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with | Some b => diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 9b59269..724ac0a 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -393,7 +393,7 @@ Section CORRECTNESS. 2: { reflexivity. } rewrite AssocMap.gss. unfold Verilog.merge_arr. - setoid_rewrite H1. + setoid_rewrite H3. reflexivity. rewrite combine_length. diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 7d89a76..c617174 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -140,7 +140,7 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - forall mem addr args s s' i c src n, translate_arr_access mem addr args stk s = OK c s' i -> tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src)) - (state_goto st n). + (state_goto st n) | tr_instr_Ijumptable : forall cexpr tbl r, cexpr = tbl_to_case_expr st tbl -> -- cgit