From 1c769f0ab5f81177e52980c47e3e42defab230eb Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Tue, 15 Sep 2026 16:17:06 -0400 Subject: [PATCH] small proof fix --- rocq-brick-libstdcpp/test/array/test_cpp_proof.v | 1 - 1 file changed, 1 deletion(-) diff --git a/rocq-brick-libstdcpp/test/array/test_cpp_proof.v b/rocq-brick-libstdcpp/test/array/test_cpp_proof.v index f2286f0a..55972fcd 100644 --- a/rocq-brick-libstdcpp/test/array/test_cpp_proof.v +++ b/rocq-brick-libstdcpp/test/array/test_cpp_proof.v @@ -215,7 +215,6 @@ Section with_cpp. Lemma last_via_end_ok : verify[ source ] last_via_end_spec. Proof using MOD. verify_spec; go. - rewrite !o_sub_sub /=. go. Qed. (** <>'s iterators are raw pointers, so a condition such as