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/RTLPar.v | |
| parent | b2d0b8f1fa008eaecdc07ffb92220cc601b70b28 (diff) | |
| download | vericert-ef0d007a20bfe6ed26add13e7459d17ed2bd3eb3.tar.gz vericert-ef0d007a20bfe6ed26add13e7459d17ed2bd3eb3.zip | |
Quick compile fix
Diffstat (limited to 'src/hls/RTLPar.v')
| -rw-r--r-- | src/hls/RTLPar.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v index 038ae32..0e94fd5 100644 --- a/src/hls/RTLPar.v +++ b/src/hls/RTLPar.v @@ -76,7 +76,7 @@ Definition successors_instr (i : control_flow_inst) : list node := | RPgoto n => n :: nil end. -Inductive state : Type := +(*Inductive state : Type := | State: forall (stack: list stackframe) (**r call stack *) (f: function) (**r current function *) @@ -96,3 +96,4 @@ Inductive state : Type := (v: val) (**r return value for the call *) (m: mem), (**r memory state *) state. +*) |