Commits

Branch selector

 master

User selector

coqbot-app[bot]

Datepicker

All time

Commit History

Commits on Sep 13, 2024

• Merge PR coq#19542: Fix all uses of instantiate_context

  Show description for 48db236
  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  48db236

  Copy full SHA for 48db236

• Merge PR coq#19394: Take RRs more into account for unification

  Show description for 64fea30
  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  64fea30

  Copy full SHA for 64fea30

• Merge PR coq#19532: Improve boxing in rewrite-rules-break-SR warning + add rewrite-rules warning category

  Show description for 2e78ca4
  

  coqbot-app[bot]

  and

  proux01

  authored
  2e78ca4

  Copy full SHA for 2e78ca4

• Merge PR coq#19522: Encourage use of metalanguages rather than plugin

  Show description for 30f5ad0
  

  coqbot-app[bot]

  and

  jfehrle

  authored
  30f5ad0

  Copy full SHA for 30f5ad0

Commits on Sep 12, 2024

• Merge PR coq#19475: Add example of "discriminate" limitation (it doesn't handle impossible equations such as n = (S n)

  Show description for f9d9e51
  

  coqbot-app[bot]

  and

  proux01

  authored
  f9d9e51

  Copy full SHA for f9d9e51

• Merge PR coq#19518: Update CI policy: adding libraries should be justified + minor cleanups

  Show description for e313e6a
  

  coqbot-app[bot]

  and

  proux01

  authored
  e313e6a

  Copy full SHA for e313e6a

• Merge PR coq#19521: Rename some coqchk files

  Show description for d2d2e00
  

  coqbot-app[bot]

  and

  proux01

  authored
  d2d2e00

  Copy full SHA for d2d2e00

Commits on Sep 11, 2024

• Merge PR coq#19525: template_polymorphism_candidate: forbid levels appearing in indices

  Show description for 44155b0
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  44155b0

  Copy full SHA for 44155b0

• Merge PR coq#19513: Fix -profile with par:, pass profiling data back to main thread and add profile entries for par: steps

  Show description for a37a2e4
  

  coqbot-app[bot]

  and

  gares

  authored
  a37a2e4

  Copy full SHA for a37a2e4

• Merge PR coq#19426: Factorize handling of control flags between synterp and interp + use control flags in stm close_proof calls

  Show description for 818fc99
  

  coqbot-app[bot]

  and

  gares

  authored
  818fc99

  Copy full SHA for 818fc99

Commits on Sep 10, 2024

• Merge PR coq#19509: Compare projections by repr name in RRs

  Show description for ce1cbe6
  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  ce1cbe6

  Copy full SHA for ce1cbe6

• 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

• Merge PR coq#19516: [CI] FCSL-pcm now depends on MathComp 2

  Show description for cc6786a
  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  cc6786a

  Copy full SHA for cc6786a

• Merge PR coq#19228: Do not create global constraints for applied template polymorphic types

  Show description for 3a19736
  

  coqbot-app[bot]

  and

  mattam82

  authored
  3a19736

  Copy full SHA for 3a19736

• Merge PR coq#19428: Add -profile support for coqchk

  Show description for 418501a
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  418501a

  Copy full SHA for 418501a

Commits on Sep 6, 2024

• Merge PR coq#19501: Ncring_tac: avoid generating temporary pairs in main loop

  Show description for 1b98a2f
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  1b98a2f

  Copy full SHA for 1b98a2f

• Merge PR coq#19410: Fix documentation for el_shft and fix lift_subst

  Show description for 2c64de2
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  2c64de2

  Copy full SHA for 2c64de2

• Merge PR coq#19495: Clean up the ring tactic protection algorithm

  Show description for 9ac7ab4
  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  9ac7ab4

  Copy full SHA for 9ac7ab4

• Merge PR coq#19494: Removes calls and definitions of unsafe constr API around Evarutil

  Show description for 60e2416
  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  60e2416

  Copy full SHA for 60e2416

Commits on Sep 5, 2024

• Merge PR coq#19031: A common execution path for universe restriction + universe declaration check

  Show description for 9c1e8bd
  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  9c1e8bd

  Copy full SHA for 9c1e8bd

• Merge PR coq#19473: Typeclasses default mode

  Show description for 7d5ef7c
  

  coqbot-app[bot]

  and

  gares

  authored
  7d5ef7c

  Copy full SHA for 7d5ef7c

Commits on Sep 4, 2024

• Merge PR coq#19441: coqchk accept absolute vo paths

  Show description for fa5011d
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  fa5011d

  Copy full SHA for fa5011d

• Merge PR coq#19472: [CI] Remove one more dependency to MathComp 1

  Show description for b558a43
  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  b558a43

  Copy full SHA for b558a43

• Merge PR coq#19476: Rely on the HConstr machinery also for opaque proofs containing side-effects

  Show description for d72fa37
  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  d72fa37

  Copy full SHA for d72fa37

• Merge PR coq#19378: "make world" and dune default target don't build coqide

  Show description for e0ac59a
  

  coqbot-app[bot]

  and

  proux01

  authored
  e0ac59a

  Copy full SHA for e0ac59a

Commits on Sep 3, 2024

• Merge PR coq#19437: Reduce the amount of typechecking in Ssrequality.

  Show description for 43cec46
  

  coqbot-app[bot]

  and

  gares

  authored
  43cec46

  Copy full SHA for 43cec46

• Merge PR coq#19281: Changelog for 8.20

  Show description for fa2dce5
  

  coqbot-app[bot]

  and

  silene

  authored
  fa2dce5

  Copy full SHA for fa2dce5

• Merge PR coq#19493: Protecting against Not_found in "use" option of deprecation attribute

  Show description for 0d5d357
  

  coqbot-app[bot]

  and

  gares

  authored
  0d5d357

  Copy full SHA for 0d5d357

• Merge PR coq#19450: Cleanup checker/values after removal of vio

  Show description for 6ecd029
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  6ecd029

  Copy full SHA for 6ecd029

• Merge PR coq#19489: Fix ltac2 unused variable checking for repeated name in binder list

  Show description for a4604d8
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  a4604d8

  Copy full SHA for a4604d8

• Merge PR coq#19491: Fix equality testing of univ instances in constrexpr

  Show description for 1fe97bc
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  1fe97bc

  Copy full SHA for 1fe97bc

Commits on Sep 2, 2024

• Merge PR coq#19492: votour add vmlibrary to known segments

  Show description for 914a38a
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  914a38a

  Copy full SHA for 914a38a

• Merge PR coq#19296: Fixes coq#7913: fixpoint with decreasing argument hidden behind a definition

  Show description for 035b56a
  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  035b56a

  Copy full SHA for 035b56a

• Merge PR coq#19363: Fix incorrect error locations with } in coqtop

  Show description for ad6c007
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  ad6c007

  Copy full SHA for ad6c007

• Merge PR coq#19431: Do not evar normalize potential hints in TC local database construction.

  Show description for 7e7de62
  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  7e7de62

  Copy full SHA for 7e7de62

Pagination

Previous

Next