From dcbfbdf8133963719b3d2f317ebf9ca47a72e9ba Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bluerock.io>
Date: Thu, 10 Sep 2026 21:58:06 -0400
Subject: [PATCH] add explicit goal selector

---
 rocq-brick-libstdcpp/proof/iostream/itree_prop.v | 12 +++++++-----
 rocq-brick-libstdcpp/test/g4g/prelude.v          | 13 +++++++++----
 2 files changed, 16 insertions(+), 9 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/iostream/itree_prop.v b/rocq-brick-libstdcpp/proof/iostream/itree_prop.v
index 0bfc710f..7f63844a 100644
--- a/rocq-brick-libstdcpp/proof/iostream/itree_prop.v
+++ b/rocq-brick-libstdcpp/proof/iostream/itree_prop.v
@@ -43,13 +43,15 @@ Section interp_itree.
   #[local]
   Instance interp_do_body_contractive {T} {K : T -> PROP} : Contractive (interp_do_body K).
   Proof using PROP_LATER.
-    repeat intro.
+    intros ??? Hdist x0.
     destruct x0; simpl; try eauto.
     { apply later_contractive. constructor.
-      intros. apply H. done. }
-    { eapply do_ne. done.
-      intro. apply bi.exist_ne; intro. apply bi.sep_ne. done. apply later_contractive.
-      constructor; intros; apply H; done. }
+      intros. apply Hdist. done. }
+    { eapply do_ne => //.
+      intro.
+      do 3 f_equiv => //.
+      apply later_contractive.
+      by constructor; intros; apply Hdist. }
   Qed.
 
   Definition interp_itree {T} (it : itree E T) (K : T -> PROP) : PROP :=
diff --git a/rocq-brick-libstdcpp/test/g4g/prelude.v b/rocq-brick-libstdcpp/test/g4g/prelude.v
index 42a2e560..4a6d0166 100644
--- a/rocq-brick-libstdcpp/test/g4g/prelude.v
+++ b/rocq-brick-libstdcpp/test/g4g/prelude.v
@@ -253,7 +253,9 @@ Section to_spectra.
     iSplitR.
     { iPureIntro.
       intros. destruct ANY_STEP.
-      inversion H0; subst. edestruct _safe0. done. intuition; eauto. }
+      inversion H0; subst.
+      edestruct _safe0; first by [].
+      intuition; eauto. }
     iIntros (?) "[% Hfrag]". iMod "Hclose".
     work.
     iApply bupd_fupd.
@@ -296,7 +298,9 @@ Section to_spectra.
     { iPureIntro. split.
       { apply AnyStep_invert_nonempty in ANY_STEP. tauto. }
       intros. destruct ANY_STEP.
-      inversion H1; subst. edestruct _safe0. done. intuition; eauto. }
+      inversion H1; subst.
+      edestruct _safe0; first by [].
+      intuition; eauto. }
     iIntros (?) "[% Hfrag]". iMod "Hclose".
     work.
     iApply bupd_fupd.
@@ -473,8 +477,9 @@ Proof.
         have->: (BS.String b str ++ rest = BS.String b (str ++ rest))%bs by done.
         constructor => //. }
       { inversion 1; subst.
-        eexists _; split. set_solver.
-        constructor. } } }
+        eexists _; split.
+        - set_solver.
+        - constructor. } } }
 Qed.
 
 #[global]