Commits

Breadcrumbs

History for

onmaster

User selector

All users

Datepicker

All time

Commit History

Commits on Sep 10, 2024

• Merge PR coq#19310: Rename Coq requirement prefix to Stdlib

  Show description for 7fec4bd
  

  coqbot-app[bot]

  and

  silene

  authored
  7fec4bd

  Copy full SHA for 7fec4bd

Commits on Sep 9, 2024

• Renaming Coq -> Stdlib

  proux01

  committed
  2d5daee

  Copy full SHA for 2d5daee

Commits on Sep 5, 2024

• ncring_tac convert some matches to lazymatch

  SkySkimmer

  committed
  82a2e20

  Copy full SHA for 82a2e20

• Ncring_tac get ring operations before main loop instead of at each step

  SkySkimmer

  committed
  4db02e0

  Copy full SHA for 4db02e0

• Ncring_tac: avoid generating temporary pairs in main loop

  SkySkimmer

  committed
  275e895

  Copy full SHA for 275e895

• Ncring_tac: don't use pairs to handle extensibility

  SkySkimmer

  committed
  8bf2ee4

  Copy full SHA for 8bf2ee4

Commits on Jul 24, 2024

• Using the name Drinker Paradox for its exact original formulation.

  herbelin

  committed
  ea775bd

  Copy full SHA for ea775bd

• Clarify the strength of Independence of general premises.

  Show description for d1ef6ed
  herbelin

  committed
  d1ef6ed

  Copy full SHA for d1ef6ed

Commits on Jul 19, 2024

• done with simple refine

  Tragicus

  committed
  6bd95e0

  Copy full SHA for 6bd95e0

• Merge PR coq#19382: [ssr] Remove no longer used not_locked_false_eq_true

  Show description for aaa0c13
  

  coqbot-app[bot]

  and

  gares

  authored
  aaa0c13

  Copy full SHA for aaa0c13

• Merge PR coq#19372: improve done

  Show description for a6bba34
  

  coqbot-app[bot]

  and

  gares

  authored
  a6bba34

  Copy full SHA for a6bba34

• [ssr] Remove no longer used not_locked_false_eq_true

  proux01

  committed
  de8f034

  Copy full SHA for de8f034

Commits on Jul 17, 2024

• Merge PR coq#19373: Speedup proof of nzhead_revapp in DecimalFacts and HexadecimalFacts

  Show description for 93ef792
  

  coqbot-app[bot]

  and

  proux01

  authored
  93ef792

  Copy full SHA for 93ef792

• Merge PR coq#17560: Add reg theorems for nat on multiplication

  Show description for a1ddcf9
  

  coqbot-app[bot]

  and

  andres-erbsen

  authored
  a1ddcf9

  Copy full SHA for a1ddcf9

Commits on Jul 16, 2024

• Speedup proof of nzhead_revapp in DecimalFacts and HexadecimalFacts

  Show description for 6662246
  SkySkimmer

  committed
  6662246

  Copy full SHA for 6662246

• improve done

  Show description for dd069dd
  Tragicus

  committed
  dd069dd

  Copy full SHA for dd069dd

Commits on Jul 15, 2024

• Remove the last use of FunInd from FMapFullAVL.

  Show description for e27b21d
  ppedrot

  committed
  e27b21d

  Copy full SHA for e27b21d

Commits on Jul 9, 2024

• Inline calls to Functional Scheme in MSetAVL.

  ppedrot

  committed
  6669123

  Copy full SHA for 6669123

Commits on Jul 5, 2024

• Merge PR coq#19312: Inline calls to Functional Scheme in FMapAVL.

  Show description for e24ab64
  

  coqbot-app[bot]

  and

  proux01

  authored
  e24ab64

  Copy full SHA for e24ab64

Commits on Jul 4, 2024

• Split the nsatz plugin into a core package and an Ltac1 syntax.

  ppedrot

  committed
  784af83

  Copy full SHA for 784af83

• Split the firstorder plugin into a core package and an Ltac1 syntax.

  ppedrot

  committed
  2ffdf62

  Copy full SHA for 2ffdf62

• Split the cc plugin into a core package and an Ltac1 syntax.

  ppedrot

  committed
  270eb2b

  Copy full SHA for 270eb2b

Commits on Jul 3, 2024

• Inline calls to Functional Scheme in FMapAVL.

  ppedrot

  committed
  a8ee67a

  Copy full SHA for a8ee67a

Commits on Jun 25, 2024

• Update theories/Vectors/VectorSpec.v

  Show description for c938f5f
  

  drenched-moth

  and

  Villetaneuse

  authored
  c938f5f

  Copy full SHA for c938f5f

• Update theories/Vectors/VectorSpec.v

  Show description for 22049a2
  

  drenched-moth

  and

  Villetaneuse

  authored
  22049a2

  Copy full SHA for 22049a2

Commits on Jun 24, 2024

• Proof should work with the existing dependencies now

  

  Lucas Donati

  committed
  d584f94

  Copy full SHA for d584f94

• Proof update, no longer using dependent induction

  

  Lucas Donati

  committed
  ee80a74

  Copy full SHA for ee80a74

• adding lemma and proof

  

  Lucas Donati

  committed
  f050af8

  Copy full SHA for f050af8

Commits on Jun 17, 2024

• Bump version (8.21+alpha)

  proux01

  committed
  cb68879

  Copy full SHA for cb68879

Commits on Jun 13, 2024

• Statically enforce primitive string size invariant.

  Show description for a5d9d6c
  rlepigre

  committed
  a5d9d6c

  Copy full SHA for a5d9d6c

• Specification of [list_compare] with an inductive.

  Show description for 4b80e20
  

  rlepigre

  and

  Jan-Oliver Kaiser

  committed
  4b80e20

  Copy full SHA for 4b80e20

• Add some theory around primitive strings.

  rlepigre

  committed
  8732467

  Copy full SHA for 8732467

• Add extraction support.

  rlepigre

  committed
  eef50df

  Copy full SHA for eef50df

• Add a primitive string type.

  rlepigre

  committed
  15c0443

  Copy full SHA for 15c0443

Commits on Jun 1, 2024

• Merge PR coq#19115: Use Coqlib for setoid_rewrite

  Show description for 7f437c3
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  7f437c3

  Copy full SHA for 7f437c3

Pagination

Previous

Next