# Controlling Extraction of Specific Types

**URL:** https://discourse.rocq-prover.org/t/controlling-extraction-of-specific-types/2029
**Category:** Using Rocq
**Created:** [September 4, 2023, 5:48am UTC](https://discourse.rocq-prover.org/t/controlling-extraction-of-specific-types/2029 "2023-09-04T05:48:03Z")
**Posts on this page:** 1
**Page:** 1

<div class="post-metadata">

### Author: ![liuxingpeng520521](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/liuxingpeng520521/32/865_2.png) [@liuxingpeng520521](https://discourse.rocq-prover.org/u/liuxingpeng520521)
#### Post date: [September 4, 2023, 5:48am UTC](https://discourse.rocq-prover.org/t/controlling-extraction-of-specific-types/2029/1 "2023-09-04T05:48:03Z")

</div>

Why would Coq want to extract the specific Inductive definition to a specific OCaml type before extraction, isn’t that redundant?