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

**URL:** https://discourse.rocq-prover.org/t/can-i-extract-part-of-a-module-instead-of-the-whole-module/1194
**Category:** Using Rocq
**Created:** [January 20, 2021, 2:55am UTC](https://discourse.rocq-prover.org/t/can-i-extract-part-of-a-module-instead-of-the-whole-module/1194 "2021-01-20T02:55:51Z")
**Posts on this page:** 1
**Page:** 1

<div class="post-metadata">

### Author: ![khieta](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/khieta/32/469_2.png) [@khieta](https://discourse.rocq-prover.org/u/khieta)
#### Post date: [January 20, 2021, 2:55am UTC](https://discourse.rocq-prover.org/t/can-i-extract-part-of-a-module-instead-of-the-whole-module/1194/1 "2021-01-20T02:55:51Z")

</div>

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](https://github.com/inQWIRE/SQIR/blob/main/VOQC/src/UnitaryListRepresentation.v)). 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?