Commits

Branch selector

 master

User selector

All users

Datepicker

All time

Commit History

Commits on Mar 6, 2024

• Merge PR #18032: [stdlib] Warn about Vector.v

  Show description for 26fbe83
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  26fbe83

  Copy full SHA for 26fbe83

Commits on Mar 5, 2024

• Merge PR #18690: Ltac2: add numgoals API and a bunch of tests for Control

  Show description for 5dcfab5
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  5dcfab5

  Copy full SHA for 5dcfab5

• Merge PR #18746: Add test for #9937

  Show description for 1997f69
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  1997f69

  Copy full SHA for 1997f69

• Merge PR #18738: test-suite: speed up report script

  Show description for 792a269
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  792a269

  Copy full SHA for 792a269

• Merge PR #18748: Applying universes restriction in Program Fixpoint

  Show description for 615f0bb
  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  615f0bb

  Copy full SHA for 615f0bb

• Merge PR #18692: Remove the Lforce node from the generic lambda AST.

  Show description for 0c88f61
  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  0c88f61

  Copy full SHA for 0c88f61

• Merge PR #18741: Fixes an anomaly with interactive Fixpoint without arguments

  Show description for ef8e8c6
  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  ef8e8c6

  Copy full SHA for ef8e8c6

• Merge PR #18745: Cleanup internal API of Micromega

  Show description for 686b20b
  

  coqbot-app[bot]

  and

  fajb

  authored
  686b20b

  Copy full SHA for 686b20b

Commits on Mar 4, 2024

• Fix an anomaly with interactive Fixpoint.

  herbelin

  committed
  da62019

  Copy full SHA for da62019

• Restricting universes in Program Fixpoint.

  Show description for e689b3b
  herbelin

  committed
  e689b3b

  Copy full SHA for e689b3b

• Merge PR #18693: Ltac profile: automatically adapt printing width

  Show description for 08de550
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  08de550

  Copy full SHA for 08de550

• Add test for #9937

  Show description for 1dce0bd
  SkySkimmer

  committed
  1dce0bd

  Copy full SHA for 1dce0bd

• Merge PR #18739: Fixes "where notation" clause of interactive Fixpoint

  Show description for 4c4de1c
  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  4c4de1c

  Copy full SHA for 4c4de1c

• Correctly classify lazy definitions native compilation.

  Show description for ecc9102
  ppedrot

  committed
  ecc9102

  Copy full SHA for ecc9102

• Correctly handle lazy constants in native compilation.

  Show description for bab9393
  ppedrot

  committed
  bab9393

  Copy full SHA for bab9393

• Remove the Lforce node from the generic lambda AST.

  Show description for 4e112d4
  ppedrot

  committed
  4e112d4

  Copy full SHA for 4e112d4

• Merge PR #16329: Issue #16262: do not override generic format if not reserved and only printing

  Show description for c9fa714
  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  c9fa714

  Copy full SHA for c9fa714

• Merge PR #18725: About and Print inform about projections

  Show description for 2979ebe
  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  2979ebe

  Copy full SHA for 2979ebe

• Simplex.integer_solver takes a WithProof.t list.

  Show description for fcdaddd
  ppedrot

  committed
  fcdaddd

  Copy full SHA for fcdaddd

• Specialize WithProof.mult to a constant variant in Micromega.

  Show description for 295c6d8
  ppedrot

  committed
  295c6d8

  Copy full SHA for 295c6d8

• Directly compute environments in Micromega certificates.

  Show description for 03571bf
  ppedrot

  committed
  03571bf

  Copy full SHA for 03571bf

• Inline static calls in Certificate.xlia.

  ppedrot

  committed
  b151a97

  Copy full SHA for b151a97

• Hide the WithProof type implementation in the Micromega API.

  ppedrot

  committed
  e364f82

  Copy full SHA for e364f82

• Ltac2 test suite: add basic tests for Control externals

  SkySkimmer

  committed
  27f0002

  Copy full SHA for 27f0002

• Ltac2: add numgoals API

  Show description for 868e5fd
  SkySkimmer

  committed
  868e5fd

  Copy full SHA for 868e5fd

Commits on Mar 3, 2024

• Merge PR #18712: Cs refactoring

  Show description for 9fdbaae
  

  coqbot-app[bot]

  and

  proux01

  authored
  9fdbaae

  Copy full SHA for 9fdbaae

• Refactor check_conv_record in evarconv.ml

  Show description for 292ed7a
  

  3 peopleauthored and

  proux01

  committed
  292ed7a

  Copy full SHA for 292ed7a

Commits on Mar 2, 2024

• Fixes "where notation" clause of interactive Fixpoint.

  herbelin

  committed
  ea99487

  Copy full SHA for ea99487

• Move the "where" notations associated to a declaration in the Declare.Info data.

  herbelin

  committed
  de276a5

  Copy full SHA for de276a5

• Change log for #18725

  herbelin

  committed
  037debc

  Copy full SHA for 037debc

• Add "as" clause in Record's printing.

  herbelin

  committed
  cb674a1

  Copy full SHA for cb674a1

• Export a function returning the canonical inhabitant name of a record.

  herbelin

  committed
  25d6e7e

  Copy full SHA for 25d6e7e

• Display projections in Print.

  herbelin

  committed
  2ab364d

  Copy full SHA for 2ab364d

• test-suite: speed up report script

  Show description for 4fb86d1
  SkySkimmer

  committed
  4fb86d1

  Copy full SHA for 4fb86d1

Commits on Mar 1, 2024

• Merge PR #18705: Don't make too many coercions reversible by default

  Show description for 139b6ce
  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  139b6ce

  Copy full SHA for 139b6ce

Pagination

Previous

Next