diff options
Diffstat (limited to 'src/hls/HTLgen.v')
| -rw-r--r-- | src/hls/HTLgen.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index aa1064b..5400e25 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -163,10 +163,9 @@ Next Obligation. constructor; simpl; auto with htlh. Qed. Program Definition map_externctrl (othermod : ident) (ctrl : controlsignal) : mon reg := do r <- create_reg None (controlsignal_sz ctrl); - fun s => let r := s.(st_freshreg) in - OK r (mkstate + fun s => OK r (mkstate s.(st_st) - (Pos.succ r) + (st_freshreg s) (st_freshstate s) (st_scldecls s) (st_arrdecls s) |