GitHub · Where software is built

8000 GitHub · Where software is built

More Web Proxy on the site http://driver.im/

Labels Milestones New issue

Typo in ErasurePlugin.Erasure.default_unsafe_passes comment

#1189

· simon-dima opened

on Jun 25, 2025

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

#1182

· simon-dima opened

on May 19, 2025

All_fold_app and All_fold_app_inv are swaped

#1179

· thomas-lamiaux opened

on May 7, 2025

Improve Quoting to also quote uniform parameters

#1120

· thomas-lamiaux opened

on Nov 21, 2024

Add a tmWarning

#1119

· thomas-lamiaux opened

on Nov 21, 2024

Improve printing functions of <code>TemplateMonad</code>

#1118

· MathisBD opened

on Nov 21, 2024

<code>tmMkDefinition</code> and friends discard the evar map

#1115

· MathisBD opened

on Nov 4, 2024

Using tmMkInductive and tmUnquote unpredictably crashes

#1114

· MathisBD opened

on Nov 4, 2024

Universe level error when defining dependent types in one metacoq call.

#1108

· DeLectionnes opened

on Oct 25, 2024

<code>Unquote Definition</code> will normalize the term

#1091

· WeituoDAI opened

on Jun 24, 2024

coq-8.17 branch no longer builds on ocaml 4.11.2

#1022

· JasonGross opened

on Nov 30, 2023

MetaCoq is missing <code>Hint Opaque</code>

#1004

· Janno opened

on Nov 2, 2023

0