fix(rocq_library): add self -Q even when out_dir is parent of dep paths

examples/rust_to_rocq/BUILD.bazel

@@ -27,22 +27,33 @@ coq_of_rust_library(
 )
 
 # Step 2: Compile the translated Rocq code
-# This compiles point.v to point.vo
+# This compiles point.v to point.vo.
+# `include_path` gives point.v a position-stable Rocq logical name --
+# `Example.point` -- regardless of whether this example is built nested in the
+# rules_rocq_rust workspace or standalone as its own BCR test module. Without
+# it, rocq_library would derive the prefix from ctx.label.package, which
+# differs between nested ("examples.rust_to_rocq") and standalone ("") and so
+# breaks point_proofs.v's import one way or the other.
 rocq_library(
     name = "point_compiled",
     srcs = [":point_translated"],
+    include_path = "Example",
     deps = [":rocq_of_rust_lib"],
     extra_flags = ["-impredicative-set"],
 )
 
 # Method 2: Convenience macro (recommended)
 # -----------------------------------------
 
-# Single target that does both translation and compilation
+# Single target that does both translation and compilation.
+# `include_path = "Example"` must match the one on `point_compiled` above:
+# both targets compile point.v to the same output path, and Bazel only
+# deduplicates the colliding actions if their args (including `-Q`) are equal.
 rocq_rust_verified_library(
     name = "point_verified",
     rust_sources = ["point.rs"],
     edition = "2021",
+    include_path = "Example",
     extra_flags = ["-impredicative-set"],
 )
 

examples/rust_to_rocq/point_proofs.v

@@ -11,7 +11,9 @@
     - The [monadic] tactic wraps Value.t expressions with [pure] *)
 
 Require Import RocqOfRust.RocqOfRust.
-From examples.rust_to_rocq Require Import point.
+(* `Example` is the stable logical prefix set by point_compiled's include_path
+   (see BUILD.bazel) -- resolves the same nested or standalone. *)
+From Example Require Import point.
 
 (* ========================================================================= *)
 (** * Section 1: Point::origin() Proofs *)

rocq/private/rocq.bzl

@@ -151,15 +151,18 @@ def _rocq_library_impl(ctx):
         # nested files like lib/lib.vo get the correct logical path RocqOfRust.lib.lib
         out_dir = output_dir if output_dir else vo_file.dirname
 
-        # Check if out_dir conflicts with deps
-        out_conflicts = out_dir in dep_paths
-        if not out_conflicts:
-            for dep_path in dep_paths.keys():
-                if dep_path.startswith(out_dir + "/"):
-                    # out_dir is a parent of dep_path - would override
-                    out_conflicts = True
-                    break
-        if not out_conflicts:
+        # coqc resolves overlapping `-Q dir prefix` mappings by deepest-ancestor
+        # match per source file, so adding a self `-Q` whose dir is a *parent*
+        # of a dep's `-Q` dir does not override the dep -- the dep's more
+        # specific mapping still wins for its own files. Only skip when a dep
+        # already maps this exact directory (where two `-Q`s with different
+        # prefixes for the same dir would be genuinely ambiguous).
+        #
+        # Without adding the self `-Q`, the compiled .vo gets no logical prefix
+        # (just the basename), which breaks `From <prefix> Require Import x`
+        # imports of generated files in root packages -- see the residual
+        # tracked in the rules_rust migration (Stage 4-fix follow-up).
+        if out_dir not in dep_paths:
             args.add("-Q")
             args.add(out_dir)
             args.add(logical_path)