aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-12-09Constrintern: shortcut in cases pattern interning.Hugo Herbelin
2020-12-09Merge PR #13591: [rm] update instructions for windows signingcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-12-09[rm] announcements to discourseEnrico Tassi
2020-12-08Merge PR #13597: Congruence: don't replace error messages by "congruence failed"coqbot-app[bot]
Reviewed-by: ejgallego Ack-by: PierreCorbineau
2020-12-08Update dev/doc/release-process.mdEnrico Tassi
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-12-08Merge PR #13572: [dune] [opam] Disable dune subst in opam files until the ↵coqbot-app[bot]
upstream fix is propagated Reviewed-by: Zimmi48
2020-12-08Merge PR #13596: Add a test for cbv over inductive types which feature ↵coqbot-app[bot]
let-bindings. Reviewed-by: SkySkimmer
2020-12-08Congruence: don't replace error messages by "congruence failed"Gaëtan Gilbert
Fix #13595
2020-12-08Reindent Cctac.cc_tacticGaëtan Gilbert
2020-12-08Add a test for cbv over inductive types which feature let-bindings.Pierre-Marie Pédrot
2020-12-07[rm] manual is uploaded by CIEnrico Tassi
2020-12-07Merge PR #13588: Add `depopts: coq-native` in coq.opam.dockercoqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: proux01
2020-12-07[rm] update instructions for windows signingEnrico Tassi
2020-12-07Merge PR #13556: Fix spelling in warning entrycoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: jfehrle
2020-12-07Add depopts:coq-native in coq.opam.dockerErik Martin-Dorel
2020-12-06Merge PR #13585: [RM] Update changes 13501coqbot-app[bot]
Reviewed-by: Zimmi48
2020-12-06[doc] update changes after 13501Enrico Tassi
2020-12-06Fix spelling in warning entrySimon Friis Vindum
2020-12-05Merge PR #13553: Document Number Notation for primitive integerscoqbot-app[bot]
Reviewed-by: jfehrle
2020-12-04Merge PR #13552: Delay inventing names for monomorphic universesPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-12-04Merge PR #13569: typocoqbot-app[bot]
Reviewed-by: jfehrle
2020-12-04[dune] [opam] Disable dune subst in opam files until the upstream fix is ↵Emilio Jesus Gallego Arias
propagated `dune subst` is broken on unicode files, see https://github.com/ocaml/dune/pull/3879 and https://github.com/ocaml/dune/pull/3879 This is a frequent problem, introduced by https://github.com/coq/coq/pull/13374 , so disabling pending on dune 2.8 being released.
2020-12-04Merge PR #13442: Add an abstraction function in the LtacX FFI.coqbot-app[bot]
Reviewed-by: kyoDralliam
2020-12-04Delay inventing names for monomorphic universesGaëtan Gilbert
This avoids doing it repeatedly for nothing in intern/extern.
2020-12-04Merge PR #13551: Stop calling Id.Map.domain on univ binders every individual ↵coqbot-app[bot]
universe Reviewed-by: herbelin
2020-12-04typoYves Bertot
2020-12-04Merge PR #13497: [rm] update release notescoqbot-app[bot]
Reviewed-by: Zimmi48
2020-12-04[rm] clarify process for is_a_released_version = trueEnrico Tassi
2020-12-04[rm] update git commands to push tagsEnrico Tassi
2020-12-04Merge PR #13527: Changes for Coq 8.13coqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: jfehrle
2020-12-03Merge PR #13546: [coqide] fix procedure to parse argumentscoqbot-app[bot]
Reviewed-by: ejgallego
2020-12-03Merge PR #13558: [refman] Fix error names.coqbot-app[bot]
Reviewed-by: jfehrle
2020-12-03Implement review corrections by Théo ZimmermannMatthieu Sozeau
2020-12-03Implement suggestions by Théo ZimmermannMatthieu Sozeau
2020-12-03Apply suggestions from code reviewMatthieu Sozeau
Co-authored-by: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2020-12-03Apply suggestions from code reviewEnrico Tassi
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-12-03Update doc/sphinx/changes.rstMatthieu Sozeau
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-12-03Fixes in the summary by Jim FehrleMatthieu Sozeau
Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
2020-12-03Changes without PR references fixesMatthieu Sozeau
2020-12-03Apply suggestions from @jfehrle code reviewMatthieu Sozeau
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-12-03[changelog] update markupEnrico Tassi
2020-12-03Add an anchor in syntax-extensionsMatthieu Sozeau
2020-12-03Changes for Coq 8.13Matthieu Sozeau
2020-12-03Merge PR #13548: Move *_with_full_binders variants out of the kernel.coqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: herbelin
2020-12-03[coqide] fix procedure to parse argumentsEnrico Tassi
coqide calls coqidetop -batch, if you are in -async-proof on then coqidetop spawns a worker and passes -batch to it. At some point, I could not find the commit, this made the worker die. On linux it seems it works anyway, but on windows this death is perceived by coqide which then does not start.
2020-12-03[refman] Fix error names.Théo Zimmermann
The @ syntax is not supported in the name, so we transform it manually as it would have been if no name had been provided.
2020-12-03Merge PR #13554: Split long lines in errors and warning indexcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-12-02Split long lines in errors and warning indexJim Fehrle
2020-12-02Merge PR #13275: Put all Int63 primitives in a separate fileVincent Laporte
Ack-by: SkySkimmer Ack-by: ppedrot Reviewed-by: vbgl
2020-12-02Document Number Notation for primitive integersPierre Roux
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 06:03:16 +0000