All issues

Search results

invalid link in README

Status: Open.

#1273 In MetaRocq/metarocq;

· fblanqui opened on Jun 5, 2026

MetaRocq.Translations.param_generous_packed is unimportable

Status: Open.

#1235 In MetaRocq/metarocq;

· JasonGross opened on Jan 25, 2026

λ-box pretty-printer giving incorrect names in mutual fixpoint

Status: Open.

#1182 In MetaRocq/metarocq;

· simon-dima opened on May 19, 2025

All_fold_app and All_fold_app_inv are swaped

Status: Open.

#1179 In MetaRocq/metarocq;

· thomas-lamiaux opened on May 7, 2025

Improve Quoting to also quote uniform parameters

Status: Open.

#1120 In MetaRocq/metarocq;

· thomas-lamiaux opened on Nov 21, 2024

Add a tmWarning

Status: Open.

#1119 In MetaRocq/metarocq;

· thomas-lamiaux opened on Nov 21, 2024

Improve printing functions of TemplateMonad

Status: Open.

#1118 In MetaRocq/metarocq;

· MathisBD opened on Nov 21, 2024

tmMkDefinition and friends discard the evar map

Status: Open.

#1115 In MetaRocq/metarocq;

· MathisBD opened on Nov 4, 2024

Using tmMkInductive and tmUnquote unpredictably crashes

Status: Open.

#1114 In MetaRocq/metarocq;

· MathisBD opened on Nov 4, 2024

Unquote Definition will normalize the term

Status: Open.

#1091 In MetaRocq/metarocq;

· WeituoDAI opened on Jun 24, 2024

coq-8.17 branch no longer builds on ocaml 4.11.2

Status: Open.

#1022 In MetaRocq/metarocq;

· JasonGross opened on Nov 30, 2023

MetaCoq is missing Hint Opaque

Status: Open.

#1004 In MetaRocq/metarocq;

· Janno opened on Nov 2, 2023