From 71722fe92cbadadb8785d6740019e74369901dd8 Mon Sep 17 00:00:00 2001 From: Alban Gruin <alban.gruin@irit.fr> Date: Wed, 27 Jul 2022 23:31:31 +0200 Subject: [PATCH] correct_store_buffer: proof simplification Signed-off-by: Alban Gruin <alban.gruin@irit.fr> --- src/correct_store_buffer.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v index ddfcc00..46b97db 100644 --- a/src/correct_store_buffer.v +++ b/src/correct_store_buffer.v @@ -305,6 +305,6 @@ Section monotonicity. - now destruct opc. (* st = Su, st' = Sn *) - - now destruct (ready _ _ _ && free _ _ _ _), (ready _ _ _ && free _ _ _ _), opc. + - now destruct (ready _ _ _ && free _ _ _ _), opc. Qed. End monotonicity. -- GitLab