Overview

19 Pull requests merged by4 people

• Small algorithmic enhancements in variable clearing

  #20374 mergedMar 20, 2025

• Do not call recursively self on subterm strategy.

  #20338 mergedMar 20, 2025

• dune-dbg don't declare rocqide_main.bc as a dependency

  #20372 mergedMar 20, 2025

• Search: don't search local defs (unless Unset Search Blacklist Locals)

  #20349 mergedMar 19, 2025

• [9.0] Bump Stdlib to V9.0.0

  #20353 mergedMar 19, 2025

• notation_subst keep track of actually used variables

  #20313 mergedMar 19, 2025

• coqpp: set location annotation when exiting user-provided code

  #20339 mergedMar 18, 2025

• Add relocatable mode

  #19901 mergedMar 18, 2025

• Small simplification in debug_print_modtab

  #20365 mergedMar 18, 2025

• Don't hcons in place in univ instances

  #20367 mergedMar 18, 2025

• TimeFileMaker put filename in the last column

  #20366 mergedMar 18, 2025

• Cleanup univ.ml(i) (remove some aliases, move hcons functions)

  #20360 mergedMar 18, 2025

• Remove unused Nametab.Modules API

  #20368 mergedMar 18, 2025

• Tweaks around memory consumption of Nametab

  #20364 mergedMar 17, 2025

• Enforce that cached include objects are properly expanded.

  #20362 mergedMar 17, 2025

• Constr and HConstr: stop hashconsing in place

  #20351 mergedMar 17, 2025

• Expand deprecation notice in Constr.v

  #20363 mergedMar 15, 2025

• Projection unfolded flag hashif b then 0 else 1 ->if b then 1 else 0

  #20358 mergedMar 14, 2025

• Hashconsing try to avoid recomputing hashes

  #20344 mergedMar 14, 2025

6 Pull requests opened by3 people

• Share code for delayed marshal between vmlibrary and library

  #20359 openedMar 14, 2025

• example simplification for bidirectionality hints in refman #12102

  #20370 openedMar 18, 2025

• Use full_path for absolute paths more consistently

  #20371 openedMar 18, 2025

• Remove the ability to declare arbitrary terms as hints.

  #20373 openedMar 19, 2025

• Delete test-suite/coq-makefile/timing-per-line

  #20375 openedMar 20, 2025

• Improve Boot.Env API and callers

  #20376 openedMar 20, 2025

6 Issues closed by2 people

• Notation - % vs %_

  #20377 closedMar 20, 2025

• Some Ltac2 notations incur exponential performance overhead when nested

  #20305 closedMar 19, 2025

• "Missing notation term for variables" should be an environment restriction at notation definition time

  #17833 closedMar 19, 2025

• "The variable Notation variable x is not available was not found in the current environment." should be more informative

  #20188 closedMar 19, 2025

• Make the build more relocatable to make the dune cache useful across worktrees

  #19900 closedMar 18, 2025

• The reference manual should document which environment variables are necessary to get a working coq

  #17158 closedMar 18, 2025

1 Issue opened by1 person

• Customize autogenerated variable names

  #20369 openedMar 17, 2025

11 Unresolved conversations

Sometimes conversations happen on old items that aren’t yet closed. Here is a list of all the Issues and Pull Requests with unresolved conversations.

• Add #[refine] attribute for Definition

  #20355 commented onMar 20, 2025 • 1 new comment

• [refman] Improve Corelib documentation

  #20356 commented onMar 14, 2025 • 1 new comment

• Help with docker-coq/docker-mathcomp rebuilds: looking for a volunteer

  #19306 commented onMar 14, 2025 • 0 new comments

• potentially unintuitive behavior of Include when defining a Module Type should be documented

  #20346 commented onMar 15, 2025 • 0 new comments

• coqc --help sends its output on stderr and not on stdout

  #20331 commented onMar 17, 2025 • 0 new comments

• Need a better example of bidirectionality hints

  #12102 commented onMar 18, 2025 • 0 new comments

• Obligations, Proof, Hint Extern, tactic option commands do not depend on ltac1

  #19690 commented onMar 20, 2025 • 0 new comments

• Provide a way to associate a name with a `Hint Extern`

  #19824 commented onMar 18, 2025 • 0 new comments

• Remove automatic adding of coqbin to PATH on windows in envars

  #20191 commented onMar 18, 2025 • 0 new comments

• test ocaml/ocaml#13861 (Gc.ramp_up)

  #20350 commented onMar 20, 2025 • 0 new comments

• Experiment with Marshal.static_from_channel

  #20354 commented onMar 20, 2025 • 0 new comments