From 04a0552ee8c1611fbcf1d97ef43ae909b5e10316 Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Wed, 16 Sep 2026 02:46:18 -0400 Subject: [PATCH] fix vector proofs --- rocq-brick-libstdcpp/test/vector/test_cpp_proof.v | 1 - 1 file changed, 1 deletion(-) diff --git a/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v b/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v index 91b979d7..ecc407fd 100644 --- a/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v +++ b/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v @@ -132,7 +132,6 @@ Module Aggregate. Proof using MOD. verify_spec. wapply op_eq_ok. go using prim.primR_aggressiveC. - by []. Qed. Definition op_neq_B := [LINK] op_neq_ok.