diff options
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. +*) |