19 Pull requests merged by 9 people

• Fix typo in comment in Ltac2.List

  #20666 merged May 24, 2025

• Fix backtrace of exception reraised in coercion handling

  #20665 merged May 23, 2025

• Monomorphize sort polymorphic code in extraction.

  #20655 merged May 22, 2025

• ltac2: register names for terms and type definitions in VtSideff

  #20625 merged May 22, 2025

• Bench use metarocq instead of metacoq

  #20664 merged May 22, 2025

• Separate nametab search handling of deprecated Coq from main algorithm

  #20661 merged May 21, 2025

• Clean up Ccprojectability implementation

  #20659 merged May 21, 2025

• Remove unused Lia Enum flag

  #20640 merged May 21, 2025

• remove some remaining uses of coq

  #20658 merged May 21, 2025

• new example for bidirectionality hints in refman #12102

  #20370 merged May 21, 2025

• Doc: add note about Printing Parentheses not adding parens to applications

  #20613 merged May 20, 2025

• [refman] Improve Corelib documentation

  #20356 merged May 20, 2025

• Added a new projection generation for congruence

  #19700 merged May 20, 2025

• Fix Print Ltac2.foo parsing

  #20633 merged May 20, 2025

• Unify nametab APIs using functors

  #20502 merged May 20, 2025

• Fix guard checker inconsistency

  #20648 merged May 20, 2025

• Use a uniform representation for inductive nodes in extraction.

  #20651 merged May 19, 2025

• Fixed plugin_tutorial in rocq

  #20378 merged May 19, 2025

• Stop relying on ref + exception in Induction.compute_elim_sig.

  #20641 merged May 19, 2025

11 Pull requests opened by 4 people

• Fix wrong threading of cv_pb/pb in unification.ml

  #20652 opened May 19, 2025

• Ltac2 add $hyp:id quotation for dynamic hypotheses (where &id is static)

  #20656 opened May 20, 2025

• Search: allow typos when searching by string

  #20660 opened May 20, 2025

• Reference not found error suggests similar names

  #20662 opened May 20, 2025

• Update parsing md & mention it in plugin tuto mlg files

  #20669 opened May 22, 2025

• Update plugin tuto

  #20670 opened May 22, 2025

• Update vscoq CI script and rename to vsrocq

  #20672 opened May 23, 2025

• Guard against parser modification in interp phase

  #20674 opened May 23, 2025

• Remove remnants of global mutable state in extraction

  #20675 opened May 24, 2025

• Small typo in ltac2.rst

  #20676 opened May 25, 2025

• Other typos in ltac2.rst

  #20677 opened May 25, 2025

3 Issues closed by 2 people

• Need a better example of bidirectionality hints

  #12102 closed May 21, 2025

• bad parsing of `Print Ltac2.foo.`

  #19424 closed May 20, 2025

• Proof of False because of guard checker issue

  #20555 closed May 20, 2025

8 Issues opened by 6 people

• Ssreflect rewrite calls to setoid fail is pattern is under binder

  #20673 opened May 23, 2025

• bypass_check(universes) incompatible with global universes

  #20671 opened May 22, 2025

• Abbreviations leak through outer module import

  #20668 opened May 22, 2025

• Unset Universe Checking breaks relevance marks

  #20667 opened May 21, 2025

• incorrect cbv with Definitional UIP

  #20663 opened May 20, 2025

• lia effectively diverges on terms with large exponents

  #20657 opened May 20, 2025

• Preterm.in_context, Preterm.in_context_prod

  #20654 opened May 19, 2025

• Sort variable cumulativity constraints

  #20653 opened May 19, 2025

36 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.

• Stricter non-ambiguousness check in Require

  #20601 commented on May 22, 2025 • 11 new comments

• Add conversion test to Ltac2/Unification

  #20649 commented on May 22, 2025 • 10 new comments

• Port `rewrite_strat` to Ltac2

  #20544 commented on May 21, 2025 • 4 new comments

• [draft] A minimal working example modifying the -vok option of coqc/rocqc

  #19932 commented on May 19, 2025 • 2 new comments

• Backport opam file changes from opam repo

  #20432 commented on May 19, 2025 • 1 new comment

• Add a module Ltac1CompatibilityNotations for Ltac1 notations like transitivity

  #20569 commented on May 20, 2025 • 1 new comment

• An algebra of types for the argument of notations

  #19404 commented on May 19, 2025 • 1 new comment

• new Printing option: FullyQualifiedNames

  #20615 commented on May 20, 2025 • 0 new comments

• Move flags from flags.ml to more precise locations

  #20606 commented on May 20, 2025 • 0 new comments

• [tauto] change proof search strategy

  #20627 commented on May 21, 2025 • 0 new comments

• Share closures in the VM.

  #20634 commented on May 22, 2025 • 0 new comments

• Avoid generating bad template constraints in ssr saturate

  #20583 commented on May 19, 2025 • 0 new comments

• Use `;` instead of `|` to separate sorts and univs (eg `Type@{s;u}`)

  #20635 commented on May 21, 2025 • 0 new comments

• Add a new loop-checking implementation of the "graph"

  #20574 commented on May 23, 2025 • 0 new comments

• ci-hott run make install (for the minimizer)

  #20637 commented on May 19, 2025 • 0 new comments

• Ltac2 custom entries

  #20561 commented on May 20, 2025 • 0 new comments

• More type enforced "instantiation" of constr patterns

  #20644 commented on May 19, 2025 • 0 new comments

• An elimination constraint graph to manage elimination of sort variables

  #20506 commented on May 23, 2025 • 0 new comments

• Move source code theories to theories/Corelib and user-contrib/Ltac2 to theories/Ltac2

  #20650 commented on May 24, 2025 • 0 new comments

• Make `Coinductive` and `Cofixpoint` stylistic alternatives to `CoInductive` and `CoFixpoint`

  #20622 commented on May 19, 2025 • 0 new comments

• Surprising Failure in Type Class Inference

  #19728 commented on May 19, 2025 • 0 new comments

• Unexpected behaviour of specialize with (...:=...) in combination with typeclasses

  #18711 commented on May 20, 2025 • 0 new comments

• Regression with action patterns in specialize in Coq 8.15

  #16020 commented on May 20, 2025 • 0 new comments

• specialize does not support evars in the instantiated args.

  #18332 commented on May 20, 2025 • 0 new comments

• Ltac2 page in refman should refer to Corelib

  #20450 commented on May 25, 2025 • 0 new comments

• Ltac2: warning when defining named type variables

  #18118 commented on May 19, 2025 • 0 new comments

• Take into account the local delta flags for "simpl"

  #18621 commented on May 19, 2025 • 0 new comments

• Add SSReflect contextual pattern `UNDER`

  #19011 commented on May 19, 2025 • 0 new comments

• [core] Improved state protection against memprof-limits interruptions

  #19177 commented on May 20, 2025 • 0 new comments

• Extraction: Allow to inject compiler pragmas in generated file

  #19906 commented on May 19, 2025 • 0 new comments

• Refold before evar instantiation

  #19987 commented on May 23, 2025 • 0 new comments

• make Fix_eq a bit easier to use

  #20018 commented on May 19, 2025 • 0 new comments

• Fix CMorphisms partial_application_tactic to correctly leverage Params instances

  #20045 commented on May 20, 2025 • 0 new comments

• Clarify release notes

  #20136 commented on May 19, 2025 • 0 new comments

• Warning when generating a constraint involving a template universe

  #20226 commented on May 19, 2025 • 0 new comments

• Tify + lra solves programs mixing Z and R

  #20288 commented on May 21, 2025 • 0 new comments