diff options
Diffstat (limited to 'src/hls/HTLgenspec.v')
| -rw-r--r-- | src/hls/HTLgenspec.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 309df3e..bd8a2e7 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -263,9 +263,9 @@ Ltac trans_step s1 s2 := (* Try to prove a goal about a state by first proving it for an earlier state and then transfering it to the final. *) Ltac monad_crush := crush; - match reverse goal with + match goal with | [ finalstate : st, prevstate : st |- _] => - match reverse goal with + match goal with | [ |- context f[finalstate]] => let inter := context f[prevstate] in try solve [ |