# \#metacoq

**URL:** https://discourse.rocq-prover.org/tag/metacoq/11.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)

---

## [Habilitation à Diriger des Recherches de Matthieu Sozeau le 12 Février 2026](https://discourse.rocq-prover.org/t/habilitation-a-diriger-des-recherches-de-matthieu-sozeau-le-12-fevrier-2026/2918)

<div class="topic-metadata">

**Author:** [@mattam82](https://discourse.rocq-prover.org/u/mattam82)\
**Replies:** 0\
**Last updated:** [January 28, 2026, 10:26am UTC](https://discourse.rocq-prover.org/t/habilitation-a-diriger-des-recherches-de-matthieu-sozeau-le-12-fevrier-2026/2918 "2026-01-28T10:26:37Z")

</div>

It is my pleasure to invite you to my Habilitation to Supervise Research defense (in english), which will take place at the University of Nantes at 2pm on the 12th of February. This is going to be all about Rocq and Meta…

---

## [MetaCoq 1.3.1 release](https://discourse.rocq-prover.org/t/metacoq-1-3-1-release/2221)

<div class="topic-metadata">

**Author:** [@mattam82](https://discourse.rocq-prover.org/u/mattam82)\
**Replies:** 0\
**Last updated:** [March 19, 2024, 10:55am UTC](https://discourse.rocq-prover.org/t/metacoq-1-3-1-release/2221 "2024-03-19T10:55:00Z")

</div>

We are happy to announce release 1.3.1 of the MetaCoq project for Coq 8.17, 8.18 and 8.19, available both as source and through opam. This release will be part of the upcoming Coq Platform release including Coq 8.19. See…

---

## [MetaCoq: what's the \`term\` equivalent of \`\_\`?](https://discourse.rocq-prover.org/t/metacoq-whats-the-term-equivalent-of/559)

<div class="topic-metadata">

**Author:** [@joomy](https://discourse.rocq-prover.org/u/joomy)\
**Replies:** 1\
**Last updated:** [January 15, 2020, 12:10pm UTC](https://discourse.rocq-prover.org/t/metacoq-whats-the-term-equivalent-of/559 "2020-01-15T12:10:27Z")

</div>

Writing reified MetaCoq terms by hand can get tedious sometimes, is there a placeholder of the type term in MetaCoq that could be used for things that can be inferred by the type checker? And if it cannot be inferred the…