diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-12 19:30:01 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-12 19:30:01 +0100 |
| commit | b32404e4b21161e9bfe5d0b15948ba27564f8f8e (patch) | |
| tree | 87984015ae90774364fd88f19fedf8722a0529cf /src/hls/HTLgenspec.v | |
| parent | 938ea320d6b990ed1b7a8409a670bc847895da75 (diff) | |
| download | vericert-b32404e4b21161e9bfe5d0b15948ba27564f8f8e.tar.gz vericert-b32404e4b21161e9bfe5d0b15948ba27564f8f8e.zip | |
Remove reverse matching from monad_crush
Unnecessary
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 [ |