Commits

Branch selector

 master

User selector

All users

Datepicker

All time

Commit History

Commits on Nov 20, 2024

• Merge PR #19852: Fix stdlib proofs to work with strict focusing

  Show description for da4e34b
  

  coqbot-app[bot]

  and

  olaure01

  authored
  da4e34b

  Copy full SHA for da4e34b

• Merge PR #19831: When a record cannot be declared with primitive projections, explain why

  Show description for d1a5a7f
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  d1a5a7f

  Copy full SHA for d1a5a7f

• Merge PR #19849: Use Vars.substituend in CClosure.comp_subs

  Show description for 6904212
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  6904212

  Copy full SHA for 6904212

Commits on Nov 19, 2024

• Fix stdlib proofs to work with strict focusing

  SkySkimmer

  committed
  4700851

  Copy full SHA for 4700851

• Merge PR #19847: Remove the unused PATTERNIDENT token.

  Show description for 3f251ce
  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  3f251ce

  Copy full SHA for 3f251ce

• Merge PR #19848: Add test for template poly extracted from mtac2

  Show description for d07ba35
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  d07ba35

  Copy full SHA for d07ba35

• Merge PR #19845: Fix binder factorization when implicit status differ

  Show description for 172b30b
  

  coqbot-app[bot]

  and

  proux01

  authored
  172b30b

  Copy full SHA for 172b30b

Commits on Nov 18, 2024

• Merge PR #19795: add_field: pass pre/post arguments down to add_ring

  Show description for 668dc3c
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  668dc3c

  Copy full SHA for 668dc3c

• Merge PR #19826: Coqinit split init_runtime to better support having multiple docs

  Show description for 15f9258
  

  coqbot-app[bot]

  and

  gares

  authored
  15f9258

  Copy full SHA for 15f9258

• Merge PR #19611: Evarconv: save keys

  Show description for fa6d92d
  

  coqbot-app[bot]

  and

  gares

  authored
  fa6d92d

  Copy full SHA for fa6d92d

• Merge PR #19844: Typeops.type_of_apply fix empty stack check

  Show description for fffbf85
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  fffbf85

  Copy full SHA for fffbf85

• prevent solving reducible and ground CS problems + save keys + LHS unfolding

  Tragicus

  committed
  e2fd033

  Copy full SHA for e2fd033

• Use Vars.substituend in CClosure.comp_subs

  SkySkimmer

  committed
  387cc3b

  Copy full SHA for 387cc3b

• Merge PR #19837: CClosure.to_constr does not take a univ instance

  Show description for e8793b2
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  e8793b2

  Copy full SHA for e8793b2

• Add test for template poly extracted from mtac2

  Show description for 966cecd
  SkySkimmer

  committed
  966cecd

  Copy full SHA for 966cecd

• Remove the unused PATTERNIDENT token.

  ppedrot

  committed
  4ffd7f6

  Copy full SHA for 4ffd7f6

• Fix binder factorization when implicit status differ

  Show description for d42ac00
  SkySkimmer

  committed
  d42ac00

  Copy full SHA for d42ac00

• When a record cannot be declared with primitive projections, explain why

  SkySkimmer

  committed
  397c560

  Copy full SHA for 397c560

• Merge PR #19832: Reduce the exposed attack surface of meta states

  Show description for 6b03a41
  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  6b03a41

  Copy full SHA for 6b03a41

• Typeops.type_of_apply fix empty stack check

  Show description for 1c1a6a8
  SkySkimmer

  committed
  1c1a6a8

  Copy full SHA for 1c1a6a8

Commits on Nov 16, 2024

• CClosure.to_constr does not take a univ instance

  Show description for b3ed51f
  SkySkimmer

  committed
  b3ed51f

  Copy full SHA for b3ed51f

Commits on Nov 15, 2024

• Merge PR #19834: Stop implicitly adding the current directory to ML paths

  Show description for 4923ec0
  

  coqbot-app[bot]

  and

  ejgallego

  authored
  4923ec0

  Copy full SHA for 4923ec0

• Merge PR #19835: Stop adding coq-core/plugins subdirs to ml loadpath

  Show description for a87553c
  

  coqbot-app[bot]

  and

  ejgallego

  authored
  a87553c

  Copy full SHA for a87553c

• Merge PR #19836: MacOS CI: install pkgconf instead of pkg-config

  Show description for 671f84d
  

  coqbot-app[bot]

  and

  proux01

  authored
  671f84d

  Copy full SHA for 671f84d

• Coqinit split init_runtime to better support having multiple docs

  Show description for 840ae45
  SkySkimmer

  committed
  840ae45

  Copy full SHA for 840ae45

• MacOS CI: install pkgconf

  Show description for 1ee9146
  SkySkimmer

  committed
  1ee9146

  Copy full SHA for 1ee9146

• Stop implicitly adding the current directory to ML paths

  Show description for 2a92515
  SkySkimmer

  committed
  2a92515

  Copy full SHA for 2a92515

• Stop adding coq-core/plugins subdirs to ml loadpath

  Show description for 73bd9b1
  SkySkimmer

  committed
  73bd9b1

  Copy full SHA for 73bd9b1

Commits on Nov 14, 2024

• Merge PR #19827: Declare ML Module allow plugin names not containing `.`

  Show description for ac0fd36
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  ac0fd36

  Copy full SHA for ac0fd36

• Merge PR #19830: CI: add elpi as dependency for CoRN

  Show description for 8dd4231
  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  8dd4231

  Copy full SHA for 8dd4231

Commits on Nov 13, 2024

• Move some meta-related APIs from Unification to Unification.Meta.

  ppedrot

  committed
  d14ae21

  Copy full SHA for d14ae21

• Stop constructing freelisted elements outside of Unification.

  ppedrot

  committed
  b175f9d

  Copy full SHA for b175f9d

• Move the fast path of meta_instance to the caller.

  ppedrot

  committed
  21d7149

  Copy full SHA for 21d7149

• CI: add elpi as dependency for CoRN

  MSoegtropIMC

  committed
  5e10635

  Copy full SHA for 5e10635

• Remove essentially unused meta API from Unification.

  ppedrot

  committed
  aa09262

  Copy full SHA for aa09262

Pagination

Previous

Next