Can I extract part of a module instead of the whole module?

Using Coq
1

Is there a way to tell Coq to only extract a subset of the definitions in a module? Here’s a minimal example:

Require Coq.extraction.Extraction.

Module Type AType.
  Parameter a : nat.
End AType.

Module BMod (A : AType).
  Definition foo : nat := 4 + A.a.
  Definition bar : bool := false.
End BMod.

Module AMod <: AType.
  Definition a := 3.
End AMod.

Module B := BMod AMod.
Recursive Extraction B.bar.

The “Recursive Extraction” here will generate OCaml code that contains B.foo and B.bar, even though I only wanted B.bar. This could be a problem when B.foo is some complicated function that is only used for proof, and never intended to be executed.

In case that’s too abstract, here’s my exact use case: I have a module containing functions for manipulating quantum programs, expressed as a list of gates (SQIR/UnitaryListRepresentation.v at main · inQWIRE/SQIR · GitHub). Within this module, I have a function that computes the semantics of a quantum program. This denotation function is only used for proofs (and has a lot of machinery behind it) so I really don’t want to extract it to OCaml. One possible solution is to manually extract this denotation function to some dummy value (with “Extract Constant”), but that seems hacky. Do I need to move the denotation function & anything that uses it to a different module?