From b32404e4b21161e9bfe5d0b15948ba27564f8f8e Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Wed, 12 May 2021 19:30:01 +0100 Subject: Remove reverse matching from monad_crush Unnecessary --- src/hls/HTLgenspec.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/hls/HTLgenspec.v') 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 [ -- cgit