removed a call to try simple apply eq_refl in SC_tac

PrincetonUniversity · Oct 13, 2023 · 915e61f · 915e61f
1 parent eb266da
commit 915e61f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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