Commits

Branch selector

 a4604d8

User selector

All users

Datepicker

All time

Commit History

Commits on Sep 3, 2024

• 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

• votour add vmlibrary to known segments

  SkySkimmer

  committed
  36e7ce3

  Copy full SHA for 36e7ce3

• Fix equality testing of univ instances in constrexpr

  Show description for f79b990
  SkySkimmer

  committed
  f79b990

  Copy full SHA for f79b990

• 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

• Merge PR coq#19481: Allow fast fresh name generation in detyping

  Show description for b151008
  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  b151008

  Copy full SHA for b151008

• Merge PR coq#19446: Reduce the Typeops API.

  Show description for 11aec05
  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  11aec05

  Copy full SHA for 11aec05

• Fix ltac2 unused variable checking for repeated name in binder list

  Show description for c379797
  SkySkimmer

  committed
  c379797

  Copy full SHA for c379797

• Ltac2 check_unused_variables take name list instead of polymorphic list

  SkySkimmer

  committed
  8963509

  Copy full SHA for 8963509

Commits on Aug 30, 2024

• Adding overlays.

  ppedrot

  committed
  ea63d52

  Copy full SHA for ea63d52

• Unconditionally use the fresh mechanism in detyping.

  Show description for 9b0cd9a
  ppedrot

  committed
  9b0cd9a

  Copy full SHA for 9b0cd9a

• Actually use the new fast map API in Detyping.

  ppedrot

  committed
  f3b077c

  Copy full SHA for f3b077c

• Add an API to get the maximal element map of fresh names.

  ppedrot

  committed
  87db195

  Copy full SHA for 87db195

• Generalize detyping and externalization w.r.t. a name generator.

  ppedrot

  committed
  31e55e1

  Copy full SHA for 31e55e1

• Generalize the implementation of fresh name generation.

  Show description for 5aef7c2
  ppedrot

  committed
  5aef7c2

  Copy full SHA for 5aef7c2

Commits on Aug 27, 2024

• Merge PR coq#19474: Tweak formatting of "Print HintDb" output

  Show description for 9ed5a0f
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  9ed5a0f

  Copy full SHA for 9ed5a0f

• Merge PR coq#19092: Better integration of Derive in declare.ml + fix of coq#18951

  Show description for 6a2431e
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  6a2431e

  Copy full SHA for 6a2431e

• Merge PR coq#18575: Clarify the status of the independence of general premises in file ClassicalFacts.v

  Show description for 8f4f3bd
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  8f4f3bd

  Copy full SHA for 8f4f3bd

• Merge PR coq#19429: coqchk understand sharing when validating

  Show description for 6e43e3e
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  6e43e3e

  Copy full SHA for 6e43e3e

• Tweak formatting of "Print HintDb" output

  jfehrle

  committed
  f19098b

  Copy full SHA for f19098b

Commits on Aug 22, 2024

• Merge PR coq#19409: Bench: don't print CPU cycles in table

  Show description for 3421892
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  3421892

  Copy full SHA for 3421892

Commits on Aug 14, 2024

• Merge PR coq#19463: [CI] Revert "Mark jasmin as allow_failure"

  Show description for d6550d1
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  d6550d1

  Copy full SHA for d6550d1

Commits on Aug 13, 2024

• Revert "[CI] Mark jasmin as allow_failure"

  Show description for 002b877
  proux01

  committed
  002b877

  Copy full SHA for 002b877

Commits on Aug 12, 2024

• Merge PR coq#19323: add table of locality attributes in refman

  Show description for 77ae011
  

  coqbot-app[bot]

  and

  jfehrle

  authored
  77ae011

  Copy full SHA for 77ae011

• Merge PR coq#19417: CoqIDE: Improve preferences dialog

  Show description for 005f17a
  

  coqbot-app[bot]

  and

  jfehrle

  authored
  005f17a

  Copy full SHA for 005f17a

Commits on Aug 10, 2024

• Add changelog for PR 19417

  Frigory33

  committed
  5597e55

  Copy full SHA for 5597e55

• CoqIDE documentation: update content; add and update a few pictures

  Frigory33

  committed
  19ad0fc

  Copy full SHA for 19ad0fc

• coqide preferences: Make indentation of sections more visible with spaces

  Frigory33

  committed
  7ee0a3c

  Copy full SHA for 7ee0a3c

• Change the name of the Coq style (CoqIDE color scheme)

  Frigory33

  committed
  a7bef73

  Copy full SHA for a7bef73

• coqide: Add preference for unjustified conclusions’ background color

  Frigory33

  committed
  0b8ee14

  Copy full SHA for 0b8ee14

• coqide: Rework preferences dialog

  Show description for ac6aabe
  Frigory33

  committed
  ac6aabe

  Copy full SHA for ac6aabe

Commits on Aug 9, 2024

• Merge PR coq#19433: Hconstr tweak debug and profile printing

  Show description for 94f1d83
  

  coqbot-app[bot]

  and

  ppedrot

  authored
  94f1d83

  Copy full SHA for 94f1d83

Pagination

Previous

Next