Commits

Branch selector

 master

User selector

SkySkimmer

Datepicker

All time

Commit History

Commits on Feb 9, 2023

• Tiny amount more code sharing in nametab

  SkySkimmer

  committed
  2c1e5c3

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

  SkySkimmer

  committed
  59917ef

Commits on Feb 8, 2023

• Genargs are not holes

  SkySkimmer

  committed
  22a76df

• Printer.pr_evgl_sign is only called on undefined evars

  SkySkimmer

  committed
  1cae388

Commits on Feb 7, 2023

• Fix canonical instance matching match terms in evarconv

  SkySkimmer

  committed
  fdb272c

• Overlay for changed Universe.pr

  SkySkimmer

  committed
  51d64b2

• Fix ppvernac on Goal: don't print an underscore for the missing name

  SkySkimmer

  committed
  740edb5

Commits on Feb 6, 2023

• Make univ binders argument of UnivNames.pr_with_global_universes optional

  SkySkimmer

  committed
  6afedb2

• Fix some universe name printing

  SkySkimmer

  committed
  78c3718

• ltac2 wit_ltac2 and with_ltac2_quotation printers: don't return garbage

  SkySkimmer

  committed
  38a0c2a

Commits on Feb 5, 2023

• Genintern.generic_substitute_notation is never passed Some constr_expr

  SkySkimmer

  committed
  db10b2f

Commits on Feb 3, 2023

• Update bench plotter

  SkySkimmer

  committed
  68d0f7b

• Fast path interleaved in conversion

  SkySkimmer

  committed
  fcadee7

Commits on Jan 27, 2023

• Expose some rel_context_val manipulation APIs in Environ

  SkySkimmer

  committed
  57152e6

• Use custom exception for "cannot coerce to an evaluable reference"

  SkySkimmer

  committed
  ec5def2

Commits on Jan 24, 2023

• Don't fail when printing a ltac2 name local to another module

  SkySkimmer

  committed
  15635d9

• Polymorphic maps

  SkySkimmer

  committed
  7e2dde1

Commits on Jan 23, 2023

• Changelog for grammar extend backtrack

  SkySkimmer

  committed
  2040a2c

• hack for elpi command extend

  SkySkimmer

  committed
  d3803c9

• Don't initialize tactic_value with trivial rules

  SkySkimmer

  committed
  6944732

• Don't initialize plugins multiple times without backtracking

  SkySkimmer

  committed
  839bbd1

• Fix backtracking over plugin vernac extensions

  SkySkimmer

  committed
  bd74bdc

• Add some doc comments on ltac2 equality APIs

  SkySkimmer

  committed
  993df1f

Commits on Jan 20, 2023

• make_case_or_project: don't produce heavy encoding for trivial match

  SkySkimmer

  committed
  2c90795

• Use custom exception for warn-as-error instead of user_err

  SkySkimmer

  committed
  99a61d6

• make-library-index: use mktemp, general cleanup

  SkySkimmer

  committed
  fbe9e28

Commits on Jan 17, 2023

• Overlay for functional grammar state

  SkySkimmer

  committed
  c68cb1a

• Grammar.safe_extend enforce that the keyword state is write only

  SkySkimmer

  committed
  02f6ca3

• Make the parser partial application lazy

  SkySkimmer

  committed
  be4afdc

• Functional lexer state access in streams

  SkySkimmer

  committed
  30ac124

• Move grammar state to pcoq

  SkySkimmer

  committed
  4c58474

• Mostly functionalize CLexer, move state ref to pcoq

  SkySkimmer

  committed
  941ef39

• Functional grammar access while parsing

  SkySkimmer

  committed
  d6ef8e3

• Remove mutable from grammar entries, use global map ref instead

  SkySkimmer

  committed
  061d532

• Split ssrparser to avoid stack overflow with flambda

  SkySkimmer

  committed
  9cc2d4d

Pagination

PreviousNext