coq
forked from coq/coq
Star 1
Fork 0
Watch

Commits on master

coqbot-app[bot]
Merge PR #22652: Fix proof of False when VM conversion eta-expands a mutual fixpoint
committed
coqbot-app[bot]
Merge PR #22647: Print Universes Subgraph: keep the constraints with Set
committed
coqbot-app[bot]
Merge PR #22641: Fix OCaml extraction callbacks for recursive functions
committed
coqbot-app[bot]
Merge PR #22623: rocqchk accumulate axioms without "opacify" logic
committed
coqbot-app[bot]
Merge PR #22650: Correctly pass side-effects in some Declare internals.
committed
Sami Jawhar
Add changelog entry and fix link for #22652
committed
Sami Jawhar
Fix proof of False when VM conversion eta-expands a mutual fixpoint
committed
Pierre-Marie Pédrot
Correctly pass side-effects in some Declare internals.
committed
Gaëtan Gilbert
Stop using resolver for nothing in checker axiom collection
committed
Matthieu Sozeau
Add changelog entry
committed
Matthieu Sozeau
Print Universes Subgraph: keep the constraints with Set
committed
coqbot-app[bot]
Merge PR #22603: Stop iterating through libobjects for Search
committed
coqbot-app[bot]
Merge PR #22638: Unfold type abbreviations when locating a fixpoint’s recursive argument.
committed
coqbot-app[bot]
Merge PR #22636: ssr: replace universe state unions by set_ustate when extending
committed
coqbot-app[bot]
Merge PR #22620: Fix recursive-call errors in fixpoint binder types
committed
Jules Massart
Fix OCaml extraction callbacks for recursive functions
committed
coqbot-app[bot]
Merge PR #22631: Export the locations of universes and the universe subgraph
committed
Rodolphe Lepigre
Fix 20632.
committed
Thomas Lamiaux
Fix recursive-call errors in fixpoint binder types
committed
Matthieu Sozeau
ssr: replace universe state unions by set_ustate when extending
committed
Matthieu Sozeau
Export the locations of universes and the universe subgraph
committed
Gaëtan Gilbert
changelog & critical bugs entry
committed
Gaëtan Gilbert
Drop useless env argument of collect_module_axioms
committed
Gaëtan Gilbert
rocqchk accumulate axioms without "opacify" logic
committed
Gaëtan Gilbert
Add test for rocqchk --output-context
committed
Gaëtan Gilbert
mdo_checking rename state variables opac -> st
committed
Gaëtan Gilbert
rocqchk unfuse "opaque" collection and checking
committed
coqbot-app[bot]
Merge PR #22624: Enforce consistency of env typing flags with ugraph type-in-type flag
committed
coqbot-app[bot]
Merge PR #22594: More informative printing of template universes
committed
coqbot-app[bot]
Merge PR #22583: define_evar_as_sort generate a flexible univ instead of rigid
committed
coqbot-app[bot]
Merge PR #22612: CoqProject_file use exn instead of exit, and catch in rocqide
committed
coqbot-app[bot]
Merge PR #22626: Github CI remove deprecated `dune-cache`
committed
Gaëtan Gilbert
Github CI remove deprecated `dune-cache`
committed
Gaëtan Gilbert
regen critical-bugs TOC
committed
Gaëtan Gilbert
Enforce consistency of env typing flags with ugraph type-in-type flag
committed
Gaëtan Gilbert
CoqProject_file use exn instead of exit, and catch in rocqide
committed
Gaëtan Gilbert
Stop iterating through libobjects for Search
committed
coqbot-app[bot]
Merge PR #22611: checker: report sealed implementation assumptions with -norec
committed
coqbot-app[bot]
Merge PR #22614: printing: warn when module contents cannot be printed
committed
Edward Miller
doc: name the module-printing-fallback warning
committed
coqbot-app[bot]
Merge PR #22615: Fix message for deprecated abbreviation and related doc
committed
Gaëtan Gilbert
Slightly more standard test files
committed
Gaëtan Gilbert
Fix message for deprecated abbreviation and related doc
committed
coqbot-app[bot]
Merge PR #22601: Reduce the combinatorics of the grammar state access in Grammar API.
committed
coqbot-app[bot]
Merge PR #22589: Nicer error for incorrect Proof using
committed
coqbot-app[bot]
Merge PR #22604: Print/About print all object kinds when ambiguous
committed
coqbot-app[bot]
Merge PR #22605: update coqdev.el refman error regex
committed
coqbot-app[bot]
Merge PR #22606: Doc: add missing names of warnings
committed
Edward Miller
printing: warn when module contents cannot be printed
committed
Edward Miller
checker: record sealed assumptions in admitted libraries
committed
Edward Miller
checker: decouple opaque dependency recording from check state
committed
Gaëtan Gilbert
rocqdomain.py enforce that every warning has a name
committed
Gaëtan Gilbert
Doc: add missing names of warnings
committed
Gaëtan Gilbert
update coqdev.el refman error regex
committed
coqbot-app[bot]
Merge PR #19404: An algebra of types for the argument of notations
committed
Gaëtan Gilbert
Print/About print all object kinds when ambiguous
committed
coqbot-app[bot]
Merge PR #22591: Catch QGraph.EliminationError when computing the allowed eliminations
committed
Gaëtan Gilbert
More informative printing of template universes
committed
Hugo Herbelin
Add overlays.
committed
Hugo Herbelin
Move and export contract_curly_brackets in an ops file so that Rocq-lsp can use it.
committed