# Developing plugins

**URL:** https://discourse.rocq-prover.org/c/plugin-development/6.md?page=1

[Latest](https://discourse.rocq-prover.org/latest.md) · [Categories](https://discourse.rocq-prover.org/categories.md) · [Tags](https://discourse.rocq-prover.org/tags.md)

**Page:** 2

---

## [How do I solve "no implementation available for ..."?](https://discourse.rocq-prover.org/t/how-do-i-solve-no-implementation-available-for/466)

<div class="topic-metadata">

**Author:** [@JasonGross](https://discourse.rocq-prover.org/u/JasonGross)\
**Replies:** 1\
**Last updated:** [October 8, 2019, 6:16pm UTC](https://discourse.rocq-prover.org/t/how-do-i-solve-no-implementation-available-for/466 "2019-10-08T18:16:21Z")

</div>

I have the following setup: $ cat \_CoqProject -I . -Q . Top StrategyTactic.v strategy\_tactic.ml strategy\_tactic.mli strategy\_tactic\_plugin.mlg strategy\_tactic\_plugin.mllib $ cat StrategyTactic.v Declare ML Modul…

---

## [Get global environment from coq](https://discourse.rocq-prover.org/t/get-global-environment-from-coq/441)

<div class="topic-metadata">

**Author:** [@ZWY](https://discourse.rocq-prover.org/u/ZWY)\
**Replies:** 0\
**Last updated:** [September 23, 2019, 2:07pm UTC](https://discourse.rocq-prover.org/t/get-global-environment-from-coq/441 "2019-09-23T14:07:03Z")

</div>

Dear Coq developers, I want to get the information(constants and inductives) needed for current proof in coq while doing proof. For example, get the information while using copide. I think I need to extract the global e…

---

## [Best way to obtain constrs free from de Bruijn indices?](https://discourse.rocq-prover.org/t/best-way-to-obtain-constrs-free-from-de-bruijn-indices/366)

<div class="topic-metadata">

**Author:** [@palmskog](https://discourse.rocq-prover.org/u/palmskog)\
**Replies:** 4\
**Last updated:** [July 31, 2019, 3:30pm UTC](https://discourse.rocq-prover.org/t/best-way-to-obtain-constrs-free-from-de-bruijn-indices/366 "2019-07-31T15:30:35Z")

</div>

I need to “resolve” de Bruijn indices in constrs to their names to get better machine-readable representations. Is there a better way to do this than recursively traversing constr and constructing and querying an ad-ho…

---

## [Trouble adding a new definition to the environment in 8.9.1](https://discourse.rocq-prover.org/t/trouble-adding-a-new-definition-to-the-environment-in-8-9-1/364)

<div class="topic-metadata">

**Author:** [@emarzion](https://discourse.rocq-prover.org/u/emarzion)\
**Replies:** 3\
**Last updated:** [July 24, 2019, 10:05pm UTC](https://discourse.rocq-prover.org/t/trouble-adding-a-new-definition-to-the-environment-in-8-9-1/364 "2019-07-24T22:05:34Z")

</div>

I am trying to write a simple plugin that parses a text file and then adds a new term based on the data present in that file. I am following the tutorials present here and I think I can handle setting up the basic plugi…

[Previous page](https://discourse.rocq-prover.org/c/plugin-development/6.md)