diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-11-04 11:47:42 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-11-04 11:47:42 +0000 |
| commit | ef0d007a20bfe6ed26add13e7459d17ed2bd3eb3 (patch) | |
| tree | c38835d82bc3cd034f788c44f24271d84e086115 /src/hls/RTLBlock.v | |
| parent | b2d0b8f1fa008eaecdc07ffb92220cc601b70b28 (diff) | |
| download | vericert-kvx-ef0d007a20bfe6ed26add13e7459d17ed2bd3eb3.tar.gz vericert-kvx-ef0d007a20bfe6ed26add13e7459d17ed2bd3eb3.zip | |
Quick compile fix
Diffstat (limited to 'src/hls/RTLBlock.v')
| -rw-r--r-- | src/hls/RTLBlock.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v index e5ce9a7..117d21b 100644 --- a/src/hls/RTLBlock.v +++ b/src/hls/RTLBlock.v @@ -76,7 +76,7 @@ Definition successors_instr (i : control_flow_inst) : list node := | RBgoto n => n :: nil end. -Definition genv := Genv.t fundef unit. +(* Definition genv := Genv.t fundef unit. Definition regset := Regmap.t val. Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := @@ -165,3 +165,6 @@ Inductive step : state -> trace -> state -> Prop := step (State s f sp pc rs m (mk_bblock nil (RBcond cond args ifso ifnot)) C) E0 (State s f sp pc' rs m (mk_bblock nil (RBcond cond args ifso ifnot)) N) . + +End RELSEM. +*) |