Commits

Branch selector

 master

User selector

All users

Datepicker

All time

Commit History

Commits on Feb 15, 2023

• Merge PR coq#17254: [coqdoc] Add links for existing instances

  

  coqbot-app[bot]

  and

  silene

  authored
  8e03144

Commits on Feb 14, 2023

• Merge PR coq#16937: Fixes coq#12467: internal inconsistency when a notation variable is used both for binder lists and for term lists

  

  coqbot-app[bot]

  and

  proux01

  authored
  f66b58c

• Dump glob for Existing Instance and Existing Class

  proux01

  committed
  b998ee4

• Renaming AsNameOrPattern into AsAnyPattern to better reflect the role.

  herbelin

  committed
  1479f9e

• Merge PR coq#17257: Revert coq#15130 as it causes test-suite failures for coqdoc to be silently ignored (fix coq#17256).

  

  coqbot-app[bot]

  and

  proux01

  authored
  585b309

• Revert coq#15130 as it causes test-suite failures for coqdoc to be silently ignored (fix coq#17256).

  silene

  committed
  bd7f2cb

• Notations: adding printing support for assumptions parsed as constr.

  herbelin

  committed
  e3ca00d

• Fixing classification bug for detection of recursive binders in notations.

  herbelin

  committed
  8f237c4

• Overlay for serapi

  herbelin

  committed
  d8980ea

• Adding change log for coq#16937.

  herbelin

  committed
  7520c7b

• Egramcoq: Cosmetic changes, reordering pattern-matching clauses.

  herbelin

  committed
  49052e0

• Adding code to parse and print binder lists made of ident, name or patterns.

  herbelin

  committed
  507563b

• Notations: factorizing the computation of the default level of pattern entry.

  herbelin

  committed
  c9ef51b

• Notations: reorganizing the conversion between parsing types and interp types.

  herbelin

  committed
  9b5d3a6

Commits on Feb 11, 2023

• Merge PR coq#17206: Fix canonical instance matching match terms in evarconv

  

  coqbot-app[bot]

  and

  gares

  authored
  1556881

• Merge PR coq#17247: Tiny amount more code sharing in nametab

  

  coqbot-app[bot]

  and

  ppedrot

  authored
  18567e7

• Merge PR coq#17249: swap sval and @sval notations

  

  coqbot-app[bot]

  and

  gares

  authored
  6efadc5

Commits on Feb 10, 2023

• Merge PR coq#17250: Move the evar clause API out of Clenv.

  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  c1bf187

• Merge PR coq#17239: Drop the abstract argument field from defined evars.

  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  c3a3d0e

• Merge PR coq#17148: Fixing syntax error reporting in the presence of token lookahead

  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  7091c5e

• swap sval and @sval notations

  affeldt-aist

  committed
  12ddae0

• Merge PR coq#17237: Minor fixes of relevance around evar-generating code

  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  485620a

• Move the evar clause API out of Clenv.

  ppedrot

  committed
  2e276dd

• Merge PR coq#17220: Genargs are not holes

  

  coqbot-app[bot]

  and

  ppedrot

  authored
  17861fe

Commits on Feb 9, 2023

• Tiny amount more code sharing in nametab

  SkySkimmer

  committed
  2c1e5c3

• Further improving syntax error reporting in the presence of lookahead.

  herbelin

  committed
  be6d234

• Improving syntax error reporting in the presence of lookahead.

  herbelin

  committed
  1e9cfab

• Merge PR coq#17241: Add CI target for coq-library-undecidability

  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  fbe061d

• Merge PR coq#17217: Fixes coq#14975: anomaly with notations abbreviating a local variable or field name

  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  a53ed9e

• Merge PR coq#17244: Dockerfile flambda switch: add "uri" for coq-lsp

  

  coqbot-app[bot]

  and

  ejgallego

  authored
  9511f29

• Merge PR coq#17171: Fix ppvernac on Goal: don't print an underscore for the missing name

  

  coqbot-app[bot]

  and

  Alizter

  authored
  e536726

• Merge PR coq#17177: Fix some universe name printing

  

  coqbot-app[bot]

  and

  Alizter

  authored
  270d080

• Update dev/ci/ci-coq_library_undecidability.sh

  

  yforster

  and

  SkySkimmer

  authored
  3140c94

• Dockerfile flambda switch: add "uri" for coq-lsp

  SkySkimmer

  committed
  59917ef

• add CI target for coq-library-undecidability

  yforster

  committed
  5de7abe

Pagination

PreviousNext