# Developing plugins

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

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

---

## [About the Developing plugins category](https://discourse.rocq-prover.org/t/about-the-developing-plugins-category/13)

<div class="topic-metadata">

**Author:** [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Replies:** 0\
**Last updated:** [February 10, 2019, 9:47pm UTC](https://discourse.rocq-prover.org/t/about-the-developing-plugins-category/13 "2019-02-10T21:47:06Z")

</div>

Ask questions and share experience and best practices about the development of Rocq plugins. Write to rocq+plugin-development@discoursemail.com to start a new topic in this category via e-mail.

---

## [Using vsrocq language server with Emacs](https://discourse.rocq-prover.org/t/using-vsrocq-language-server-with-emacs/3119)

<div class="topic-metadata">

**Author:** [@Michalis](https://discourse.rocq-prover.org/u/Michalis)\
**Replies:** 1\
**Last updated:** [September 29, 2026, 10:13pm UTC](https://discourse.rocq-prover.org/t/using-vsrocq-language-server-with-emacs/3119 "2026-09-29T22:13:33Z")

</div>

Has anyone looked at integrating the vsrocq language server with emacs? I have been using jpoiret/rocq-mode.el: An Emacs mode for the Rocq theorem prover, using coq-lsp - Codeberg.org, and I really like its workflow over…

---

## [Tuareg-mode doesn't really work for mlg file](https://discourse.rocq-prover.org/t/tuareg-mode-doesnt-really-work-for-mlg-file/2885)

<div class="topic-metadata">

**Author:** [@HuStmpHrrr](https://discourse.rocq-prover.org/u/HuStmpHrrr)\
**Replies:** 1\
**Last updated:** [December 20, 2025, 1:47pm UTC](https://discourse.rocq-prover.org/t/tuareg-mode-doesnt-really-work-for-mlg-file/2885 "2025-12-20T13:47:55Z")

</div>

the tutorial says to use tuareg mode for mlg files: rocq/doc/plugin\_tutorial at master · rocq-prover/rocq · GitHub However, in the same tutorial, when I open rocq/doc/plugin\_tutorial/tuto1/src/g\_tuto1.mlg at master · ro…

---

## [Any good resources on extracting Coq to other languages?](https://discourse.rocq-prover.org/t/any-good-resources-on-extracting-coq-to-other-languages/2709)

<div class="topic-metadata">

**Author:** [@Tralalero-Tralalal](https://discourse.rocq-prover.org/u/Tralalero-Tralalal)\
**Replies:** 0\
**Last updated:** [May 18, 2025, 12:27pm UTC](https://discourse.rocq-prover.org/t/any-good-resources-on-extracting-coq-to-other-languages/2709 "2025-05-18T12:27:22Z")

</div>

I’m curious as to whether there are any digestable resources on how to extract Coq (or any other theorem prover) into another language. What are you recommendations?

---

## [Figuring out How Rocq Imports Affect the names available to Smartlocate.global\_alias\_\* calls in an OCaml Plugin](https://discourse.rocq-prover.org/t/figuring-out-how-rocq-imports-affect-the-names-available-to-smartlocate-global-alias-calls-in-an-ocaml-plugin/2535)

<div class="topic-metadata">

**Author:** [@barclata](https://discourse.rocq-prover.org/u/barclata)\
**Replies:** 3\
**Last updated:** [February 14, 2025, 7:02am UTC](https://discourse.rocq-prover.org/t/figuring-out-how-rocq-imports-affect-the-names-available-to-smartlocate-global-alias-calls-in-an-ocaml-plugin/2535 "2025-02-14T07:02:36Z")

</div>

I’m developing a plugin that builds Rocq terms of a specific type (defined in a separate package) and adds them to the global environment as a definition. I’m using Smartlocate.global\_constructor\_with\_alias to get the co…

---

## [Best way to deal with mlg files warning-as-errors in plugins built by dune?](https://discourse.rocq-prover.org/t/best-way-to-deal-with-mlg-files-warning-as-errors-in-plugins-built-by-dune/2333)

<div class="topic-metadata">

**Author:** [@wolly](https://discourse.rocq-prover.org/u/wolly)\
**Replies:** 3\
**Last updated:** [June 22, 2024, 9:46am UTC](https://discourse.rocq-prover.org/t/best-way-to-deal-with-mlg-files-warning-as-errors-in-plugins-built-by-dune/2333 "2024-06-22T09:46:13Z")

</div>

Dear Coq Discourse, I have a question regarding how warnings are handled in .mlg files / coq.pp stanzas whilst building plugins with dune, and how one should go about setting up projects accordingly. Context I am a re…

---

## [Learning to write Coq plugins - what is the purpose of .mlg files?](https://discourse.rocq-prover.org/t/learning-to-write-coq-plugins-what-is-the-purpose-of-mlg-files/2317)

<div class="topic-metadata">

**Author:** [@wolly](https://discourse.rocq-prover.org/u/wolly)\
**Replies:** 5\
**Last updated:** [June 7, 2024, 11:22am UTC](https://discourse.rocq-prover.org/t/learning-to-write-coq-plugins-what-is-the-purpose-of-mlg-files/2317 "2024-06-07T11:22:59Z")

</div>

Dear Coq Discourse folks, After recently learning Coq to a level where I feel confident using all of Coqs user features and being able to load and use external plugins, I have come to the conclusion that for some of the…

---

## [Coq Plugin to output hypotheses, goal and tactic in JSON](https://discourse.rocq-prover.org/t/coq-plugin-to-output-hypotheses-goal-and-tactic-in-json/2220)

<div class="topic-metadata">

**Author:** [@florath](https://discourse.rocq-prover.org/u/florath)\
**Replies:** 4\
**Last updated:** [May 11, 2024, 8:11am UTC](https://discourse.rocq-prover.org/t/coq-plugin-to-output-hypotheses-goal-and-tactic-in-json/2220 "2024-05-11T08:11:38Z")

</div>

Hello! I want the following as JSON. In proofs: Goal (top one / first) all hypotheses last applied tactics For those I do not just need the string representation, but names and also the types (like variable, …). It l…

---

## [Proof of Concept in getting COQ running inside of LLama.cpp, need help](https://discourse.rocq-prover.org/t/proof-of-concept-in-getting-coq-running-inside-of-llama-cpp-need-help/2126)

<div class="topic-metadata">

**Author:** [@jmikedupont2](https://discourse.rocq-prover.org/u/jmikedupont2)\
**Replies:** 2\
**Last updated:** [December 12, 2023, 3:56pm UTC](https://discourse.rocq-prover.org/t/proof-of-concept-in-getting-coq-running-inside-of-llama-cpp-need-help/2126 "2023-12-12T15:56:22Z")

</div>

Dear Coq Community, I am humbly working on a proof of concept code that modifies the llama.cpp llm engine with callbacks for calling native code. The goals are :slight\_smile: that we can construct proofs about the stat…

---

## [Is there a way to extract ASTs from the Coq compiler?](https://discourse.rocq-prover.org/t/is-there-a-way-to-extract-asts-from-the-coq-compiler/1950)

<div class="topic-metadata">

**Author:** [@caverill](https://discourse.rocq-prover.org/u/caverill)\
**Replies:** 2\
**Last updated:** [June 15, 2023, 6:42pm UTC](https://discourse.rocq-prover.org/t/is-there-a-way-to-extract-asts-from-the-coq-compiler/1950 "2023-06-15T18:42:20Z")

</div>

I’m interested in analyzing the ASTs that the Coq compiler generates while it compiles. Is there any way to extract these by default, or will I have to go digging around in the compiler source?

---

## [A guide to building your Coq libraries and plugins with Dune](https://discourse.rocq-prover.org/t/a-guide-to-building-your-coq-libraries-and-plugins-with-dune/20)

<div class="topic-metadata">

**Author:** [@ejgallego](https://discourse.rocq-prover.org/u/ejgallego)\
**Replies:** 35\
**Last updated:** [April 29, 2023, 3:21am UTC](https://discourse.rocq-prover.org/t/a-guide-to-building-your-coq-libraries-and-plugins-with-dune/20 "2023-04-29T03:21:12Z")

</div>

Developing Coq plugins and libraries using Dune as their build system does offer some extra features and flexibility when compared to the traditional coq\_makefile setup: compositional build: you can drop your plugin in…

---

## [How does one access the dependent type unification algorithm from Coq's internals -- especially the one from apply and the substitution solution?](https://discourse.rocq-prover.org/t/how-does-one-access-the-dependent-type-unification-algorithm-from-coqs-internals-especially-the-one-from-apply-and-the-substitution-solution/1731)

<div class="topic-metadata">

**Author:** [@brando90](https://discourse.rocq-prover.org/u/brando90)\
**Replies:** 0\
**Last updated:** [July 13, 2022, 2:09pm UTC](https://discourse.rocq-prover.org/t/how-does-one-access-the-dependent-type-unification-algorithm-from-coqs-internals-especially-the-one-from-apply-and-the-substitution-solution/1731 "2022-07-13T14:09:55Z")

</div>

Cross posting because I’ve found that the discussions allows on this cite (that are not usually allowed on stack overflow) can be very useful. So posting: TLDR: I want to be able to compare two terms – one with a hole …

---

## [What are Generic Arguments in Coq and how are they structured in their OCaml code?](https://discourse.rocq-prover.org/t/what-are-generic-arguments-in-coq-and-how-are-they-structured-in-their-ocaml-code/1732)

<div class="topic-metadata">

**Author:** [@brando90](https://discourse.rocq-prover.org/u/brando90)\
**Replies:** 0\
**Last updated:** [July 14, 2022, 7:20pm UTC](https://discourse.rocq-prover.org/t/what-are-generic-arguments-in-coq-and-how-are-they-structured-in-their-ocaml-code/1732 "2022-07-14T19:20:25Z")

</div>

I was trying to figure out why it seems that in a Coq generic argument there seems to be 3 arguments to the constructor GenArg when according to me there should only be 2 (plus one of the argument seems to skip to other …

---

## [How to evaluate proof terms through opaque definitions?](https://discourse.rocq-prover.org/t/how-to-evaluate-proof-terms-through-opaque-definitions/1664)

<div class="topic-metadata">

**Author:** [@Gopiandcode](https://discourse.rocq-prover.org/u/Gopiandcode)\
**Replies:** 0\
**Last updated:** [May 30, 2022, 8:49am UTC](https://discourse.rocq-prover.org/t/how-to-evaluate-proof-terms-through-opaque-definitions/1664 "2022-05-30T08:49:15Z")

</div>

I was wondering if there is a way to force computation over opaque terms, for the purposes of debugging/meta-analysis of proof scripts. I understand why Coq doesn’t do this by default, and guess it would probably intera…

---

## [Cannot Compile Ynot Library in CoqIDE](https://discourse.rocq-prover.org/t/cannot-compile-ynot-library-in-coqide/1416)

<div class="topic-metadata">

**Author:** [@lyl](https://discourse.rocq-prover.org/u/lyl)\
**Replies:** 4\
**Last updated:** [May 12, 2022, 8:22am UTC](https://discourse.rocq-prover.org/t/cannot-compile-ynot-library-in-coqide/1416 "2022-05-12T08:22:29Z")

</div>

I am working on compiling Ynot library (8.3pl2 Release). My idea is just to follow its Tutorial to get a sense of how it turns Coq to be non-terminated and have side effects. Then, I would like to re-implement the certif…

---

## [Calling Coq from OCaml](https://discourse.rocq-prover.org/t/calling-coq-from-ocaml/1643)

<div class="topic-metadata">

**Author:** [@Gopiandcode](https://discourse.rocq-prover.org/u/Gopiandcode)\
**Replies:** 1\
**Last updated:** [April 22, 2022, 1:35pm UTC](https://discourse.rocq-prover.org/t/calling-coq-from-ocaml/1643 "2022-04-22T13:35:08Z")

</div>

I’m working on a project where for various reasons I’ve found myself needing to inspect the intermediate proof contexts of Coq proofs in a programmatic way from OCaml. Example: (\* proof.v \*) Lemma add\_comm: forall x …

---

## [Ltac2: unfold](https://discourse.rocq-prover.org/t/ltac2-unfold/1345)

<div class="topic-metadata">

**Author:** [@AoS](https://discourse.rocq-prover.org/u/AoS)\
**Replies:** 2\
**Last updated:** [June 10, 2021, 2:34pm UTC](https://discourse.rocq-prover.org/t/ltac2-unfold/1345 "2021-06-10T14:34:09Z")

</div>

Dear community, I would like to understand how to use the Ltac2 unfold tactic inside an Ltac2 function. I know that, when proving a goal, we can use unfold lemma\_name where lemma\_name is the name of a previously prov…

---

## [Ltac2: pose and exists](https://discourse.rocq-prover.org/t/ltac2-pose-and-exists/1344)

<div class="topic-metadata">

**Author:** [@AoS](https://discourse.rocq-prover.org/u/AoS)\
**Replies:** 1\
**Last updated:** [June 10, 2021, 1:29pm UTC](https://discourse.rocq-prover.org/t/ltac2-pose-and-exists/1344 "2021-06-10T13:29:25Z")

</div>

Dear community, I would like to create an Ltac2 function that does the equivalent of the following Coq tactics: pose (ident := constr); exists ident. An example of the above would be when proving a trivial statement o…

---

## [Ltac2: timeout tactic](https://discourse.rocq-prover.org/t/ltac2-timeout-tactic/1328)

<div class="topic-metadata">

**Author:** [@AoS](https://discourse.rocq-prover.org/u/AoS)\
**Replies:** 0\
**Last updated:** [May 30, 2021, 3:08pm UTC](https://discourse.rocq-prover.org/t/ltac2-timeout-tactic/1328 "2021-05-30T15:08:59Z")

</div>

Dear community, I would like to know if there is a native Ltac2 version of the timeout from Ltac1. I have tried to use this tactic in Ltac2, but I get the Unbound value timeout error. For instance, the following examp…

---

## [Ltac2: distinguishing between tactics with the same \`beginning\` of the name](https://discourse.rocq-prover.org/t/ltac2-distinguishing-between-tactics-with-the-same-beginning-of-the-name/1318)

<div class="topic-metadata">

**Author:** [@AoS](https://discourse.rocq-prover.org/u/AoS)\
**Replies:** 3\
**Last updated:** [May 23, 2021, 1:01pm UTC](https://discourse.rocq-prover.org/t/ltac2-distinguishing-between-tactics-with-the-same-beginning-of-the-name/1318 "2021-05-23T13:01:35Z")

</div>

Dear community, I was working with Ltac2 on creating some simple tactics, and I ran into the following problem: let us assume that we have some Ltac2 tactics Ltac2 Notation "Tactic name" s(constr) := ... Ltac2 Notation…

---

## [Ltac2: checking if an optional input variable is present](https://discourse.rocq-prover.org/t/ltac2-checking-if-an-optional-input-variable-is-present/1315)

<div class="topic-metadata">

**Author:** [@AoS](https://discourse.rocq-prover.org/u/AoS)\
**Replies:** 2\
**Last updated:** [May 21, 2021, 10:30am UTC](https://discourse.rocq-prover.org/t/ltac2-checking-if-an-optional-input-variable-is-present/1315 "2021-05-21T10:30:33Z")

</div>

Dear community, I am working with Ltac2 on creating several tactics, and some of them require having an optional argument/variable. I am wondering how to check whether the optional argument was indeed introduced when c…

---

## [Ltac2: Function to match a variable with a type](https://discourse.rocq-prover.org/t/ltac2-function-to-match-a-variable-with-a-type/1302)

<div class="topic-metadata">

**Author:** [@Nifrec](https://discourse.rocq-prover.org/u/Nifrec)\
**Replies:** 3\
**Last updated:** [May 10, 2021, 5:16pm UTC](https://discourse.rocq-prover.org/t/ltac2-function-to-match-a-variable-with-a-type/1302 "2021-05-10T17:16:11Z")

</div>

Dear Coq community, I have been trying to write a function in Ltac2 that takes two arguments: a constr ‘x’ that can be of any type a constr ‘t’ that is a Type I want this function to give different output if ‘x’ belo…

---

## [How to properly configure the ML load path for ocaml packages in opam projects](https://discourse.rocq-prover.org/t/how-to-properly-configure-the-ml-load-path-for-ocaml-packages-in-opam-projects/1109)

<div class="topic-metadata">

**Author:** [@Lasse](https://discourse.rocq-prover.org/u/Lasse)\
**Replies:** 7\
**Last updated:** [November 18, 2020, 3:54pm UTC](https://discourse.rocq-prover.org/t/how-to-properly-configure-the-ml-load-path-for-ocaml-packages-in-opam-projects/1109 "2020-11-18T15:54:57Z")

</div>

Hi Everyone, I’m trying to create a plugin that has dependencies on external OCaml packages. I am aware of the linking issues with this, but using dune I can compile my plugin with relative ease. The problem occurs whe…

---

## [Recommended resource for developing Coq plugin](https://discourse.rocq-prover.org/t/recommended-resource-for-developing-coq-plugin/1101)

<div class="topic-metadata">

**Author:** [@ZWY](https://discourse.rocq-prover.org/u/ZWY)\
**Replies:** 3\
**Last updated:** [November 5, 2020, 5:25pm UTC](https://discourse.rocq-prover.org/t/recommended-resource-for-developing-coq-plugin/1101 "2020-11-05T17:25:15Z")

</div>

I have been working on developing Coq plugins for more than one year. However, I am still struggling with the architecture of Coq source code and often can not find suitable functions inner Coq to implement my ideas. T…

---

## [Proofview.tactic to string or Pp.t](https://discourse.rocq-prover.org/t/proofview-tactic-to-string-or-pp-t/1025)

<div class="topic-metadata">

**Author:** [@randair](https://discourse.rocq-prover.org/u/randair)\
**Replies:** 3\
**Last updated:** [August 22, 2020, 11:07am UTC](https://discourse.rocq-prover.org/t/proofview-tactic-to-string-or-pp-t/1025 "2020-08-22T11:07:30Z")

</div>

Is there a way to print a Proofview.tactic as an Ltac expression?

---

## ["Running" Proofview.tactic to see if it would succeed](https://discourse.rocq-prover.org/t/running-proofview-tactic-to-see-if-it-would-succeed/973)

<div class="topic-metadata">

**Author:** [@randair](https://discourse.rocq-prover.org/u/randair)\
**Replies:** 1\
**Last updated:** [August 21, 2020, 5:05pm UTC](https://discourse.rocq-prover.org/t/running-proofview-tactic-to-see-if-it-would-succeed/973 "2020-08-21T17:05:10Z")

</div>

I’m writing a plugin that suggests a sequence of tactics to copy-and-paste into my proof. I would prefer not to generate tactics that fail. My idea is to first build the Proofview representation of these tactics, and th…

---

## [Can you pass tactics to a plugin?](https://discourse.rocq-prover.org/t/can-you-pass-tactics-to-a-plugin/974)

<div class="topic-metadata">

**Author:** [@randair](https://discourse.rocq-prover.org/u/randair)\
**Replies:** 4\
**Last updated:** [August 21, 2020, 5:03pm UTC](https://discourse.rocq-prover.org/t/can-you-pass-tactics-to-a-plugin/974 "2020-08-21T17:03:55Z")

</div>

Is it possible for a plugin command to get tactic scripts as input? I would imagine this is possible since try accepts an Ltac expression.

---

## [Real number without axiom](https://discourse.rocq-prover.org/t/real-number-without-axiom/903)

<div class="topic-metadata">

**Author:** [@itleigns](https://discourse.rocq-prover.org/u/itleigns)\
**Replies:** 8\
**Last updated:** [June 28, 2020, 2:52pm UTC](https://discourse.rocq-prover.org/t/real-number-without-axiom/903 "2020-06-28T14:52:47Z")

</div>

Hello everyone. I composed real number without using any axioms other than that of logic. Is this useful for the community?

---

## [Converting an Ltac tactic to Proofview.tactic](https://discourse.rocq-prover.org/t/converting-an-ltac-tactic-to-proofview-tactic/864)

<div class="topic-metadata">

**Author:** [@lukaszcz](https://discourse.rocq-prover.org/u/lukaszcz)\
**Replies:** 1\
**Last updated:** [May 30, 2020, 11:22am UTC](https://discourse.rocq-prover.org/t/converting-an-ltac-tactic-to-proofview-tactic/864 "2020-05-30T11:22:55Z")

</div>

Suppose I have tactic TAC declared in a \*.v file by Ltac TAC args := … I want to access it in a plugin at the OCaml level as a Proofview.tactic. What is the best way to do this? In particular, if TAC takes a constr argu…

---

## [How can an OCaml tactic return something else than unit?](https://discourse.rocq-prover.org/t/how-can-an-ocaml-tactic-return-something-else-than-unit/812)

<div class="topic-metadata">

**Author:** [@cloudyhug](https://discourse.rocq-prover.org/u/cloudyhug)\
**Replies:** 1\
**Last updated:** [April 29, 2020, 8:09am UTC](https://discourse.rocq-prover.org/t/how-can-an-ocaml-tactic-return-something-else-than-unit/812 "2020-04-29T08:09:12Z")

</div>

Hello everyone. I am currently trying to write a tactic in Ltac that needs to interact with a data structure remembering Coq terms. As these terms do not necessarily have the same types in Coq, the structure must be han…

[Next page](https://discourse.rocq-prover.org/c/plugin-development/6.md?page=1)