plugins · coq · Tangled

forked from coq/coq

coq plugins

17 folders

coqbot-app[bot] · Merge PR #22641: Fix OCaml extraction callbacks for recursive functions · 2w ago

Merge PR #22074: Remove more global lazys

Remove Constr.eq_constr_nounivs.

Merge PR #21987: Keep track of which variables are section variables and use this info to fix bugs

Fix OCaml extraction callbacks for recursive functions

Merge PR #22074: Remove more global lazys

Use the now correct set and maps Names APIs.

[ssreflect] Accept `tac; [tac|...|tac] => intro` syntax

Use the now correct set and maps Names APIs.

Remove compat coq-core libraries (not executables)

Abstract away the Summary reference type.

Merge PR #22074: Remove more global lazys

Use the now correct set and maps Names APIs.

Merge PR #21955: Remove compat coq-core libraries (not executables)

ssr: replace universe state unions by set_ustate when extending

Turn notation into a record

Abstract away the Summary reference type.

Remove Constr.eq_constr_nounivs.