From 915e61f6e1e74575f227b7ec38cd7d83f556f280 Mon Sep 17 00:00:00 2001 From: LennartBeringer Date: Fri, 13 Oct 2023 15:32:46 -0400 Subject: [PATCH] removed a call to try simple apply eq_refl in SC_tac --- floyd/VSU.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/floyd/VSU.v b/floyd/VSU.v index c9682d738..ee296384c 100644 --- a/floyd/VSU.v +++ b/floyd/VSU.v @@ -888,7 +888,7 @@ Ltac SC_tac := lazymatch goal with | |- Funspecs_must_match ?i _ _ => try solve [constructor; unfold abbreviate; - try simple apply eq_refl; + (*Lennart: don't do try simple apply eq_refl;*) repeat f_equal] | |- Identifier_not_found ?i ?fds2 => fail "identifer" i "not found in funspecs" fds2