GitHub webhook has been successfully configured by Zimmi48.
ppedrot pushed 10 commits to branch master. Commits by JasonGross (9) and ppedrot (1).
Add a with_strategy
tactic (2edbbfe )
Fix the with_strategy
tactic to work with abstract
(33388d1 )
Elaborate with_strategy warning (ee3b91f )
Work around a bug in Coq in the doc (452f809 )
[with_strategy] Work around #12191 (adff727 )
Fix a bug with with_strategy, behavior on multisuccess tactics (573fed5 )
[with_strategy] Fix for coqchk (3c66c60 )
Revert "[with_strategy] Fix for coqchk" (6b223d1 )
Add another note about removing a tactic after abstract (6e4ebb2 )
Merge PR #12129: Add a with_strategy
tactic (0abac9b )
Some squashing wouldn't have hurt, especially of the "Fix" and "Revert Fix" commits :P
ppedrot pushed 2 commits to branch v8.11. Commits by ejgallego (1) and ppedrot (1).
[errors] Don't raise inside exception printers (7ea8894 )
Merge PR #12294: [errors] Don't raise inside exception printers (484bb2f )
ppedrot deleted the branch macos-binary-8.11.1.
ejgallego pushed 4 commits to branch master. Commits by ppedrot (3) and ejgallego (1).
Port Evar_tactics to the new API. (36f8369 )
Remove call to Refiner API from Funind. (ffda464 )
Deprecate the legacy tacticals from module Refiner. (1d16c80 )
Merge PR #12273: Deprecate Refiner API (76f7adc )
herbelin pushed 2 commits to branch master2. Commits by herbelin (1) and lthms (1).
chore: Add missing [Register] for inductive types in Datatypes.v (28a698d )
Merge PR #10609: Register (for Coqlib.ref_lib) several base datatypes of stdlib (d640d9d )
herbelin pushed 2 commits to branch master. Commits by herbelin (1) and lthms (1).
chore: Add missing [Register] for inductive types in Datatypes.v (28a698d )
Merge PR #10609: Register (for Coqlib.ref_lib) several base datatypes of stdlib (d640d9d )
herbelin deleted the branch master2.
herbelin pushed 2 commits to branch master. Commits by herbelin (1) and ppedrot (1).
In non-strict mode, accept any variable as a tactic reference. (c43231d )
Merge PR #12254: In non-strict mode, accept any variable as a tactic reference. (00328b2 )
ppedrot pushed 24 commits to branch v8.11. Commits by ppedrot (10), herbelin (8), Zimmi48 (2) and others (4).
Add an example to motivate strictly positive occurrences check (496fe37 )
Drop some the coqtop output, rephrase a bit (d35a4fe )
Backport PR #12268: Add an example to motivate strictly positive occurrences check (285a687 )
Coqide completion: Avoiding using an iterator in an apparently sensitive code. (2cb25bd )
Change log for #12068 (Coqide segfault tentative fix). (8a29575 )
CoqIDE completion: Relying on INSERT mark of the buffer. (0b86cb6 )
Backport PR #12068: Coqide completion: tentative fix for #11943 (bf8354e )
Less confusing configure message when lablgtk exists but not lablgtksourceview. (90f5e8c )
Backport PR #12222: Less confusing configure message when lablgtk exists but not lablgtksourceview (ca5c499 )
CoqIDE: Avoid invalidation of an iterator in insert callback. (b6203de )
Backport PR #12160: CoqIDE: Avoid invalidation of an iterator in insert callback (d7e1cfd )
Remove documentation for Hide menu in CoqIDE (was removed in 8.5). (e9fcab7 )
Backport PR #12090: Remove documentation for Hide menu in CoqIDE (was removed in 8.5). (7fad899 )
CoqIDE: Disable client-side decoration on Windows (55b8585 )
Backport PR #12060: CoqIDE: Disable client-side decoration on Windows (9458d25 )
Coqide: Apply style scheme and language to the three buffers. (7369fb4 )
CoqIDE: Adding a short documentation on style/theme customization. (17a5ffd )
Backport PR #12106: Coqide: Apply style scheme and language settings to the three sourceview buffers. (595329b )
CoqIDE: Revert overzealous application of language-based highlighting in #12169. (06000a7 )
Backport PR #12173: CoqIDE: Revert overzealous application of language-based highlighting from #12169 (fc20150 )
[and 4 more commit(s)]
Zimmi48 pushed 2 commits to branch master. Commits by Zimmi48 (1) and olaure01 (1).
fuse changelogs for #11249 and #12237 (9f5a604 )
Merge PR #12303: [changelog] Fuse changelogs for #11249 and #12237 (007ed9e )
anton-trunov pushed 2 commits to branch master. Commits by anton-trunov (1) and olaure01 (1).
Declare more Permutation instances as Global (354582c )
Merge PR #12190: [stdlib] [Permutation] Declare more instances as Global (6977301 )
ppedrot pushed 18 commits to branch v8.11. Commits by ppedrot (8), herbelin (5), kyoDralliam (2) and others (3).
Fixes #11194 (Canonical/Coercion not located for coqdoc). (90c2b3d )
Backport PR #12025: Fixes #11194 (Canonical/Coercion not located for coqdoc) (49dc6bc )
Don't create index entries for the name "_" (3bcd035 )
Backport PR #12123: Don't create index entries for the name "_" (f645a4b )
Fixing #12045 (missing normalization in conclusion of custom induction scheme). (1ad28cc )
Change log for PR #12045. (414e602 )
Backport PR #12116: Fixing #12045: missing normalization in conclusion of custom induction scheme (c61a6c5 )
Fixing export of CAML_LD_LIBRARY_PATH from config/Makefile to Makefile.common. (6690268 )
Exporting BEST as OPT for the tests using coq_makefile-generated Makefile. (e74eeb4 )
Backport PR #12082: Fixes #11808: support for test-suite in -byte-only mode (184dd2f )
[documentation] ssreflect: Abbreviations do not support scope (4ad3486 )
Backport PR #12154: [documentation] ssreflect: Abbreviations do not support scope (ec1c1d4 )
Document +
in polymorphic universe levels (6697520 )
Backport PR #12156: Document +
in polymorphic universe levels (ad51950 )
Doc: extend example for induction a bit (4da2740 )
Backport PR #12176: Doc: extend example for induction a bit (e9230c2 )
Improve error messages for Set and Unset commands. (305b7a5 )
Backport PR #12003: Improve error messages for Set and Unset commands. (ba4abe3 )
ppedrot pushed 5 commits to branch master. Commits by herbelin (4) and ppedrot (1).
Termops: Adding functions local_occur_var_in_decl and occur_var_indirectly. (aa23fb7 )
Tactic subst now inactive on section variables occurring indirectly in goal. (dd9bcf3 )
Adding change log for #12146. (3dbf278 )
Documenting the new behavior of "subst". (3a8376b )
Merge PR #12146: Fixes #10812: tactic subst failure with section variables indirectly dependent in goal (efb78e3 )
anton-trunov pushed 2 commits to branch master. Commits by anton-trunov (1) and olaure01 (1).
rename Bool.leb into Bool.le (same for ltb and compareb) (1019cb4 )
Merge PR #12162: Fixing #12161: rename Bool.leb into Bool.le (5784bb9 )
ppedrot pushed 4 commits to branch master. Commits by herbelin (3) and ppedrot (1).
Locating error again in TacAtom and TacAlias (fixes #12152, fixes #12255). (01e4659 )
Adding tests for error location (403fe03 )
Change log for #12223. (cb14a7e )
Merge PR #12223: Locating error again in atomic tactics (fixes #12152) (942a198 )
ppedrot pushed 4 commits to branch v8.11. Commits by SkySkimmer (2) and ppedrot (2).
Fix #11783 Require in Section (d85e9fd )
Backport PR #11972: Fix require in section (6b78420 )
Fix #11854 error message on unsolved evars in Instance. (e0ae592 )
Backport PR #11982: Fix #11854 error message on unsolved evars in Instance. (b378f6e )
JasonGross pushed 6 commits to branch master. Commits by kyoDralliam (3), ppedrot (2) and JasonGross (1).
Allow to rebind the old value of a mutable Ltac2 entry. (457cee4 )
Generalize the Ltac2 value criterion to pure let-bindings. (ead129a )
Correcting ltac2's documentation on values turning test into proper check. (6cb2449 )
More tests of rebinding Ltac2 definitions (ceb1f56 )
documenting with examples the dynamic behaviour of Ltac2 Set (639b19e )
Merge PR #11503: Allow to rebind the old value of a mutable Ltac2 entry. (0992c26 )
ejgallego pushed 9 commits to branch master. Commits by ppedrot (8) and ejgallego (1).
Remove useless try-with blocks in congruence. (e802f48 )
Do not use Unsafe.to_constr for old refiner conclusion. (d31cb4d )
Wrap the legacy refiner type into the Logic API. (65551cd )
Remove useless try-with clauses in newring. (8bc79fd )
Remove legacy Refiner error constructors. (5530ac6 )
Clean up the legacy refiner implementation. (b3b9673 )
Write the outermost part of the legacy refiner directly in the monad. (20ed946 )
Remove a unused legacy tactic from Clenv. (c5fdfe6 )
Merge PR #12307: Cleaning up the legacy proof engine (4a59444 )
cpitclaudel pushed 2 commits to branch master. Commits by Zimmi48 (1) and cpitclaudel (1).
Remove documentation of -compile, which was removed in #8690. (e3e889c )
Merge PR #12309: Remove documentation of -compile, which was removed in #8690. (67f0e9f )
ppedrot pushed 6 commits to branch v8.11. Commits by herbelin (3), ppedrot (2) and proux01 (1).
Locating error again in TacAtom and TacAlias (fixes #12152, fixes #12255). (8892a08 )
Adding tests for error location (93691be )
Change log for #12223. (0af9e5c )
Backport PR #12223: Locating error again in atomic tactics (fixes #12152) (53c3f81 )
Ignore -native-compiler option when disabled (6f276f6 )
Backport PR #12070: Ignore -native-compiler option when disabled (d75e245 )
ppedrot pushed 2 commits to branch v8.11.
Tweak the OCaml version used to generate the MacOS package. (45432df )
Merge PR #12310: Tweak the OCaml version used to generate the MacOS package. (4ea03e6 )
anton-trunov pushed 7 commits to branch clarify-merging-with-overlays. Commits by llelf (5) and anton-trunov (2).
do not re-export ListNotations from Program (b500758 )
do not re-export ListNotations from Program: overlays (7776cf7 )
do not re-export ListNotations from Program: changelog (1175ca0 )
do not re-export ListNotations from Program: fix testsuite (4a47406 )
do not re-export ListNotations from Program: vst overlay (38c522d )
Merge PR #11992: do not re-export ListNotations from Program (026aa3e )
Clarify the documentation for merging PRs with overlays (5e1110b )
anton-trunov deleted the branch clarify-merging-with-overlays.
ppedrot pushed 2 commits to branch v8.11. Commits by Zimmi48 (1) and ppedrot (1).
Remove documentation of -compile, which was removed in #8690. (098fb32 )
Backport PR #12309: Remove documentation of -compile, which was removed in #8690. (ebf789e )
SkySkimmer pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
[obligations] Deprecated flag cleanup (2b3bd34 )
Merge PR #11828: [obligations] Deprecated flag cleanup (23be910 )
Zimmi48 pushed 7 commits to branch master. Commits by herbelin (6) and Zimmi48 (1).
Documenting plugin/tactic/stdlib keywords in corresponding chapters. (62f6fb8 )
Mention keywords used in tactics from g_tactic.mlg. (259162b )
Mention keywords from g_ltac.mlg used in Ltac. (986bfd1 )
Stop keeping outdated static list of keywords. (86cdd51 )
Moving lazymatch and multimatch to simple identifiers. (20f0e2e )
Keywords: Applying suggestions from Jim Fehrle and Théo Zimmermann. (037c8d2 )
Merge PR #12229: Hopefully consensual cleaning of keywords (d804588 )
Zimmi48 pushed 2 commits to branch master. Commits by Zimmi48 (1) and k4rtik (1).
Remove (outdated) timestamps from man pages (844142c )
Merge PR #12293: Fix timestamp of coqchk manpage (91b5990 )
ejgallego pushed 3 commits to branch master. Commits by ppedrot (2) and ejgallego (1).
Store the OCaml version used for Coq in vo files. (3e04d6c )
Centralize the OCaml version-checking function. (9e31583 )
Merge PR #12244: Store the OCaml version used for Coq in vo files. (2a43f3e )
ejgallego pushed 2 commits to branch master. Commits by ejgallego (1) and herbelin (1).
Tests for bugs #9583 (fixed by #11613) and #9679. (354cf42 )
Merge PR #12315: Tests for bugs #9583 (fixed by #11613) and #9679. (9c639d6 )
ejgallego pushed 5 commits to branch master. Commits by herbelin (4) and ejgallego (1).
Extending support for mixing binders and terms in abbreviations. (466e673 )
Documenting notations with both terms and binders. (d5a6c8a )
Overlay elpi (9e3f168 )
Adding change log for #8808. (e9692be )
Merge PR #8808: Extending support for mixing binders and terms in abbreviations (8b0d7a1 )
ejgallego pushed 4 commits to branch master. Commits by Zimmi48 (2), Lasse Blaauwbroek (1) and ejgallego (1).
Interleave commandline require/set/unset commands (bd78f32 )
Document the changes regarding the order of command-line options. (684bbe5 )
Test interleaving of command-line options. (4c5e40b )
Merge PR #12097: Interleave commandline require/set/unset commands (734d732 )
vbgl pushed 2 commits to branch master. Commits by SkySkimmer (1) and vbgl (1).
nit: don't open Persistent_cache in micromega (7ed5fc9 )
Merge PR #12214: nit: don't open Persistent_cache in micromega (86867b4 )
SkySkimmer pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
[ci] [sf] Fix SF build. (2bdea3e )
Merge PR #12320: [ci] [sf] Fix SF build. (13bd7be )
SkySkimmer pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Make explicit that UGraph lower bounds are only of two kinds. (f71ef93 )
Merge PR #12313: Make explicit that UGraph lower bounds are only of two kinds. (6f2b886 )
Zimmi48 pushed 3 commits to branch master. Commits by anton-trunov (2) and Zimmi48 (1).
Clarify the documentation for merging PRs with overlays (842502a )
Clarify the assignee's role in removing the overlay information (122ab27 )
Merge PR #12312: Clarify the documentation for merging PRs with overlays (8dd5c47 )
ppedrot pushed 2 commits to branch v8.11. Commits by ejgallego (1) and ppedrot (1).
[ci] [sf] Fix SF build. (fd2c75f )
Backport PR #12320: [ci] [sf] Fix SF build. (07fa380 )
maximedenes pushed 4 commits to branch master. Commits by ppedrot (3) and maximedenes (1).
No more local reduction functions in Reductionops. (2a79abc )
Further cleanup: remove the local_reduction_function type. (cf60564 )
Add overlays. (101d898 )
Merge PR #11922: No more local reduction functions in Reductionops. (81fba80 )
Zimmi48 pushed 2 commits to branch master. Commits by Zimmi48 (1) and ppedrot (1).
Add a changelog for 8.11.2. (9f9a77f )
Merge PR #12327: Add a changelog for 8.11.2. (e36c415 )
Janno pushed 1 commit to branch janno/cs_lambda.
Enable canonical fun _ => _
projections. (034b7b5 )
@Janno You seem to have mistakenly pushed to the main repo. Could you please delete your branch?
Oh, sure! I wonder how that happened
Janno deleted the branch janno/cs_lambda.
From the name of the branch, I bet this is a confusion in the git push
syntax.
I.e. you probably wanted to push to your fork and pushed to a new janno/branch_name
branch instead.
Oh, indeed, I copied git
's proposed --set-upstream
thingy which always suggests origin
..
I should absolutely not be able to push anything to the main repo, btw. GitHub really needs to come up with a better way of handling permissions..
FTR I recommend adopting the following convention:
upstream points to upstream
origin points to your personal fork
Then, you can use a .gitconfig
similar to mine: https://github.com/Zimmi48/dotfiles/blob/master/.gitconfig
(see in particular push.default
+ remote.pushdefault
) so that pushing always go to your fork by default.
GitHub really needs to come up with a better way of handling permissions..
Agreed!
Théo Zimmermann said :
FTR I recommend adopting the following convention:
upstream points to upstream
origin points to your personal fork
Then, you can use a .gitconfig
similar to mine: https://github.com/Zimmi48/dotfiles/blob/master/.gitconfig
(see in particular push.default
+ remote.pushdefault
) so that pushing always go to your fork by default.
I'll try to adopt that convention!
SkySkimmer pushed 3 commits to branch master. Commits by herbelin (2) and SkySkimmer (1).
Fixes #12234 (wrong environment for Show Proof). (cd1bb55 )
Added change log. (5c3b9f9 )
Merge PR #12296: Fixes #12234: wrong environment for Show Proof (cc54af3 )
herbelin pushed 7 commits to branch master. Commits by ppedrot (6) and herbelin (1).
Move the static check of evaluability in unfold tactic to runtime. (be56f39 )
Generalize the interpretation of syntactic notation as reference to their head. (3af3409 )
Add test for #11727, which was indirectly fixed by this PR. (2e53445 )
Tweak the error message of reference internalization. (5e1da5b )
Remove an outdated piece of documentation about limitations of unfold. (ec14db8 )
Adding changelog. (b5ecd2e )
Merge PR #12256: Move the static check of evaluability in unfold tactic to runtime. (56e2384 )
ppedrot pushed 2 commits to branch v8.11.
Add a changelog for 8.11.2. (bfd529d )
Backport PR #12327: Add a changelog for 8.11.2. (1816614 )
ppedrot pushed 3 commits to branch v8.11.
Bump the version number to 8.11.2. (8832e1f )
Mark this commit as a released version. (4960de3 )
Merge PR #12328: Release 8.11.2 (1539a9a )
ppedrot pushed tag V8.11.2.
ppedrot pushed 1 commit to branch v8.11.
MSoegtropIMC pushed 8 commits to branch master. Commits by gares (7) and MSoegtropIMC (1).
[win] Coq trunk is now called master (9c111b3 )
[win] since 4.07 the seq package is part of ocaml (d93b46d )
[win] bump camlp5 to 7.11 since OCaml 4.08 requires it (dd90217 )
[win] rules to build Elpi (f4e2b0b )
[win] addon for elpi (40e7685 )
[win] addon for Hierarchy Builder (a8fbe8b )
[win] CI build addons Coq-Elpi Hierarchy-Builder (64cce27 )
Merge PR #12032: [win] Elpi, Coq-Elpi and HB (a605c48 )
anton-trunov pushed 7 commits to branch master. Commits by llelf (6) and anton-trunov (1).
do not re-export ListNotations from Program (b500758 )
do not re-export ListNotations from Program: overlays (7776cf7 )
do not re-export ListNotations from Program: changelog (1175ca0 )
do not re-export ListNotations from Program: fix testsuite (4a47406 )
do not re-export ListNotations from Program: vst overlay (38c522d )
do not re-export ListNotations from Program: kill overlays (7510aa6 )
Merge PR #11992: do not re-export ListNotations from Program (959254c )
ejgallego pushed 2 commits to branch master. Commits by Zimmi48 (1) and ejgallego (1).
Add advisories on OCaml setup to INSTALL.md. (5383050 )
Merge PR #12243: Add a note on build-time dependencies to INSTALL.md. (bcfb5f2 )
ppedrot pushed 2 commits to branch master. Commits by ejgallego (1) and ppedrot (1).
[exn] [tactics] improve backtraces on monadic errors (e8bde45 )
Merge PR #11755: [exn] [tactics] improve backtraces on monadic errors (b5b6e2d )
herbelin pushed 12 commits to branch master. Commits by proux01 (11) and herbelin (1).
NumTok.int doesn't exist anymore (492eae7 )
Uniformize indentation in theories/Numbers (3864d78 )
Decimal: specify numeral notation for Q (5372090 )
Decimal: prove numeral notation for Q (a9ecce2 )
Add helper function (97567ff )
Rename functions (deb2607 )
Add hexadecimal numerals (692c642 )
[doc] Add hexadecimal numerals (0ee6e30 )
Hexadecimal: proofs that conversions from/to nat,N,Z and Q are bijections (da4a78d )
Hexadecimal: conversion to/from Coq strings (2d6c26c )
Add overlays (31f5e89 )
Merge PR #11948: Hexadecimal numerals (a5c9ad8 )
ejgallego pushed 3 commits to branch master. Commits by Zimmi48 (2) and ejgallego (1).
Add a rudimentary script to generate release changelog. (3ed313c )
Support when release branch is checked out in a worktree. (8208e5f )
Merge PR #11979: Add a rudimentary script to generate release changelog. (215990f )
ejgallego pushed 3 commits to branch master. Commits by herbelin (2) and ejgallego (1).
Fixes #12322 (anomaly when printing "fun" binders with implicit types). (6a85fd4 )
Add changelog for #12323. (6b793e6 )
Merge PR #12323: Fixes #12322: anomaly when printing "fun" binders with implicit types (03e0aa5 )
cpitclaudel pushed 61 commits to branch master. Commits by Zimmi48 (60) and cpitclaudel (1).
Extract Sorts out of CIC. (9727d6f )
Create new file on sorts. (73b1000 )
Extract Private inductive types from Gallina. (c7b529c )
Create a new file on Variants. (b0e3404 )
Extract Variants from Gallina. (abe9dbd )
Create a new file on Variants. (37b1a35 )
Extract match from Gallina. (fc29e2d )
Add match to new file on Variants. (4f71e81 )
Merge sections on Variants and Private inductive types into new file. (f6c8f67 )
Merge sections on variants and match into new file. (f2e86f9 )
Extract Inductive types from Gallina. (d3ad26c )
Create new file on Inductive types. (a403808 )
Extract Recursive functions from Gallina. (f0cc07b )
Add Recursive functions to new file on Inductive types. (1d34b15 )
Merge sections on Inductive types and Recursive functions in new file. (4bfee4c )
Extract Inductive types from CIC. (485c5a1 )
Create new file on Inductive types. (75d32b4 )
Merge section on Inductive types from Gallina and CIC. (11b1e41 )
Extract CoInductive types from Gallina. (8f0236f )
Create new file on CoInductive types. (308da7f )
[and 41 more commit(s)]
ppedrot pushed 3 commits to branch master. Commits by ejgallego (2) and ppedrot (1).
[misc] Better preserve backtraces in several modules (7e078b0 )
[interp] Register printers for InternalizationError instead of ad-hoc hanlding. (8fd01b5 )
Merge PR #11566: [misc] Better preserve backtraces in several modules (ebaaa73 )
Zimmi48 pushed 3 commits to branch master. Commits by gares (2) and Zimmi48 (1).
Clarify release-process.md (878ffbe )
Update dev/doc/release-process.md (40af9cd )
Merge PR #12335: Clarify release-process.md (accac86 )
Zimmi48 pushed 2 commits to branch master. Commits by Zimmi48 (1) and herbelin (1).
Checking validity of coqdoc file name. (632f709 )
Merge PR #12277: Checking validity of coqdoc file name (fixes #12265) (05e811a )
ejgallego pushed 14 commits to branch master. Commits by herbelin (7), Zimmi48 (6) and ejgallego (1).
Update docgram following #12122 and #12229. (576d84e )
Renaming search_about_item into search_item. (a28c4b0 )
Search: new clauses for searching head, conclusion, kind... (96333c1 )
Addressing a suggestion from Théo Zimmermann. (7c113b3 )
Move SSR's Search to a new plugin and deprecate it. (023d189 )
Search: Displaying the "use About" notice only when really needed. (34237bb )
Cleaning the use of pstate and evar_map in Search. (5037435 )
Moving interpretation of Search commands to their own file: comSearch.ml . (ac507d8 )
Add overlays for coqhammer and coq-dpdgraph. (7026c49 )
Deprecate SearchHead. (eae7b25 )
Document new Search features. (de91dd4 )
Test new Search features. (fc20005 )
Changelog entries for #8855. (ca00028 )
Merge PR #8855: More search options (2b0df4d )
cpitclaudel pushed 2 commits to branch master. Commits by Zimmi48 (1) and cpitclaudel (1).
Add redirects for HTML pages that were moved. (3324759 )
Merge PR #12330: Add redirects for HTML pages that were moved. (8df74ac )
Zimmi48 pushed 4 commits to branch master. Commits by ejgallego (3) and Zimmi48 (1).
[micromega] Revert bad change from 5001deed21e8f4027411cc6413a9d2b98e1bccee (daa5d0f )
Revert "Temporarily disable Windows job on Azure." (660eef9 )
[ci] [azure] Rework windows Azure pipeline (6ce9ba1 )
Merge PR #12071: [ci] [micromega] Fix windows build and Micromega bug introduced in #11756 (e35949c )
ejgallego pushed 3 commits to branch master. Commits by Matafou (1), Zimmi48 (1) and ejgallego (1).
Fix #11761: Functional Induction throws unrecoverable error. (888aaeb )
Fix note on implicit arguments in doc of functional induction. (e83a92d )
Merge PR #12326: Fix #11761: Functional Induction throws unrecoverable error. (d81bb40 )
MSoegtropIMC pushed 2 commits to branch master. Commits by MSoegtropIMC (1) and VincentSe (1).
Prove that classical reals implement constructive reals. Also move sums, min and max to CoRN. (e663b60 )
Merge PR #12288: Prove that classical reals implement constructive reals. (b9591f1 )
JasonGross pushed 2 commits to branch master. Commits by JasonGross (1) and MSoegtropIMC (1).
Ltac2: add notations for eval cbv in ... and other in place reductions (e6b295a )
Merge PR #11981: Ltac2: add notations for eval cbv in ... and other in place reductions (5ec4008 )
ejgallego pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
test-suite/Makefile: fix incomplete prerequisite list (835289d )
Merge PR #12345: test-suite/Makefile: fix incomplete prerequisite list (a891dd5 )
Zimmi48 pushed 2 commits to branch master. Commits by Zimmi48 (1) and ejgallego (1).
[search] [ssr] Emit deprecated message when calling search from ssreflect (57c023f )
Merge PR #12341: [search] [ssr] Emit deprecated message when calling search from ssreflect (b7c14a8 )
b7c14a8 changed its status to success .
Janno opened PR #12349 Allow dependent products in canonical instances. from janno/cs_dep_prod
to master
:
This removes the restriction to non-dependent products. Dependent and non-dependent products are handled the same way.
The code is arguably simpler than before and also more powerful. I have some use cases in mind but they would probably only work with Unicoq so I can't provide a very compelling example here. In any case, @gares and @mattam82 seemed to agree that this could be a worthwhile change, and, based on what @ggonthier's wrote in https://github.com/coq/coq/issues/11189#issuecomment-558673619 , it seems that removing the dependency check could be the right thing to do even without any use cases where the function type actually is dependent (as opposed to just appearing dependent during unification).
This needs benchmarking since it might well be slower for non-dependent functions than the original code.
I'll add documentation after #12329 is merged since that PR contains new documentation for canonical structures.
<!-- Thank you for your contribution.
Make sure you read the contributing guide and fill this template. -->
<!-- Keep what applies -->
Kind: feature.
<!-- If there is a user-visible change in coqc/coqtop/coqchk/coq_makefile behavior and testing is not prohibitively expensive: -->
<!-- (Otherwise, remove this line.) -->
[X] Added / updated test-suite
<!-- If this is a feature pull request / breaks compatibility: -->
<!-- (Otherwise, remove these lines.) -->
[ ] Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).
[ ] Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details).
Janno requested pretyper-maintainers for a review on PR #12349 Allow dependent products in canonical instances. .
60ec5b9 changed its status to failure .
60ec5b9 changed its status to pending .
GitHub webhook has been successfully configured by Zimmi48.
@Gaëtan Gilbert I've moved the other notifications that you had added to another topic "GitHub Noisy Notifications", so that people (like me) can easily mute them.
cool
ejgallego pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
Improve spacing in Print Assumptions (2d6dd66 )
Merge PR #11980: Improve spacing in Print Assumptions (b456cf6 )
ejgallego pushed 2 commits to branch master. Commits by Zimmi48 (1) and ejgallego (1).
Zimmi48 pushed the branch v8.12.
gares pushed tag V8.13+alpha.
gares removed tag V8.13+alpha.
herbelin pushed 5 commits to branch master. Commits by SkySkimmer (3), ejgallego (1) and herbelin (1).
test-suite: fix bug causing unit tests to be skipped (d70eded )
Fix proof_diffs_test.ml (4c69c4a )
Revert "[test] unit tests for ide/coq_lex.ml" + makefile support (7da245b )
[azure OSX] Export OCAMLPATH so test-suite sees OCaml libs (3decaca )
Merge PR #12289: test-suite: fix bug causing unit tests to be skipped (2222e45 )
Maybe we should have a stream just for notifications too btw
Yes, seems too noisy, especially with the CI event.
(you can mute any given topic)
I'm going to disable the CI events, they just post commit hashes so it's impossible to tell which ones we should care about.
Still would be a bit more organized under their own stream IMO
They pollute the topic namespace
SkySkimmer pushed 5 commits to branch master. Commits by ejgallego (4) and SkySkimmer (1).
[obligations] Pre-functionalize Program state (809291d )
[declare] Merge DeclareObl
into Declare
(c8b54d7 )
[declare] Grand unification of the proof save path. (5ae026c )
[ci] Old overlay cleanup. (833d767 )
Merge PR #12301: [declare] Grand unification of the proof save path. (407ca66 )
ejgallego pushed 3 commits to branch master. Commits by gares (2) and ejgallego (1).
Update release-process.md (e1e4073 )
Update release-process.md (ffe1de0 )
Merge PR #12353: Update release-process.md (5b23b80 )
cpitclaudel pushed 4 commits to branch master. Commits by Zimmi48 (2), cpitclaudel (1) and jfehrle (1).
Bump minimal versions of refman dependencies. (7cac115 )
Support :gdef:text <term>
syntax (adding "<term>") (ae208f0 )
Use the new gdef alt-text feature in the refman. (c1125bd )
Merge PR #12224: Support :gdef:text<term>
syntax (adding "<term>") (ed0f2f0 )
ejgallego pushed 2 commits to branch master. Commits by Zimmi48 (1) and ejgallego (1).
Use dev version for opam git pinning in .gitlab-ci.yml. (82d26fe )
Merge PR #12362: Use dev version for opam git pinning in .gitlab-ci.yml. (2cd3c71 )
SkySkimmer pushed 2 commits to branch master. Commits by SkySkimmer (1) and Zimmi48 (1).
Direct URL for triggering a pipeline with SKIP_DOCKER=false. (de90f07 )
Merge PR #12342: Direct URL for triggering a pipeline with SKIP_DOCKER=false. (547a384 )
SkySkimmer pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
[universes] [api] Provide UState.from_env (c8e7ffe )
Merge PR #12354: [universes] [api] Provide UState.from_env (7163b75 )
SkySkimmer pushed 4 commits to branch master. Commits by ejgallego (3) and SkySkimmer (1).
[declare] Remove dead code in prepare_obligation (e12716e )
[declare] Minor tweaks in prepare_obligation (d97499e )
[declare] Remove unused parameters in prepare_obligation (0643873 )
Merge PR #12356: [declare] Remove unused parameters in prepare_obligation (a87e046 )
SkySkimmer pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
[test-suite] Ensure copies of files are writable (17de81c )
Merge PR #12350: [test-suite] Ensure copies of files are writable (5fcd4fc )
SkySkimmer pushed 2 commits to branch master. Commits by JasonGross (1) and SkySkimmer (1).
[ci] Add mit-plv/engine-bench (e7908df )
Merge PR #12359: [ci] Add mit-plv/engine-bench (9a8e6cb )
cpitclaudel pushed 2 commits to branch master. Commits by Zimmi48 (1) and cpitclaudel (1).
Adapt the documentation to the move from Gitter to Zulip. (192d4bd )
Merge PR #12377: Adapt the documentation to the move from Gitter to Zulip. (5bf1609 )
SkySkimmer pushed 4 commits to branch master. Commits by JasonGross (3) and SkySkimmer (1).
Use pagination in fetching the number of reviews (9cc5075 )
[merge-pr.sh] Follow next links instead (19a231a )
[merge-pr] Use a simpler method to get all pages (8263c13 )
Merge PR #12316: Use pagination in fetching the number of reviews (7c17979 )
SkySkimmer pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
[topfmt] Set formatter + flush fix (fb0caf1 )
Merge PR #12358: [topfmt] Set formatter + flush fix (0aedb0c )
SkySkimmer pushed 3 commits to branch master. Commits by SkySkimmer (1), Zimmi48 (1) and ejgallego (1).
[ci] [docker] Bump ocamlformat and dune (a89ea61 )
Bump nixpkgs to get ocamlformat 0.14.2. (7e8897a )
Merge PR #12364: [ci] [docker] Bump ocamlformat and dune (fe15084 )
SkySkimmer pushed 2 commits to branch master. Commits by JasonGross (1) and SkySkimmer (1).
Print a newline at the end of timing tables (0f8de9b )
Merge PR #12368: Print a newline at the end of timing tables (d84cbac )
SkySkimmer pushed 5 commits to branch master. Commits by ejgallego (4) and SkySkimmer (1).
[nit] Remove Declare.Obls.err_not_transp
(70c4c51 )
[declare] [nit] Use proper type alias for in ProgramDecl interface (bb46ed3 )
[obligations] declare_obligation
now takes an UState.t
(7db54ab )
[obligations] [nit] Refactor obligation printing. (e0dc8cb )
Merge PR #12371: [obligations] Minor refactoring (90389df )
This topic was moved here from #Coq devs & plugin devs > Github Push Notifications by Théo Zimmermann
ejgallego pushed 2 commits to branch v8.12. Commits by Zimmi48 (1) and ejgallego (1).
Use pinned commits in dev/ci/ci-user-overlays.sh. (e0b1d9a )
Merge PR #12355: [8.12] Use pinned commits in dev/ci/ci-user-overlays.sh. (701d713 )
ppedrot pushed 2 commits to branch master. Commits by ppedrot (1) and proux01 (1).
[primitive floats] Add low level hexadecimal printing (04e22ab )
Merge PR #11986: [primitive floats] Add low level printing (7e09ee6 )
ppedrot pushed 4 commits to branch master. Commits by herbelin (3) and ppedrot (1).
Fixes #12233 (wrong printing env in presence of match branches eta-expansion). (1e80f73 )
Ssrmatching: Hack to circumvent a hack. (8f5e1e1 )
Added change log. (30ccbef )
Merge PR #12295: Fixes #12233: printing environment corrupted with eta-expansion of "match" branches (ea9463b )
ppedrot pushed 5 commits to branch master. Commits by proux01 (4) and ppedrot (1).
[coqchk] Change list to set (fff8086 )
[coqchk] Fix #5030 (f44ec99 )
[coqchk] Add test (4bab696 )
[coqchk] Improve previous heuristic. (5b2e6c3 )
Merge PR #12076: [coqchk] Fix #5030 (coqchk reports names from opaque modules as axioms) (127c61a )
ejgallego pushed 2 commits to branch v8.12. Commits by ejgallego (1) and ppedrot (1).
Tweak the OCaml version used to generate the MacOS package. (00368b4 )
Merge PR #12363: [8.12] Tweak the OCaml version used to generate the MacOS package. (82c5cc1 )
Zimmi48 pushed 26 commits to branch v8.12. Commits by Zimmi48 (11), proux01 (4), SkySkimmer (3) and others (8).
Bump fiat-crypto for compatibility with #12358. (50ee793 )
[topfmt] Set formatter + flush fix (cdd7c6e )
Backport PR #12358: [topfmt] Set formatter + flush fix (ef7a157 )
test-suite: fix bug causing unit tests to be skipped (1e03b02 )
Fix proof_diffs_test.ml (efda845 )
Revert "[test] unit tests for ide/coq_lex.ml" + makefile support (093f339 )
[azure OSX] Export OCAMLPATH so test-suite sees OCaml libs (f2126a1 )
Backport PR #12289: test-suite: fix bug causing unit tests to be skipped (84061b4 )
[test-suite] Ensure copies of files are writable (cb39edb )
Backport PR #12350: [test-suite] Ensure copies of files are writable (3776c11 )
Print a newline at the end of timing tables (e866c53 )
Backport PR #12368: Print a newline at the end of timing tables (ca06cf2 )
Fixes #12233 (wrong printing env in presence of match branches eta-expansion). (dfb0b42 )
Ssrmatching: Hack to circumvent a hack. (95afb6d )
Added change log. (18d6a50 )
Backport PR #12295: Fixes #12233: printing environment corrupted with eta-expansion of "match" branches (3392077 )
[coqchk] Change list to set (1090241 )
[coqchk] Fix #5030 (c18a49e )
[coqchk] Add test (a9e6813 )
[coqchk] Improve previous heuristic. (c16ff69 )
[and 6 more commit(s)]
Zimmi48 pushed 2 commits to branch master. Commits by Zimmi48 (1) and jfehrle (1).
Omit volumnious Latex messages (e6ae2dc )
Merge PR #12379: Omit voluminous Latex warnings (2b8f1c3 )
JasonGross pushed 3 commits to branch master. Commits by Zimmi48 (2) and JasonGross (1).
[backport-pr] Select correct remote of the master branch. (59e7a45 )
[dev/tools] Fix #12314: do not die silently if branch has no remote. (dbefe07 )
Merge PR #12392: [backport-pr] Select correct remote of the master branch. (16e0877 )
Zimmi48 pushed 2 commits to branch master. Commits by Zimmi48 (1) and mdempsky (1).
Fix hyperlinks in changes.rst (a4f6fdd )
Merge PR #12403: Fix hyperlinks in changes.rst (85694cf )
ppedrot pushed 3 commits to branch master. Commits by SkySkimmer (2) and ppedrot (1).
ppedrot pushed 2 commits to branch master. Commits by gasparattila (1) and ppedrot (1).
Delay evaluating arguments of the "exists" tactic (85d7906 )
Merge PR #12366: Delay evaluating arguments of the "exists" tactic (8b3ce74 )
SkySkimmer pushed 2 commits to branch master. Commits by JasonGross (1) and SkySkimmer (1).
Fix an uncaught python exception in timing (7731b88 )
Merge PR #12388: Fix an uncaught python exception in timing (7a72315 )
SkySkimmer pushed 2 commits to branch master. Commits by JasonGross (1) and SkySkimmer (1).
dev/tools/make-changelog.sh now asks about fixed bugs (09a4ffe )
Merge PR #12410: dev/tools/make-changelog.sh now asks about fixed bugs (1eb5f05 )
Zimmi48 pushed 11 commits to branch v8.12. Commits by Zimmi48 (7), JasonGross (1), gasparattila (1) and others (2).
[backport-pr] Select correct remote of the master branch. (3570bfe )
[dev/tools] Fix #12314: do not die silently if branch has no remote. (3ae1ebd )
Backport PR #12392: [backport-pr] Select correct remote of the master branch. (4d77ba2 )
Omit volumnious Latex messages (a3a46f4 )
Backport PR #12379: Omit voluminous Latex warnings (ec34cc6 )
Fix hyperlinks in changes.rst (9b80607 )
Backport PR #12403: Fix hyperlinks in changes.rst (1dad1a1 )
Delay evaluating arguments of the "exists" tactic (e13a3d9 )
Backport PR #12366: Delay evaluating arguments of the "exists" tactic (8c9f9bd )
Fix an uncaught python exception in timing (62815da )
Backport PR #12388: Fix an uncaught python exception in timing (dc8f5b2 )
ejgallego pushed 2 commits to branch master. Commits by Zimmi48 (1) and ejgallego (1).
Fix output tests for location errors when running in async mode. (488cd01 )
Merge PR #12408: Fix output tests for location errors when running in async mode. (35e1757 )
gares pushed 3 commits to branch master. Commits by Mbodin (2) and gares (1).
Promoting COQLIBINSTALL and COQDOCINSTALL in coq_makefile to the parameters section. (9514c7d )
Adding changelog. (4bdfeb3 )
Merge PR #12389: Small coq_makefile improvement. (a102a80 )
Zimmi48 pushed 3 commits to branch master. Commits by ppedrot (2) and Zimmi48 (1).
Remove the prolog tactic. (a181ea2 )
Add a changelog. (6dab02e )
Merge PR #12399: Remove the prolog tactic. (7c21e56 )
ejgallego pushed 3 commits to branch master. Commits by herbelin (2) and ejgallego (1).
Fixing compilation with -natdynlink no. (5e0907d )
Adding missing DECLARE PLUGIN so that compilation with -natdynlink no works. (19c8ac8 )
Merge PR #12421: Fixes for compilation without native dynlink (d75b889 )
SkySkimmer pushed 10 commits to branch master. Commits by ejgallego (9) and SkySkimmer (1).
[declare] Simplify exported type of definition_entry (946c6c7 )
[declare] Don't expose internal parameter obls (09891ac )
[nit] Remove unused exported error message in obligations (baef982 )
[declare] Turn restrict_ucontext hack into an internal parameter (d9d4dcb )
[declare] Nit on errors. (e1a3216 )
[declare] Factor out universe computation in close_proof (3b38364 )
[declare] Split univs_deferred in close_proof (7661029 )
[declare] Factor common universe computation in close proof. (afa3d2f )
[declare] Split univs_poly_private in close_proof (288110c )
Merge PR #12393: [declare] Miscellaneous nits from my main dev tree (831e901 )
SkySkimmer pushed 2 commits to branch master. Commits by JasonGross (1) and SkySkimmer (1).
[ci] Split fiat-crypto into non-OCaml and OCaml (f427613 )
Merge PR #12431: [ci] Split fiat-crypto into non-OCaml and OCaml (4270ed3 )
ejgallego pushed 3 commits to branch master. Commits by herbelin (2) and ejgallego (1).
Fixes #12418 (inference of return clause meets assert false). (22d0e5c )
Change log for #12422. (dec5edf )
Merge PR #12422: Fixes #12418: an assert false in inference of return clause (558e20c )
ejgallego pushed 8 commits to branch master. Commits by Zimmi48 (7) and ejgallego (1).
Fix changelog for #11986. (1f04d9e )
Release notes for 8.12. (2f0a89e )
Changelog entries for the 8.12 changes to the reference manual. (296eef0 )
[changelog/8.12] Split misc entries out in more relevant sections. (ce3de8c )
[changelog/8.12] Use sections and provide a local TOC. (80fb192 )
[changelog/8.12] Wording improvements. (29d1594 )
Add more changelog entries which have been backported to v8.12. (f69bb33 )
Merge PR #12396: Release notes 8.12 (a1fa186 )
ejgallego pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
Require in Section: warning is now about fragility not deprecation. (083ab9f )
Merge PR #11974: Require in Section: warning is now about fragility not deprecation. (d495815 )
gares pushed 4 commits to branch master. Commits by Zimmi48 (3) and gares (1).
Remove command-line options that do not exist anymore. (2d9988d )
Fix worker handling of command-line options that are already included in initial state. (c684557 )
Fix usage of -rifrom, -refrom. (850e363 )
Merge PR #12412: Reduce options passed to workers (db768e6 )
Zimmi48 pushed 24 commits to branch v8.12. Commits by Zimmi48 (18), herbelin (4), JasonGross (1) and others (1).
Release notes for 8.12. (4391a23 )
Changelog entries for the 8.12 changes to the reference manual. (9886fbf )
[changelog/8.12] Split misc entries out in more relevant sections. (e7c74fc )
[changelog/8.12] Use sections and provide a local TOC. (d55395f )
[changelog/8.12] Wording improvements. (2b3cdf8 )
Add more changelog entries which have been backported to v8.12. (a76d7c9 )
Backport PR #12396: Release notes 8.12 (6bb5ffa )
Bump fiat-crypto pin to be able to use new targets in CI. (0a27c5e )
[ci] Split fiat-crypto into non-OCaml and OCaml (44a8980 )
Backport PR #12431: [ci] Split fiat-crypto into non-OCaml and OCaml (38899a5 )
Remove command-line options that do not exist anymore. (cd92d55 )
Fix worker handling of command-line options that are already included in initial state. (f27a850 )
Fix usage of -rifrom, -refrom. (514cd2d )
Backport PR #12412: Reduce options passed to workers (3b29a88 )
Fix output tests for location errors when running in async mode. (839a054 )
Backport PR #12408: Fix output tests for location errors when running in async mode. (179c41f )
Fixing compilation with -natdynlink no. (5029e9d )
Adding missing DECLARE PLUGIN so that compilation with -natdynlink no works. (db1f565 )
Backport PR #12421: Fixes for compilation without native dynlink (1fb2a48 )
Fixes #12418 (inference of return clause meets assert false). (42dcec8 )
[and 4 more commit(s)]
gares pushed 2 commits to branch master. Commits by gares (1) and maximedenes (1).
Move CoqIDE to its own folder (3302161 )
Merge PR #12337: Move CoqIDE to its own folder (42e9c71 )
gares pushed 2 commits to branch master. Commits by gares (1) and herbelin (1).
Coq_makefile: adding a dependency of .coqdeps on _CoqProject. (c803c10 )
Merge PR #12427: Add a dependency of coq_makefile's coqdep target into _CoqProject (5ea6ef7 )
herbelin pushed 6 commits to branch master. Commits by ppedrot (5) and herbelin (1).
Some wrapper cleanup around eauto. (5488b4a )
Make explicit the computation of lists of goals in eauto. (645727a )
Factor the computation of head constant in Eauto resolution. (a20d537 )
Simplify Eauto.e_trivial_resolve. (4f2bca1 )
Enforce statically the invariant that a goal comes with its database in eauto. (13b1000 )
Merge PR #12419: Various cleanups in eauto (e766d31 )
SkySkimmer pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
[declare] Hide internals of variable declaration entries. (6fe12fd )
Merge PR #12440: [declare] Hide internals of variable declaration entries. (0ae2017 )
maximedenes pushed 4 commits to branch master. Commits by ppedrot (3) and maximedenes (1).
Move the cbn reduction to its own file, and simplify the RAKAM accordingly. (7a8c400 )
Further cleanup. (4d98718 )
Move the Cbn module to tactics/. (497a300 )
Merge PR #11707: Split the Reductionops machine from the cbn one (0379ab6 )
Zimmi48 pushed 1 commit to branch document-sphinx-3-incompatibility.
Document incompatibility with Sphinx 3. (b6c9403 )
Zimmi48 deleted the branch document-sphinx-3-incompatibility.
ejgallego pushed 3 commits to branch master. Commits by Zimmi48 (2) and ejgallego (1).
Fix version switcher when building with Dune. (4f4ad56 )
Adjust list of versions in version switcher. (2b337fa )
Merge PR #12456: Fix version switcher when building with Dune. (de43053 )
ejgallego pushed 2 commits to branch master. Commits by Zimmi48 (1) and ejgallego (1).
Fix #12280: do not use xindy to avoid build failures on some machines. (19d5ebc )
Merge PR #12397: Fix #12280: do not use xindy to avoid build failures on some machines. (c937f72 )
ejgallego pushed 2 commits to branch master. Commits by Zimmi48 (1) and ejgallego (1).
Fix ONLY_WINDOWS in .gitlab-ci.yml. (2beed70 )
Merge PR #12437: Fix ONLY_WINDOWS in .gitlab-ci.yml. (7bfd2bf )
ejgallego pushed 2 commits to branch master. Commits by Zimmi48 (1) and ejgallego (1).
Document incompatibility with Sphinx 3. (b6c9403 )
Merge PR #12459: Document incompatibility with Sphinx 3. (e36b1c2 )
ejgallego pushed 2 commits to branch master. Commits by Zimmi48 (1) and ejgallego (1).
Add remaining 8.12+beta1 changelog entries. (dd7857c )
Merge PR #12460: Add remaining 8.12+beta1 changelog entries. (2f2d21a )
ejgallego pushed 3 commits to branch master. Commits by Zimmi48 (2) and ejgallego (1).
Document known issue of Proof <term> with PG. (08e73f2 )
Tweak wording. (f47b2ed )
Merge PR #12450: Document known issue of Proof <term> with PG. (e9bba6f )
herbelin pushed 2 commits to branch master. Commits by herbelin (1) and ppedrot (1).
Factorize code in hint declaration. (0d3e83a )
Merge PR #12336: Factorize code in hint declaration. (9c26e58 )
Zimmi48 pushed 6 commits to branch master. Commits by cpitclaudel (4) and Zimmi48 (2).
[sphinx] Remove most pylint warnings (101b98f )
[sphinx] Get rid of anonymous targets (Sphinx 2.3.1 doesn't like them) (c654804 )
[sphinx] Improve the error message printed for duplicate names (51b13de )
[sphinx] Fix #12361 (73d400a )
Fix comment. (20cee60 )
Merge PR #12380: Fix #12361 (indexing issues in the PDF) (d0e4e7e )
Zimmi48 pushed 14 commits to branch v8.12.
Fix version switcher when building with Dune. (cae5695 )
Adjust list of versions in version switcher. (ba20868 )
Backport PR #12456: Fix version switcher when building with Dune. (fa84da6 )
Fix #12280: do not use xindy to avoid build failures on some machines. (7f9c0b1 )
Backport PR #12397: Fix #12280: do not use xindy to avoid build failures on some machines. (9531c68 )
Fix ONLY_WINDOWS in .gitlab-ci.yml. (0b33af6 )
Backport PR #12437: Fix ONLY_WINDOWS in .gitlab-ci.yml. (3399fc0 )
Document incompatibility with Sphinx 3. (91f2372 )
Backport PR #12459: Document incompatibility with Sphinx 3. (93caba9 )
Add remaining 8.12+beta1 changelog entries. (baa5ca0 )
Backport PR #12460: Add remaining 8.12+beta1 changelog entries. (235f483 )
Document known issue of Proof <term> with PG. (5fa88e7 )
Tweak wording. (64ea579 )
Backport PR #12450: Document known issue of Proof <term> with PG. (468d891 )
Zimmi48 pushed 6 commits to branch v8.12. Commits by cpitclaudel (4) and Zimmi48 (2).
[sphinx] Remove most pylint warnings (0ea7cb3 )
[sphinx] Get rid of anonymous targets (Sphinx 2.3.1 doesn't like them) (4a3ea3e )
[sphinx] Improve the error message printed for duplicate names (d500ce7 )
[sphinx] Fix #12361 (56d0010 )
Fix comment. (e720add )
Backport PR #12380: Fix #12361 (indexing issues in the PDF) (1b55bd6 )
cpitclaudel pushed 2 commits to branch master. Commits by cpitclaudel (1) and jfehrle (1).
Match only a single line as the coqtop prompt (c964091 )
Merge PR #12473: Match only a single line as the coqtop prompt in coqtop:: directive (aad87d7 )
ejgallego pushed 2 commits to branch master. Commits by Zimmi48 (1) and ejgallego (1).
Fix Flocq build in Windows add-ons. (d930f65 )
Merge PR #12451: Fix Flocq build on Windows. (61744ac )
Zimmi48 pushed 2 commits to branch master. Commits by Zimmi48 (1) and cpitclaudel (1).
[sphinx] Fix regexp used in coqdomain.CoqtopBlocksTransform.split_lines (7612610 )
Merge PR #12477: [sphinx] Fix regexp used in coqdomain.CoqtopBlocksTransform.split_lines (3b030bf )
ppedrot pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Fix uncaught NotArity in inductive type (bc842a9 )
Merge PR #12471: Fix uncaught NotArity in inductive type (522a1d3 )
ejgallego pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
Don't suggest Proof using when no section variables (10e90e2 )
Merge PR #12480: Don't suggest Proof using when no section variables (c0f4d0f )
Zimmi48 pushed 6 commits to branch v8.12. Commits by Zimmi48 (4), cpitclaudel (1) and jfehrle (1).
Match only a single line as the coqtop prompt (656df4c )
Backport PR #12473: Match only a single line as the coqtop prompt in coqtop:: directive (01477d8 )
[sphinx] Fix regexp used in coqdomain.CoqtopBlocksTransform.split_lines (7cebf06 )
Backport PR #12477: [sphinx] Fix regexp used in coqdomain.CoqtopBlocksTransform.split_lines (91c065b )
Fix Flocq build in Windows add-ons. (679a6c2 )
Backport PR #12451: Fix Flocq build on Windows. (723ecfe )
Zimmi48 pushed 4 commits to branch v8.12. Commits by SkySkimmer (2) and Zimmi48 (2).
Fix uncaught NotArity in inductive type (791734d )
Backport PR #12471: Fix uncaught NotArity in inductive type (3be0565 )
Don't suggest Proof using when no section variables (2cb2f63 )
Backport PR #12480: Don't suggest Proof using when no section variables (3080a8e )
Zimmi48 pushed 2 commits to branch master. Commits by Zimmi48 (1) and ejgallego (1).
[ci] [overlays] Pin unicoq to a stable version. (6e09f3a )
Merge PR #12482: [ci] [overlays] Pin unicoq to a stable version. (2e85a6b )
Zimmi48 pushed 2 commits to branch master. Commits by Zimmi48 (1) and mattam82 (1).
Summary of changes for 8.12 (4167ef6 )
Merge PR #12462: Summary of changes for 8.12 (10e126b )
Zimmi48 pushed 7 commits to branch master. Commits by jfehrle (6) and Zimmi48 (1).
Refactor SELF code for clarity (376425b )
Add MOVEALLBUT operation (485054a )
Report an error for empty (sub)productions (12540e1 )
Add NOTINRSTS nonterminal to suppress messages (11baeee )
Make automatic name generation for directives more consistent: (6a76e43 )
Convert Ltac chapter to prodn (27d6686 )
Merge PR #12103: Convert Ltac chapter to prodn (4642ce1 )
VincentSe pushed 2 commits to branch master. Commits by MSoegtropIMC (1) and VincentSe (1).
CReal: changed epsilon for modulus of convergence from 1/n to 2^z (3d775bd )
Merge PR #12186: CReal: changed epsilon for modulus of convergence from 1/n to 1/2^n (95fb6a9 )
silene pushed 3 commits to branch master. Commits by proux01 (2) and silene (1).
Fix 12483 (8ecdb85 )
Update dev/doc/critical-bugs (9c76e6b )
Merge PR #12484: Fix #12483 Incorrect specification of PrimFloat.leb (95be052 )
Zimmi48 pushed 12 commits to branch v8.12. Commits by jfehrle (6), Zimmi48 (3), proux01 (2) and others (1).
Summary of changes for 8.12 (3cbc380 )
Backport PR #12462: Summary of changes for 8.12 (e4ec975 )
Refactor SELF code for clarity (0a9a66e )
Add MOVEALLBUT operation (fe3741a )
Report an error for empty (sub)productions (f9125b5 )
Add NOTINRSTS nonterminal to suppress messages (ba425b5 )
Make automatic name generation for directives more consistent: (a38b073 )
Convert Ltac chapter to prodn (3ccd52a )
Backport PR #12103: Convert Ltac chapter to prodn (6c14a25 )
Fix 12483 (a75959a )
Update dev/doc/critical-bugs (464c3a5 )
Backport PR #12484: Fix #12483 Incorrect specification of PrimFloat.leb (6c30332 )
cpitclaudel pushed 2 commits to branch master. Commits by Zimmi48 (1) and cpitclaudel (1).
Update changelog for 8.12+beta1. (65a64e6 )
Merge PR #12491: Update changelog for 8.12+beta1. (c077db4 )
ppedrot pushed 2 commits to branch master. Commits by jfehrle (1) and ppedrot (1).
Remove info tactic, deprecated in 8.5 (044f76c )
Merge PR #12423: Remove info tactic, deprecated in 8.5 (5611f23 )
ppedrot pushed 2 commits to branch master. Commits by gasparattila (1) and ppedrot (1).
Fix #12442: Confusing error message when the intro pattern of "apply in" fails (c3dc9c5 )
Merge PR #12443: Fix #12442: Confusing error message when the intro pattern of "apply in" fails (149d960 )
ejgallego pushed 6 commits to branch master. Commits by Zimmi48 (3), MSoegtropIMC (2) and ejgallego (1).
Windows: fix menhir and coq-menhirlib build for latest version. (628ed59 )
Windows: fix build of Gappa C++ tool (3b556e1 )
Fix Coquelicot build in Windows add-ons. (85999bc )
Call autoreconf in interval, flocq and gappa-plugin. (e2afb5b )
Fix the build of Elpi by calling Dune directly. (ba8c793 )
Merge PR #12492: Fix Windows addons. (965c095 )
ejgallego pushed 4 commits to branch master. Commits by Zimmi48 (3) and ejgallego (1).
Minor improvements to the section on basics. (fcbae04 )
Minor improvements to the section on sorts. (7fa123e )
Merge sections on functions and function types. (daddc14 )
Merge PR #12481: Minor improvements to the sections on basics and sorts. (55d1ea3 )
Zimmi48 pushed 14 commits to branch v8.12. Commits by Zimmi48 (11), MSoegtropIMC (2) and gasparattila (1).
Update changelog for 8.12+beta1. (d7bdcaa )
Backport PR #12491: Update changelog for 8.12+beta1. (753d297 )
Minor improvements to the section on basics. (0fe8ea9 )
Minor improvements to the section on sorts. (61f28dd )
Merge sections on functions and function types. (bdd5913 )
Backport PR #12481: Minor improvements to the sections on basics and sorts. (61b048a )
Fix #12442: Confusing error message when the intro pattern of "apply in" fails (c8e0614 )
Backport PR #12443: Fix #12442: Confusing error message when the intro pattern of "apply in" fails (5919812 )
Windows: fix menhir and coq-menhirlib build for latest version. (6a7513f )
Windows: fix build of Gappa C++ tool (1c2f5c7 )
Fix Coquelicot build in Windows add-ons. (fdc0dc1 )
Call autoreconf in interval, flocq and gappa-plugin. (ad5afd9 )
Fix the build of Elpi by calling Dune directly. (304109e )
Backport PR #12492: Fix Windows addons. (8587ea4 )
maximedenes pushed 2 commits to branch master. Commits by ejgallego (1) and maximedenes (1).
[dune] [dbg] Fix coqide target after CoqIDE move. (7fb7c9e )
Merge PR #12498: [dune] [dbg] Fix coqide target after CoqIDE move. (96d206a )
ejgallego pushed 6 commits to branch v8.12. Commits by Zimmi48 (3), MSoegtropIMC (2) and ejgallego (1).
CI/Windows: Adjust CompCert version and build instructions (02af003 )
Windows: Adjust version of VST and enable platform friendly VST build (5e9804c )
Revert "Windows: switch OCaml to 4.08.1" (1a3a6b3 )
Carefully select which versions of add-ons are included in the Windows installer. (d29ced0 )
Enable all addons in release branch. (a11c796 )
Merge PR #12415: [v8.12] Carefully select which versions of add-ons are included in the Windows installer. (dad84cd )
ejgallego pushed 2 commits to branch v8.12. Commits by Zimmi48 (1) and ejgallego (1).
Bump version number to 8.12+beta1. (fd4dc52 )
Merge PR #12500: Bump version number to 8.12+beta1. (393e1cd )
gares pushed 4 commits to branch master. Commits by ejgallego (3) and gares (1).
[declare] Remove some unused fix_exn
(0e2897d )
[stm] Simplify logic involving forced futures. (558b24c )
[test-suite] [stm] Interactive test case for fail-on-qed. (213c928 )
Merge PR #12357: [declare] Remove some unused fix_exn
(13e8d04 )
Zimmi48 pushed 2 commits to branch v8.12.
Bump Coq-Elpi to not include memory intensive tests. (d4f06b7 )
Merge PR #12501: Coq-Elpi patch to remove memory-intensive test. (15a5797 )
Zimmi48 pushed tag V8.12+beta1.
Zimmi48 pushed 1 commit to branch v8.12.
First commit after V8.12+beta1. (905d6fc )
vbgl pushed 2 commits to branch master. Commits by Zimmi48 (1) and vbgl (1).
[dev/ci/nix] Support for building the Gappa plugin. (89d6507 )
Merge PR #12494: [dev/ci/nix] Support for building the Gappa plugin. (61b63e0 )
maximedenes pushed 5 commits to branch master. Commits by fajb (4) and maximedenes (1).
[micromega] native support for boolean operators (f8e91cb )
Update theories/micromega/ZifyBool.v (13f0909 )
fix according to review by @pi8027 (5017d52 )
Update zify documentation (12e9f7e )
Merge PR #11906: [micromega] native support for boolean operators (90345eb )
Zimmi48 pushed 2 commits to branch master. Commits by Zimmi48 (1) and beta-ziliani (1).
updated ci for unicoq (d008763 )
Merge PR #12509: updated ci for unicoq (a006765 )
ppedrot pushed the branch binary-macOS-8.11.2.
gares pushed 2 commits to branch master. Commits by ejgallego (1) and gares (1).
[toplevel] Annotate tailcall functions (ce26ccf )
Merge PR #12506: [toplevel] Annotate tailcall functions (fd173d5 )
CohenCyril pushed 4 commits to branch master. Commits by gares (3) and cyrilcohen (1).
[ssr] remove catch all (73c3dd1 )
[ssr] fix env handling in error message (fix #12507) (8cbb01a )
make the linter happy (22ea81e )
Merge PR #12508: Fix #12507 Anomaly when using a ssreflect reflect
view (6499de1 )
Zimmi48 pushed 2 commits to branch v8.12.
Bump Gappa plugin to use latest release and remove the compatibility patch. (f71e6ec )
Merge PR #12511: [v8.12] Bump Gappa plugin to use latest release and remove the compatibility patch (432d2b4 )
Zimmi48 pushed 2 commits to branch master. Commits by Blaisorblade (1) and Zimmi48 (1).
tactics.rst: readd cbv
(5fbbf2f )
Merge PR #12536: tactics.rst: fix typo — readd cbv
to title of its section (33e763a )
Zimmi48 pushed 4 commits to branch v8.12. Commits by Zimmi48 (3) and proux01 (1).
[CI] Update paramcoq branch to v8.12 (9000f3c )
Bump the version of interval. (9ef6034 )
Merge PR #12535: [v8.12] Bump interval (dda4715 )
Merge PR #12533: [CI] Update paramcoq branch to v8.12 (48879ac )
Zimmi48 pushed 6 commits to branch v8.12. Commits by gares (3), Zimmi48 (2) and Blaisorblade (1).
[ssr] remove catch all (fe0290d )
[ssr] fix env handling in error message (fix #12507) (7050773 )
make the linter happy (189d90c )
Backport PR #12508: Fix #12507 Anomaly when using a ssreflect reflect
view (229e80f )
tactics.rst: readd cbv
(28356df )
Backport PR #12536: tactics.rst: fix typo — readd cbv
to title of its section (586929a )
ppedrot deleted the branch binary-macOS-8.11.2.
SkySkimmer pushed 4 commits to branch master. Commits by ppedrot (3) and SkySkimmer (1).
Do not reallocate named_context_val of the pretyping environment. (9ad3bb7 )
Share the identity instance in pretyping environments. (9cff67c )
Try to preserve more sharing in nf_evars_and_universes_opt_subst. (695ca08 )
Merge PR #12502: Preserve sharing in evar instances (72b25f1 )
SkySkimmer pushed 3 commits to branch master. Commits by ppedrot (2) and SkySkimmer (1).
Check duplicity of constructor names in an algorithmically efficient way. (e67f4a4 )
Use an efficient data structure for VM compilation indexing. (3b81ff4 )
Merge PR #12531: Fast inductive compilation (6cdccde )
anton-trunov pushed 2 commits to branch master. Commits by Blaisorblade (1) and anton-trunov (1).
Fix #12406: fix Coq type error in dependent induction's Ltac (0df0e9c )
Merge PR #12407: Fix #12406: fix Coq type error in dependent induction's Ltac (43dba0d )
cpitclaudel pushed 2 commits to branch master. Commits by Zimmi48 (1) and cpitclaudel (1).
Add index for coqdoc. (5f9572b )
Merge PR #12559: Add index for coqdoc. (3f8629c )
herbelin pushed 11 commits to branch master. Commits by ppedrot (10) and herbelin (1).
Factorize hint flags in Class_tatcis.make_make_resolve_hyp. (6c4ecea )
Do not be verbose when declaring subclass hints. (ca6dd28 )
Do not export flags in Hints.make_resolves. (f66bd46 )
Do not export Hints.make_extern. (7ac18ed )
Remove dead code in the Hints API. (2a24a66 )
Opacify the type of hint metadata. (21b4e41 )
Remove access to hint section variables. (437f86a )
Wrap the content of full hints into a record. (9eca7cc )
Move the hint polymorphic status to the hint instance. (c00a369 )
Add overlays. (1d64f9d )
Merge PR #12505: Cleanup the Hints API (95dc295 )
ejgallego pushed 2 commits to branch master. Commits by ejgallego (1) and tchajed (1).
[ci] Use a tested branch of Perennial (21cc4cb )
Merge PR #12546: [ci] Use a tested branch of Perennial (257564b )
SkySkimmer pushed 2 commits to branch master. Commits by JasonGross (1) and SkySkimmer (1).
Add a generated file to .gitignore (6e60934 )
Merge PR #12555: Add test-suite/redirect_test.out file to .gitignore (bb543b4 )
SkySkimmer pushed 2 commits to branch master. Commits by SkySkimmer (1) and herbelin (1).
Slight improvement in naming existential variables. (f12b5b2 )
Merge PR #12434: Slight improvement in naming dependent existential variables in goals (b34680b )
herbelin pushed 1 commit to branch master+elementary-properties-IZR.
Elementary properties about IZR for generic use. (9dc1f1f )
herbelin deleted the branch master+elementary-properties-IZR.
herbelin pushed 4 commits to branch master. Commits by ppedrot (3) and herbelin (1).
Remove dead code in autorewrite. (948d8bc )
Code simplification in Autorewrite. (31cbaf0 )
Use evar clauses instead of meta clauses in Autorewrite hint registration. (1ef9819 )
Merge PR #12520: Cleanup the autorewrite implementation (2139991 )
SkySkimmer pushed 2 commits to branch master. Commits by SkySkimmer (1) and herbelin (1).
Elementary properties about IZR for generic use. (9dc1f1f )
Merge PR #8796: Elementary properties about IZR for generic use (34e62d0 )
fajb pushed 2 commits to branch master. Commits by fajb (1) and pi8027 (1).
Add a pre-hook mechanism for the zify
tactic (8095d7d )
Merge PR #12552: Add a pre-hook mechanism for the zify
tactic (700918a )
maximedenes pushed 2 commits to branch master. Commits by SkySkimmer (1) and maximedenes (1).
Fix glob_sort_family for SProp (3083eac )
Merge PR #12530: Fix glob_sort_family for SProp (5d65a66 )
MSoegtropIMC pushed 2 commits to branch master. Commits by MSoegtropIMC (1) and vbgl (1).
CoqIDE: accept to open files with invalid names (518d92d )
Merge PR #12562: CoqIDE: accept to open files with invalid names (25ece32 )
Zimmi48 pushed 13 commits to branch v8.12. Commits by Zimmi48 (7), ppedrot (2), Blaisorblade (1) and others (3).
Check duplicity of constructor names in an algorithmically efficient way. (c1e4016 )
Use an efficient data structure for VM compilation indexing. (79b10ac )
Backport PR #12531: Fast inductive compilation (eb1e591 )
Fix #12406: fix Coq type error in dependent induction's Ltac (97061a9 )
Backport PR #12407: Fix #12406: fix Coq type error in dependent induction's Ltac (d807a10 )
Add index for coqdoc. (72f24b8 )
Backport PR #12559: Add index for coqdoc. (b2df824 )
Add a generated file to .gitignore (266deee )
Backport PR #12555: Add test-suite/redirect_test.out file to .gitignore (eceafd7 )
Fix glob_sort_family for SProp (546e9de )
Backport PR #12530: Fix glob_sort_family for SProp (da7a2e2 )
CoqIDE: accept to open files with invalid names (35bd89c )
Backport PR #12562: CoqIDE: accept to open files with invalid names (16984af )
SkySkimmer pushed 2 commits to branch master. Commits by JasonGross (1) and SkySkimmer (1).
[ci] Add coq-community/coq-performance-tests (7ea8f82 )
Merge PR #12577: [ci] Add coq-community/coq-performance-tests (3ba88c9 )
mattam82 pushed 3 commits to branch master. Commits by ppedrot (2) and mattam82 (1).
Use the unification result for eauto's eapply. (189f418 )
Add a test for the strange behaviour encountered with this change. (c1f7048 )
Merge PR #12532: Use the unification result for eauto's eapply. (0465e99 )
ejgallego pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
Revert "[opam] Don't disable native compute in opam.dev file" (e22a741 )
Merge PR #12550: Fix configure usage in .opam (82485e9 )
gares pushed 2 commits to branch master. Commits by gares (1) and maximedenes (1).
Fix #4459 by improving par:
error message (f67a09a )
Merge PR #12517: Fix #4459 by improving par:
error message (ba355fb )
ejgallego pushed 2 commits to branch master. Commits by ejgallego (1) and ppedrot (1).
Remove the catchable-exception related functions. (ec15eb5 )
Merge PR #12580: Remove the catchable-exception related functions. (88e7e1d )
ejgallego pushed 6 commits to branch master. Commits by ppedrot (5) and ejgallego (1).
Remove dead code in branch_args. (43b1742 )
Remove all uses of clenv_unique_resolver. (b89584b )
Merge Clenvtac into Clenv. (34aeda3 )
Actually remove internal API from the Clenv mli. (96eab2e )
Simplify Clenv.clenv_pose_metas_as_evars. (d46c2dc )
Merge PR #12579: Simplify Clenv API (7b50daa )
ejgallego pushed 3 commits to branch master. Commits by JasonGross (2) and ejgallego (1).
Add back fiat-crypto-legacy to the CI (f9057bd )
[ci] [fiat-crypto-legacy] allow_failure: true (40308a1 )
Merge PR #12554: Add back fiat-crypto-legacy to the CI (d7d3c70 )
Zimmi48 pushed 2 commits to branch v8.12.
Bump Equation to 1.2.2 and UniCoq to 1.4. (edc80fc )
Merge PR #12544: [v8.12] Bump Equation to 1.2.2 and UniCoq to 1.4. (2622d48 )
Zimmi48 pushed 2 commits to branch master. Commits by Zimmi48 (1) and lilred (1).
Mention VSCoq with respect to _CoqProject (84461cb )
Merge PR #12598: Mention VSCoq with respect to _CoqProject (427fb92 )
Zimmi48 pushed 4 commits to branch v8.12. Commits by Zimmi48 (2), SkySkimmer (1) and maximedenes (1).
Revert "[opam] Don't disable native compute in opam.dev file" (c86f7dd )
Backport PR #12550: Fix configure usage in .opam (aace63a )
Fix #4459 by improving par:
error message (c82f464 )
Backport PR #12517: Fix #4459 by improving par:
error message (6fcc943 )
SkySkimmer pushed 2 commits to branch master. Commits by JasonGross (1) and SkySkimmer (1).
[test-suite] Fix dependencies of modules/ files (9690b13 )
Merge PR #12583: [test-suite] Fix dependencies of modules/ files (c9ca432 )
SkySkimmer pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
[ci] [ocaml] Track OCaml 4.12 (8d595f4 )
Merge PR #12518: [ci] [ocaml] Track OCaml 4.12 (6e5fee1 )
SkySkimmer pushed 29 commits to branch master. Commits by ejgallego (28) and SkySkimmer (1).
[declare] Stronger typing for start_proof (f77743c )
[declare] Move proof information to declare. (43d381a )
[declare] Remove mutual internals from Info.t structure. (2ac5353 )
[declare] Remove Lemmas module (671004a )
[declare] Refactor constant information into a record. (1f121eb )
[declare] Make ProgramDecl.t abstract (7d183d8 )
[declare] [api] Removal of deprecated functions (d83e95c )
[declare] [api] Removal of duplicated type aliases. (a6d663c )
[declare] Move udecl to Info structure. (b143d12 )
[declare] Reify Proof.t API into the Proof module. (030bb57 )
[declare] [api] Modify logical presentation of declare interfaces (c09871d )
[declare] [compat] Remove exception alias. (6291e5b )
[declare] Documentation on obligations (9c58cd6 )
[declare] Nit on interface (ba8db3c )
[declare] Nit on hook call. (22bb101 )
[declare] Refactor analysis and construction of mutual lemmas (c7a62d0 )
[declare] Use Recthm.t in mutual analysis functions (e622379 )
[declare] Nit on regular lemma init. (f72efb3 )
[vernac] Nit refatoring on lemma command interpretation (862e5a0 )
[declare] Improve organization of proof/constant information. (ea8b9e0 )
[and 9 more commit(s)]
gares pushed 2 commits to branch master. Commits by andres-erbsen (1) and gares (1).
ppedrot pushed 2 commits to branch master. Commits by ppedrot (1) and proux01 (1).
Fix #12228 negative integers not accepted in ltac integer_list (d958feb )
Merge PR #12541: Fix #12228 negative integers not accepted in ltac integer_list (1221b56 )
ppedrot pushed 2 commits to branch master. Commits by jlottes (1) and ppedrot (1).
CoqIDE: fix lexing of UTF-8 in quotations like constr:() (a6571b3 )
Merge PR #12570: CoqIDE: fix lexing of UTF-8 in quotations like constr:() (c2b7696 )
Zimmi48 pushed 10 commits to branch v8.12. Commits by Zimmi48 (5), JasonGross (1), andres-erbsen (1) and others (3).
Mention VSCoq with respect to _CoqProject (679aa51 )
Backport PR #12598: Mention VSCoq with respect to _CoqProject (7fd7a81 )
[test-suite] Fix dependencies of modules/ files (734fd00 )
Backport PR #12583: [test-suite] Fix dependencies of modules/ files (85b3b1f )
Update CAMLDONTLINK in CoqMakefile.in (4d87858 )
Backport PR #12604: Update CAMLDONTLINK in CoqMakefile.in (63d6005 )
Fix #12228 negative integers not accepted in ltac integer_list (eb3956a )
Backport PR #12541: Fix #12228 negative integers not accepted in ltac integer_list (54f9afd )
CoqIDE: fix lexing of UTF-8 in quotations like constr:() (8c985bf )
Backport PR #12570: CoqIDE: fix lexing of UTF-8 in quotations like constr:() (12d19da )
ejgallego pushed 3 commits to branch master. Commits by SkySkimmer (2) and ejgallego (1).
Make compute_instance_binders internal to UState (50361dc )
Generate names for anonymous polymorphic universes (ae1acfe )
Merge PR #11977: Generate default names for bound universes of polymorphic definitions (bffe3e8 )
ejgallego pushed 7 commits to branch master. Commits by ppedrot (6) and ejgallego (1).
Remove the deprecated functions from refiner, moving them to Tacticals. (f499083 )
Remove Refiner.refiner. (e5b3551 )
Moving the remaining Refiner functions to Tacmach. (f34dcb9 )
Move the FailError exception from Refiner to Tacticals. (d28af58 )
Refining out the Refiner. (a33f772 )
Adding overlay. (6bb0c6d )
Merge PR #12599: Remove the Refiner module (9c9330f )
ejgallego pushed 2 commits to branch master. Commits by Zimmi48 (1) and ejgallego (1).
Credit Erik Martin-Dorel for work on Docker. (7187b7a )
Merge PR #12596: Credit Erik Martin-Dorel for work on Docker. (119b218 )
SkySkimmer pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
[ci] Disable the OCaml 4.12 target (2168f9e )
Merge PR #12616: [ci] Disable the OCaml 4.12 target (69e798f )
SkySkimmer pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
[ci] [performance-tests] Use a lighter target. (fac794d )
Merge PR #12615: [ci] [performance-tests] Use a lighter target. (d1407a5 )
SkySkimmer pushed 2 commits to branch master. Commits by SkySkimmer (1) and gares (1).
[test-suite] async-proofs off in tests with Fail Timeout (397fb9d )
Merge PR #12605: [test-suite] async-proofs off in tests with Fail Timeout (144d121 )
SkySkimmer pushed 3 commits to branch master. Commits by ejgallego (2) and SkySkimmer (1).
[states] Move States to vernac (e260c20 )
[declaremods] Remove abstraction of imperative module operations (b0169fc )
Merge PR #12504: [states] Move States to vernac (b017e30 )
ppedrot pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Use weak ref to memoize Evarutil.is_ground_env (36faebc )
Merge PR #12618: Use weak ref to memoize Evarutil.is_ground_env (2fc9f27 )
SkySkimmer pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
[state] Consolidate state handling in Vernacstate (4a6a94d )
Merge PR #12620: [state] Consolidate state handling into Vernacstate (e04fbe4 )
SkySkimmer pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Correctly classify variables as being unfoldable in dnet patterns. (93e7eff )
Merge PR #12572: Correctly classify variables as being unfoldable in dnet patterns. (a1835c7 )
ejgallego pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
Cleanup mentions of -as in coqdep usage message (01128e3 )
Merge PR #12614: Cleanup mentions of -as in coqdep usage message (ce1d407 )
ejgallego pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
Fix debug printer for auctx in presence of Anonymous (140f935 )
Merge PR #12628: Fix debug printer for auctx in presence of Anonymous (ce500b3 )
maximedenes pushed 3 commits to branch master. Commits by SkySkimmer (2) and maximedenes (1).
SkySkimmer pushed 2 commits to branch master. Commits by SkySkimmer (1) and maximedenes (1).
Fix #11121: Simultaneous definition of term and notation in custom grammar (53e19f7 )
Merge PR #12523: Fix #11121: Simultaneous definition of term and notation in custom gr… (cf388fd )
ppedrot pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Remove deprecated (in 8.8 #6277) coqchk -I (828b84e )
Merge PR #12613: Remove deprecated (in 8.8 #6277) coqchk -I (9988982 )
MSoegtropIMC pushed 4 commits to branch master. Commits by ppedrot (3) and MSoegtropIMC (1).
Factorize tac2type syntax to fix the parsing of (t1, ..., tn) t. (4e498fa )
Add a test for Ltac2 parsing of parameterized types. (7bec233 )
Add a changelog. (810197a )
Merge PR #12594: Fix ltac2 type parameters (0545c94 )
gares pushed 3 commits to branch master. Commits by MSoegtropIMC (2) and gares (1).
Windows build: use architecture dependent version of windres (5facdb7 )
Windows build: remove patch for windres architecture (6eecb3c )
Merge PR #12641: Windows build: use architecture dependent version of windres (cea10e4 )
SkySkimmer pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Use goal cycling instead of manual evar generation order in internal_cut_rev. (a37b68c )
Merge PR #12622: Use goal cycling instead of manual evar generation order in internal_cut_rev (3244b9c )
ppedrot pushed 2 commits to branch master. Commits by maximedenes (1) and ppedrot (1).
Primitive persistent arrays (0ea2d0f )
Merge PR #11604: Primitive persistent arrays (8907a5b )
ejgallego pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
Fix Context with nonmaximplicit. (fd4bc8c )
Merge PR #12626: Fix Context with nonmaximplicit. (827425e )
ejgallego pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
Fix erroneous implicits-in-term warning (1bc0b15 )
Merge PR #12652: Fix erroneous implicits-in-term warning (5331a01 )
ejgallego pushed 5 commits to branch master. Commits by ppedrot (4) and ejgallego (1).
Small code simplification in Evarutil.new_evar. (7ba8eaf )
Remove Evarutil.new_pure_evar_full from the API. (c6391a7 )
Remove Evarutil.new_evar_from_context from the API. (aba870c )
Remove Evarutil.new_evar_instance from the API. (834c640 )
Merge PR #12645: Cleanup Evarutil API (cf383c1 )
ejgallego pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
ejgallego pushed 2 commits to branch master. Commits by ejgallego (1) and erikmd (1).
docs(README.md): Update badge and links (2443722 )
Merge PR #12612: docs(README.md): Update badge and links (421b221 )
gares pushed 2 commits to branch master. Commits by SkySkimmer (1) and gares (1).
Fix Canonical with universe polymorphism and primitive projection (1e92ed4 )
Merge PR #12627: Fix Canonical with universe polymorphism and primitive projection (769823c )
SkySkimmer pushed 9 commits to branch master. Commits by ejgallego (7) and SkySkimmer (2).
[declare] Generalize type of hooks. (e047457 )
[obligations] Functionalize Program state (54788df )
[obligations] Remove duplicate progmap_remove. (301e9cb )
[obligations] Allow state-modifying hooks (1954fb6 )
[obligations] Allow to simultaneously open a proof and add obligations (a164eaa )
[declare] Allow obligations update on equations closing hook. (4413a1f )
[ci] Overlay for metacoq and rewriter (22e2ab0 )
declare: Add [save_regular] API for obligation-ignoring proofs (3ef2bd3 )
Merge PR #11836: [obligations] Functionalize Program state (577ec77 )
MSoegtropIMC pushed 2 commits to branch master. Commits by MSoegtropIMC (1) and llee454 (1).
Defined arbitrary base logarithms (Rlog) and added natural lemmas concerning ln, exp, and Rlog to the Real library. Additionally made the real exponent notation nonlocal. (50b0b8f )
Merge PR #12542: Defined arbitrary base logarithms (Rlog) and added natural lemmas to the Real library (9b4d89c )
SkySkimmer pushed 4 commits to branch master. Commits by herbelin (3) and SkySkimmer (1).
Preserve delta-resolver at Module and Module Type starting. (0970c10 )
Adding test for #12525 (Search of lemmas in Include failing when in Module). (c68e580 )
Adding change log. (0046a16 )
Merge PR #12537: Take into account the existing delta-resolver when starting a new interactive module or module type (f2dc2f5 )
Zimmi48 pushed 13 commits to branch v8.12. Commits by Zimmi48 (7), MSoegtropIMC (2), SkySkimmer (2) and others (2).
Credit Erik Martin-Dorel for work on Docker. (ce4b60a )
Backport PR #12596: Credit Erik Martin-Dorel for work on Docker. (026848b )
[test-suite] async-proofs off in tests with Fail Timeout (f292909 )
Backport PR #12605: [test-suite] async-proofs off in tests with Fail Timeout (65ecf56 )
Cleanup mentions of -as in coqdep usage message (6b852e2 )
Backport PR #12614: Cleanup mentions of -as in coqdep usage message (aa59ac3 )
Windows build: use architecture dependent version of windres (6649733 )
Windows build: remove patch for windres architecture (712806a )
Backport PR #12641: Windows build: use architecture dependent version of windres (3bdb514 )
Fix erroneous implicits-in-term warning (46728f7 )
Backport PR #12652: Fix erroneous implicits-in-term warning (ab801f0 )
docs(README.md): Update badge and links (c0a19c3 )
Backport PR #12612: docs(README.md): Update badge and links (36468ab )
ejgallego pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
Add test for #10890 derive vs abstract (34e69c8 )
Merge PR #12666: Add test for #10890 derive vs abstract (511d2ca )
gares pushed 7 commits to branch master. Commits by ppedrot (6) and gares (1).
Stop back-and-forth array to list conversions in simpl. (69d25de )
Inline mutual recursion helpers in simpl implementation. (5c1730c )
Inline the Reductionops.fix_recarg function. (a659a12 )
Inline make_elim_fun in Tacred. (9895f45 )
Remove the last use of the Stack module in Tacred. (c6985ba )
Further cleanup of dead code in the Reductionops API. (9065877 )
Merge PR #12638: Some changes of representation in Tacred (7e149d3 )
ppedrot pushed 2 commits to branch master. Commits by jfehrle (1) and ppedrot (1).
Correct comment and clarify constant (2b87740 )
Merge PR #12635: Correct comment and clarify constant (c412b32 )
ppedrot pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Correctly readback blocked CaseInvert matches in VM/native (aacfda0 )
Merge PR #12646: Correctly readback blocked CaseInvert matches in VM/native (ed8a428 )
ppedrot pushed 3 commits to branch master. Commits by SkySkimmer (2) and ppedrot (1).
Recordops: unify struc_typ summary record and libobject entry struc_tuple (dc16333 )
Overlay for removing struc_tuple (5fad3ec )
Merge PR #12650: Recordops: unify struc_typ summary record and libobject entry struc_tuple (f4593ab )
Blaisorblade pushed 1 commit to branch Blaisorblade-loose-hint-docs.
tactics.rst: Require A
is enough for A
's hints (f91f2ac )
Zimmi48 pushed 2 commits to branch master. Commits by Blaisorblade (1) and Zimmi48 (1).
tactics.rst: Require A
is enough for A
's hints (f91f2ac )
Merge PR #12681: tactics.rst: Require A
is enough for A
's hints (f238b25 )
Zimmi48 deleted the branch Blaisorblade-loose-hint-docs.
ejgallego pushed 2 commits to branch master. Commits by ejgallego (1) and herbelin (1).
Compatibility of make-change-log with MacOS X whose "sed" does not support "\+". (1b7565e )
Merge PR #12692: Compatibility of make-change-log with MacOS X whose "sed" does not support the "\+" operator of regular expressions (bcccf10 )
ejgallego pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
Fix fiat_crypto(_ocaml) needs/dependencies (5a6afa0 )
Merge PR #12673: Fix fiat_crypto(_ocaml) needs/dependencies (d0cfc7a )
ejgallego pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
Minor improvement to CI logs (0fe42aa )
Merge PR #12671: Minor improvement to CI logs (33e7485 )
Zimmi48 pushed 20 commits to branch v8.12. Commits by Zimmi48 (9), SkySkimmer (6), ppedrot (4) and others (1).
Bump HoTT pin for compatibility with #12572. (dd3b075 )
Correctly classify variables as being unfoldable in dnet patterns. (3ac78b3 )
Backport PR #12572: Correctly classify variables as being unfoldable in dnet patterns. (bcb5a41 )
Fix debug printer for auctx in presence of Anonymous (c946925 )
Backport PR #12628: Fix debug printer for auctx in presence of Anonymous (c948df5 )
Factorize tac2type syntax to fix the parsing of (t1, ..., tn) t. (8b48ca7 )
Add a test for Ltac2 parsing of parameterized types. (4cc0a72 )
Add a changelog. (3814012 )
Backport PR #12594: Fix ltac2 type parameters (9b54f78 )
Fix Context with nonmaximplicit. (fa78577 )
Backport PR #12626: Fix Context with nonmaximplicit. (db236c9 )
Use weak ref to memoize Evarutil.is_ground_env (f79e8c4 )
Backport PR #12618: Use weak ref to memoize Evarutil.is_ground_env (4150a32 )
tactics.rst: Require A
is enough for A
's hints (b681c9e )
Backport PR #12681: tactics.rst: Require A
is enough for A
's hints (855ff0e )
Fix fiat_crypto(_ocaml) needs/dependencies (7efcfcc )
Backport PR #12673: Fix fiat_crypto(_ocaml) needs/dependencies (0b05f6a )
Recordops: unify struc_typ summary record and libobject entry struc_tuple (a115caa )
Overlay for removing struc_tuple (f75ed38 )
Backport PR #12650: Recordops: unify struc_typ summary record and libobject entry struc_tuple (2356e74 )
ejgallego pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
Don't catch anomalies for evarconv "cannot find an instance" error (8641cb7 )
Merge PR #12675: Don't catch anomalies for evarconv "cannot find an instance" error (3eccf67 )
ejgallego pushed 3 commits to branch master. Commits by ppedrot (2) and ejgallego (1).
Fix #12513: coq no longer reports mismatched version numbers. (763c71e )
Add changelog. (e52f070 )
Merge PR #12677: Fix #12513: coq no longer reports mismatched version numbers. (f54bc66 )
ejgallego pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
Fix record pattern interpretation with implicit arguments (7bc3fb4 )
Merge PR #12631: Fix record pattern interpretation with implicit arguments (e04e12c )
ejgallego pushed 3 commits to branch master. Commits by herbelin (2) and ejgallego (1).
Fixes #12682 (recursive notation printing bug with n-ary applications). (8b97126 )
Adding change log. (5b277eb )
Merge PR #12683: Fixes #12682: printing bug with recursive notations for n-ary applications used with applied references (f67c382 )
ejgallego pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
CI: pass -silent to coqchk in compcert job (22b6d45 )
Merge PR #12702: CI: pass -silent to coqchk in compcert job (7e56c97 )
ejgallego pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
CI: Use bundled compcert for VST (1158886 )
Merge PR #12701: CI: Use bundled compcert for VST (2c482e5 )
ejgallego pushed 2 commits to branch v8.12. Commits by Zimmi48 (1) and ejgallego (1).
Use 8.12 specific branch for QuickChick. (11362ff )
Merge PR #12705: [v8.12] Use 8.12 specific branch for QuickChick. (c95bd4c )
ejgallego pushed 3 commits to branch master. Commits by Zimmi48 (2) and ejgallego (1).
Advertise switch to maintainer teams and credit maintainers. (730f9d3 )
Wording improvements. (c3f0ebe )
Merge PR #12670: Advertise switch to maintainer teams and credit maintainers. (153454d )
herbelin pushed 2 commits to branch master. Commits by ejgallego (1) and herbelin (1).
[search] Don't use ad-hoc Dumpglob table for Search (782173c )
Merge PR #12693: [search] Don't use ad-hoc Dumpglob table for Search (78689c1 )
herbelin pushed 2 commits to branch master+fixing-refman-tactic-notation-qualid-unfold-example.
Add tests for the interpretation of "unfold". (e221ebd )
Documenting new primitive entry evaluable_ref usable for tactic notations. (a34ba68 )
herbelin deleted the branch master+fixing-refman-tactic-notation-qualid-unfold-example.
gares pushed 3 commits to branch master. Commits by ppedrot (2) and gares (1).
Do not store the full environment inside ssr ast_closure_term. (ebf809d )
Add a changelog. (7fab7a5 )
Merge PR #12708: Do not store the full environment inside ssr ast_closure_term. (81a1bcf )
ppedrot pushed 2 commits to branch master. Commits by ejgallego (1) and ppedrot (1).
[gramlib] Remove legacy located exception wrapper in favor of standard infrastructure. (4a4d35b )
Merge PR #12696: [gramlib] Remove legacy located exception wrapper in favor of standard infrastructure. (689a391 )
ppedrot pushed 4 commits to branch master. Commits by ejgallego (3) and ppedrot (1).
[exn] Remove some uses of print (20f55b7 )
[reductionops] Comment about absorption of anomalies. (619533e )
[error handling] Anomaly in Conversion is a "precatchable_exception" (d2ca1ef )
Merge PR #12588: [exn] Remove some uses of print (e6d92a9 )
kyoDralliam pushed 3 commits to branch master. Commits by ppedrot (2) and kyoDralliam (1).
Better location for match! pattern variables in Ltac2. (4b4daab )
Clarify the Ltac2 invalid identifier message. (bece685 )
Merge PR #12680: Better location for match! pattern variables in Ltac2. (e9061bb )
SkySkimmer pushed 2 commits to branch master. Commits by SkySkimmer (1) and herbelin (1).
Do not print global refs as terms when asked to be printed as themselves. (a89bde7 )
Merge PR #12684: Do not print constructor and inductive types as terms when asked to be printed as themselves (d6aff77 )
ejgallego pushed 2 commits to branch master. Commits by Zimmi48 (1) and ejgallego (1).
Fix typo in contributing guide. (3416439 )
Merge PR #12660: Fix typo in contributing guide. (d57839d )
ejgallego pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
CI: deploy make-built stdlib doc (3039bb0 )
Merge PR #12712: CI: deploy make-built stdlib doc (f44202e )
ejgallego pushed 2 commits to branch master. Commits by ejgallego (1) and herbelin (1).
Fix bug #12691 (an only parsing notation induces a generic printing format). (fff1525 )
Merge PR #12697: Fix bug #12691: an only-parsing notation needs to produce a generic printing format in anticipation of further not-only-parsing uses of the notation (8f4d7dd )
SkySkimmer pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
[declare] Remove some dead code in declare_mutual_definition (708869a )
Merge PR #12714: [declare] Remove some dead code in declare_mutual_definition (56fd98a )
ppedrot pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Turn various anomalies into regular errors in primitive declaration path (7461fe4 )
Merge PR #12664: Turn various anomalies into regular errors in primitive declaration path (3962027 )
SkySkimmer pushed 2 commits to branch master. Commits by SkySkimmer (1) and whonore (1).
Add Coqtail to CI (ca5aaa5 )
Merge PR #12715: Add Coqtail to CI (1ea5dec )
ejgallego pushed 27 commits to branch v8.12. Commits by Zimmi48 (10), ejgallego (5), SkySkimmer (4) and others (8).
CI: deploy make-built stdlib doc (7a3c7f3 )
Backport PR #12712: CI: deploy make-built stdlib doc (c706b62 )
Advertise switch to maintainer teams and credit maintainers. (7b1c36b )
Wording improvements. (4f61342 )
Backport PR #12670: Advertise switch to maintainer teams and credit maintainers. (2019d84 )
CI: pass -silent to coqchk in compcert job (6670c66 )
Backport PR #12702: CI: pass -silent to coqchk in compcert job (ea80bf3 )
Fix record pattern interpretation with implicit arguments (8968a00 )
Backport PR #12631: Fix record pattern interpretation with implicit arguments (15c5120 )
Fix #12513: coq no longer reports mismatched version numbers. (7991006 )
Add changelog. (74793f8 )
Backport PR #12677: Fix #12513: coq no longer reports mismatched version numbers. (4fceedc )
Don't catch anomalies for evarconv "cannot find an instance" error (6af6824 )
Backport PR #12675: Don't catch anomalies for evarconv "cannot find an instance" error (773d27f )
Do not store the full environment inside ssr ast_closure_term. (f20993a )
Add a changelog. (0ec9a04 )
Backport PR #12708: Do not store the full environment inside ssr ast_closure_term. (fda7fba )
Fixes #12682 (recursive notation printing bug with n-ary applications). (e5cd8fb )
Adding change log. (79a647c )
Backport PR #12683: Fixes #12682: printing bug with recursive notations for n-ary applications used with applied references (e083dda )
[and 7 more commit(s)]
ejgallego pushed 2 commits to branch v8.12. Commits by ejgallego (1) and herbelin (1).
Fix bug #12691 (an only parsing notation induces a generic printing format). (ac987cd )
Backport PR #12697: Fix bug #12691: an only-parsing notation needs to produce a generic printing format in anticipation of further not-only-parsing uses of the notation (8ca0009 )
Zimmi48 pushed 3 commits to branch master. Commits by herbelin (2) and Zimmi48 (1).
Add tests for the interpretation of "unfold". (e221ebd )
Documenting new primitive entry evaluable_ref usable for tactic notations. (a34ba68 )
Merge PR #12698: Fixing mention of unfold
as example of tactic taking a qualid in tactic notations (b8962b4 )
SkySkimmer pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Remove redundant data from VM case switch. (675b23d )
Merge PR #12679: Remove redundant data from VM case switch. (58df19e )
SkySkimmer pushed 2 commits to branch master. Commits by SkySkimmer (1) and Zimmi48 (1).
Ignore installation failure during call to brew. (b7d501f )
Merge PR #12672: Fix failing macOS build. (667fac4 )
ejgallego pushed 4 commits to branch master. Commits by ppedrot (3) and ejgallego (1).
Tweak the warning for arbitrary term hints. (85a4780 )
Add changelog. (de89e56 )
Remove automatic formatting of ComHints. (f41fcca )
Merge PR #12678: Tweak the warning for arbitrary term hints. (70bc0c7 )
Zimmi48 pushed 2 commits to branch master. Commits by Zimmi48 (1) and ejgallego (1).
[changelog] Latest changes backported to 8.12 branch. (7c3961c )
Merge PR #12734: [changelog] Latest changes backported to 8.12 branch. (8ad615c )
ejgallego pushed 12 commits to branch v8.12. Commits by ejgallego (6), ppedrot (3), herbelin (2) and others (1).
Tweak the warning for arbitrary term hints. (1712d24 )
Add changelog. (031b3ec )
Remove automatic formatting of ComHints. (ac2fddb )
Backport PR #12678: Tweak the warning for arbitrary term hints. (b44b684 )
Ignore installation failure during call to brew. (a469ace )
Backport PR #12672: Fix failing macOS build. (0a78e7e )
Add tests for the interpretation of "unfold". (bfc397a )
Documenting new primitive entry evaluable_ref usable for tactic notations. (10aa264 )
Backport PR #12698: Fixing mention of unfold
as example of tactic taking a qualid in tactic notations (3e3de57 )
[changelog] Latest changes backported to 8.12 branch. (736c094 )
Backport PR #12734: [changelog] Latest changes backported to 8.12 branch. (ebd4c42 )
[ci] Pin equations to right commit for 8.12.0 (5e347e8 )
Zimmi48 pushed 3 commits to branch master. Commits by ejgallego (2) and Zimmi48 (1).
[changelog] Fix hanging file extension. (57f1199 )
[changelog] Incorporate hanging changelog entry for 8.12+beta1 (744ef30 )
Merge PR #12739: [changelog] Fix hanging changelog entry for 8.12 beta (63c216d )
ejgallego pushed 3 commits to branch v8.12.
[changelog] Fix hanging file extension. (9deae60 )
[changelog] Incorporate hanging changelog entry for 8.12+beta1 (caecb0a )
Backport PR #12739: [changelog] Fix hanging changelog entry for 8.12 beta (5486c72 )
ejgallego pushed 2 commits to branch master. Commits by SkySkimmer (1) and ejgallego (1).
Fix coqdoc bad bulleting from incorrect space count (e140848 )
Merge PR #12747: Fix coqdoc bad bulleting from incorrect space count (55f4095 )
ejgallego pushed 2 commits to branch v8.12. Commits by SkySkimmer (1) and ejgallego (1).
Fix coqdoc bad bulleting from incorrect space count (302705c )
Backport PR #12747: Fix coqdoc bad bulleting from incorrect space count (f162f83 )
ejgallego pushed 2 commits to branch v8.12. Commits by MSoegtropIMC (1) and ejgallego (1).
Updated picks for CompCert and VST (2922c95 )
Merge PR #12745: [8.12] Updated picks for CompCert and VST (8de0960 )
Zimmi48 pushed 2 commits to branch v8.12. Commits by Zimmi48 (1) and ejgallego (1).
[release] Bump magic numbers for 8.12.0 tag (bc2e89d )
Merge PR #12735: [release] Bump magic numbers for 8.12.0 tag (558e8ea )
Zimmi48 pushed tag V8.12.0.
Zimmi48 pushed 1 commit to branch v8.12.
First commit after V8.12.0. (c97b82c )
jashug pushed 1 commit to branch dont-refresh-argument-names.
Do not refresh the names of implicit arguments. (6140d64 )
jashug deleted the branch dont-refresh-argument-names.
ppedrot pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Hint Opaque/Transparent/Unfold: don't error on opaque constants (37ba76b )
Merge PR #12573: Hint Opaque/Transparent/Unfold: don't error on Opaque Defined constants (91aef2c )
ppedrot pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Clarify Global.env usage in ppvernac (974401d )
Merge PR #12726: Clarify Global.env usage in ppvernac (4b67e66 )
SkySkimmer pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Faster algorithm to compute algebraic universe mapping in mimization. (b4bc3b7 )
Merge PR #12729: Faster algorithm to compute algebraic universe mapping in minimization. (9d8efb0 )
Lysxia pushed 3 commits to branch master. Commits by herbelin (2) and Lysxia (1).
Fixes #12752 (applying symbol escaping in index produced by coqdoc). (56ab658 )
Adding change log for #12754. (23303e6 )
Merge PR #12754: Fixes #12752: applying symbol escaping in coqdoc index (827d430 )
barras pushed 1 commit to branch scala-extraction.
barras deleted the branch scala-extraction.
coqbot pushed 2 commits to branch master. Commits by coqbot (1) and shiatsumat (1).
Fix do in ssreflect-proof-language.rst (adfcba5 )
Merge PR #12767: Fix do in ssreflect-proof-language.rst (e0b8b46 )
Lysxia pushed 2 commits to branch master. Commits by Lysxia (1) and lthms (1).
coqdoc: Fix the “details” environment (ce233d5 )
Merge PR #12772: coqdoc: Fix the “details” environment (2793c3c )
coqbot pushed 2 commits to branch master. Commits by coqbot (1) and jtcoolen (1).
Mention coqbot minimize feature in issue template. (046cf2c )
Merge PR #12706: Mention coqbot minimize feature in issue template. (40b4e84 )
coqbot pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot (1).
CI metacoq: make .merlin (54ba930 )
Merge PR #12724: CI metacoq: make .merlin (51eccce )
coqbot pushed 2 commits to branch master. Commits by Mbodin (1) and coqbot (1).
Trying to rephrase complex sentences to make them easier to read. (ddce800 )
Merge PR #12782: Trying to rephrase complex sentences to make them easier to read. (a5a4cbb )
coqbot pushed 2 commits to branch master. Commits by coqbot (1) and jfehrle (1).
Document "Print Debug GC" command and OCAMLRUNPARAM env variable (2d7a257 )
Merge PR #12643: Document "Print Debug GC" command and OCAMLRUNPARAM environment variable (7427e7c )
vbgl pushed 2 commits to branch master. Commits by Zimmi48 (1) and vbgl (1).
[default.nix] Propagate dependency on num following #12604. (a2da872 )
Merge PR #12796: [default.nix] Propagate dependency on num following #12604. (ef08abe )
CohenCyril pushed 2 commits to branch master. Commits by CohenCyril (1) and gares (1).
[ssr] turn "nothing to inject" into a real warning (fix #12746) (0aa3f87 )
Merge PR #12749: [ssr] turn "nothing to inject" into a real warning (fix #12746) (d5a8bdc )
vbgl pushed 2 commits to branch master. Commits by fajb (1) and vbgl (1).
[zify] fix for bug#12791 (4da8f11 )
Merge PR #12814: [zify] fix for bug#12791 (83ca3cb )
vbgl pushed 2 commits to branch master. Commits by fajb (1) and vbgl (1).
[micromega] Fix bug#12790 (74932ad )
Merge PR #12815: [micromega] Fix bug#12790 (873130a )
ppedrot pushed 2 commits to branch master. Commits by eponier (1) and ppedrot (1).
Repair coqide option "Display parentheses" (12acf83 )
Merge PR #12794: Repair coqide option "Display parentheses" (1d6c794 )
ppedrot pushed 2 commits to branch master. Commits by jfehrle (1) and ppedrot (1).
More documentation on grammars and parsing (1121a2d )
Merge PR #12717: More documentation on grammars and parsing (e0e07f5 )
coqbot pushed 2 commits to branch master. Commits by MSoegtropIMC (1) and coqbot (1).
Windows CI: changed cygwin repo server (f01b4c5 )
Merge PR #12748: Windows CI: changed cygwin repo server (a9786e8 )
Zimmi48 pushed 23 commits to branch v8.12. Commits by Zimmi48 (13), fajb (2), herbelin (2) and others (6).
Fixes #12752 (applying symbol escaping in index produced by coqdoc). (7842206 )
Adding change log for #12754. (229d7fd )
Backport PR #12754: Fixes #12752: applying symbol escaping in coqdoc index (e6ddf11 )
coqdoc: Fix the “details” environment (703e1f9 )
Backport PR #12772: coqdoc: Fix the “details” environment (b8748a2 )
Fix do in ssreflect-proof-language.rst (4c3034d )
Backport PR #12767: Fix do in ssreflect-proof-language.rst (4e4406b )
Trying to rephrase complex sentences to make them easier to read. (a09f977 )
Backport PR #12782: Trying to rephrase complex sentences to make them easier to read. (8a5c7cd )
Document "Print Debug GC" command and OCAMLRUNPARAM env variable (fd2f0c1 )
Backport PR #12643: Document "Print Debug GC" command and OCAMLRUNPARAM environment variable (96e0db6 )
[default.nix] Propagate dependency on num following #12604. (911e1b6 )
Backport PR #12796: [default.nix] Propagate dependency on num following #12604. (21b2455 )
Use versions of elpi and hb recommended by Enrico. (3a1477e )
Bump pin of perennial. (0188cc0 )
More documentation on grammars and parsing (aa15ad1 )
Backport PR #12717: More documentation on grammars and parsing (a1cb604 )
Repair coqide option "Display parentheses" (1be4d40 )
Backport PR #12794: Repair coqide option "Display parentheses" (7702208 )
[zify] fix for bug#12791 (3cacaf3 )
[and 3 more commit(s)]
anton-trunov pushed 2 commits to branch master. Commits by JasonGross (1) and anton-trunov (1).
Bring Int63 notations into line with stdlib (d39730a )
Merge PR #12479: Bring Int63 notations into line with stdlib (8ef7077 )
herbelin pushed 2 commits to branch master. Commits by JasonGross (1) and herbelin (1).
Bring Float notations in line with stdlib (fcc3db4 )
Merge PR #12556: Bring Float notations in line with stdlib (ab2a867 )
herbelin pushed 2 commits to branch master. Commits by herbelin (1) and ppedrot (1).
Do not rely on higher-order interfaces for patterns in dnets. (82caf82 )
Merge PR #12718: Do not rely on higher-order interfaces for patterns in dnets. (2dbeadd )
herbelin pushed 15 commits to branch master. Commits by ppedrot (14) and herbelin (1).
Inline Class_tactics.clenv_of_prods. (85e56b4 )
Perfom an goal enter in the relevant class tactics instead of outside. (e52a8a8 )
Do not tamper with hints in Class_tactics.with_prods. (2423629 )
Do not do a round trip with auto hint representation in autoapply. (8db43ca )
Move connect_hint_clenv from Auto to Hints. (b0aa5bd )
Make the Hint.hint type private. (de16cf5 )
Code simplification around hint manipulation in Class_tactics. (a666788 )
Export a dedicated function that applies immediately a hint. (e28edfd )
Tentatively more efficient implementation of e_give_exact for typeclasses. (2e22662 )
Remove dead code after the previous commit. (70b7aab )
Split the uses of connect_hint_clenv into two different functions. (2a62e99 )
Further code simplification in typeclass resolution tactic. (8e6ed55 )
Cosmetic changes as suggested by SkySkimmer. (52894e9 )
Add overlays. (404314c )
Merge PR #12720: Factor code related to class hint clenv (ae5f5ba )
anton-trunov pushed 3 commits to branch master. Commits by liyishuai (2) and anton-trunov (1).
deprecate prod_curry and prod_uncurry (c34596a )
add deprecation to changelog (5169633 )
Merge PR #12716: deprecate prod_curry and prod_uncurry (226ed20 )
anton-trunov pushed 2 commits to branch master. Commits by anton-trunov (1) and olaure01 (1).
Additional statements about List.repeat (94bb6fa )
Merge PR #12799: [stdlib] [List] Additional statements about List.repeat (422e2ec )
gares pushed 3 commits to branch master. Commits by ppedrot (2) and gares (1).
Move reduce_mind_case from Reductionops to Tacred. (5aebae7 )
Small code simplification in contract_(co)fix. (0c576f9 )
Merge PR #12823: Move reduce_mind_case from Reductionops to Tacred. (ca47fb6 )
ppedrot pushed 2 commits to branch master. Commits by herbelin (1) and ppedrot (1).
Fixes reduction effect printing in the presence of non purely applicative stacks. (bae2909 )
Merge PR #12751: Fixes reduction effect printing in the presence of non purely applicative stacks (700aaaa )
coqbot pushed 2 commits to branch master. Commits by coqbot (1) and jfehrle (1).
Document semantic restriction on patterns (0e96c24 )
Merge PR #12802: Document semantic restriction on patterns in Gallina match construct (55c6617 )
coqbot pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot (1).
Recommend replace as a replacement to cutrewrite. (e60721c )
Merge PR #12841: Recommend replace as a replacement to cutrewrite. (aa92642 )
ppedrot pushed 2 commits to branch master. Commits by herbelin (1) and ppedrot (1).
Remaining bugs in PR#12223 which fixed location of tactic errors (issue #12152). (05eb5d9 )
Merge PR #12774: Fixing tactic loc updating in #12223 (daed771 )
gares pushed 9 commits to branch master. Commits by ppedrot (8) and gares (1).
Store the default evar instance inside the evar info. (29cc320 )
Remove several calls to Evarutil.new_pure_evar. (a91d0e3 )
Fast path for evar substitution relying on evar identity substitutions. (f7b465b )
Use the evarinfo-stored identity substitution where applicable. (d987a15 )
Store the default instance in named_context_val. (8076de0 )
Actually use the default instance stored inside named_context_val. (7126990 )
Actually update uninitialized evar instances (hum hum). (ed4159b )
Add a few comments about the code. (2edad4e )
Merge PR #12725: Store evar identity instances in evarinfo / named_context_val (ae38c38 )
mattam82 pushed 2 commits to branch master. Commits by mattam82 (1) and ppedrot (1).
Do not precompute hint dnets eagerly. (bbed52c )
Merge PR #12822: Do not precompute hint dnets eagerly (7a051f3 )
mattam82 pushed 5 commits to branch master. Commits by ppedrot (4) and mattam82 (1).
Ensure statically that Hint Extern comes with a pattern. (a9541e2 )
Simplify the computation of the head global for hint patterns. (c5e68b5 )
Replace Hints.head_constr_bound with Hints.head_bound. (dc8b5be )
Add overlay. (46cdf9a )
Merge PR #12709: Simplify hint pattern handling (a18d81c )
coqbot pushed 2 commits to branch master. Commits by Mbodin (1) and coqbot (1).
Fixes #10902 by adding a mention of the JSON extraction in the documentation. (87d6d18 )
Merge PR #12856: Adding a mention of the JSON extraction in the documentation. (b409b98 )
jfehrle pushed 1 commit to branch show_proof_diffs.
Add a "Show Proof Diffs" message to the XML protocol (40285cd )
maximedenes pushed 2 commits to branch master. Commits by jashug (1) and maximedenes (1).
Do not refresh the names of implicit arguments. (300157f )
Merge PR #12756: Do not refresh the names of implicit arguments. (6091524 )
coqbot pushed 2 commits to branch master. Commits by coqbot (1) and gares (1).
[vernac] refine check for unresolved evars (d269b70 )
Merge PR #12759: [vernac] refine check for unresolved evars (5db27e4 )
ppedrot pushed 2 commits to branch master. Commits by gares (1) and ppedrot (1).
[ssr] when porting v8.2 code no backtracking point has to be added (af686af )
Merge PR #12857: [ssr] when porting v8.2 code no backtracking point has to be added (85dad6f )
ppedrot pushed 4 commits to branch master. Commits by herbelin (3) and ppedrot (1).
In tacinterp.ml , renaming eval_tactic into eval_tactic_ist to match the API. (3c45a14 )
Prefer eval_tactic_ist, which has error localisation, to interp_tactic. (9029403 )
Yet other tactic error location fixes (see PR#12223 and PR#12774). (f10b202 )
Merge PR #12853: Another tactic error location fix after PR#12223 and PR#12774 (f149d61 )
jfehrle deleted the branch show_proof_diffs.
herbelin pushed 2 commits to branch master. Commits by herbelin (1) and jashug (1).
Use properly fresh names for Scheme Equality (a2b4233 )
Merge PR #12866: Less fragile scheme equality (692b2de )
maximedenes pushed 2 commits to branch master. Commits by herbelin (1) and maximedenes (1).
Extraction: At declaration point of a global, use its declaring name. (1b8ce11 )
Merge PR #12851: Extraction: At declaration point of a global, use its declaring name (98734a2 )
ppedrot pushed 4 commits to branch master. Commits by herbelin (2), maximedenes (1) and ppedrot (1).
Quick fix to #12787 (injection anomaly due to inconsistent comp. of free vars). (13e4331 )
Adding change log for PR #12816. (c75f4dc )
Special commit to start benchmarking. (68a18c8 )
Merge PR #12816: Fixes #12787: anomaly of tactic injection in the presence of artificial dependencies disappearing by reduction (80aca04 )
coqbot pushed 3 commits to branch master. Commits by Zimmi48 (2) and coqbot (1).
Introduce GitHub Action to check for conflicts in PRs. (c424aea )
Add Actions to CI realm in CODEOWNERS. (6f18542 )
Merge PR #12832: Introduce GitHub Action to check for conflicts in PRs. (59f383a )
coqbot pushed 2 commits to branch master. Commits by coqbot (1) and herbelin (1).
No more arithmetic directory test-suite. (c3ff8bd )
Merge PR #12854: Mini-fix in test suite: arithmetic directory does no longer exist (99e944f )
SkySkimmer pushed 2 commits to branch master. Commits by JasonGross (1) and SkySkimmer (1).
Improve make approve-output
(bcc012e )
Merge PR #12864: Improve make approve-output
(f42b28e )
coqbot pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot (1).
Fix subject reduction VS cumulative inductives and function eta (97b8b79 )
Merge PR #12738: Fix subject reduction VS cumulative inductives and function eta (0f5bd6a )
coqbot pushed 4 commits to branch master. Commits by ppedrot (3) and coqbot (1).
Dnets now consider axioms as being opaque for pattern recognition. (4ebccb9 )
Do not store the transparent state in delayed dnets. (ca58a80 )
Adding overlays. (94bbe5b )
Merge PR #12565: Dnets now consider axioms as being opaque for pattern recognition. (188e8f7 )
herbelin pushed 2 commits to branch master. Commits by Mbodin (1) and herbelin (1).
Adding the example of bug #2904 into the test suite, and reorganising the test files. (81ed307 )
Merge PR #12835: Slightly reorganising the test suite to follow its documentation (d49b9f2 )
anton-trunov pushed 4 commits to branch master. Commits by jashug (3) and anton-trunov (1).
Modify Init/Logic.v to compile with -mangle-names. (73854ca )
Modify Init/Datatypes.v to compile with -mangle-names. (e070b2a )
Modify Init/Specif.v to compile with -mangle-names (65f99a0 )
Merge PR #12868: Lint stdlib with -mangle-names #1 (6a529d7 )
SkySkimmer pushed 2 commits to branch master. Commits by SkySkimmer (1) and whonore (1).
Fix Coqtail test directory. (c15eb9c )
Merge PR #12886: Fix Coqtail test directory. (016bafd )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and maximedenes (1).
Update sigma instead of erasing it in update_global_env
(a970072 )
Merge PR #12878: Update sigma instead of erasing it in update_global_env
(bd4791f )
coqbot-app[bot] pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot-app[bot] (1).
Merging is now possible with coqbot. (76abadc )
Merge PR #12778: Merging is now possible with coqbot. (ae7e82a )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
CI: stop testing 4.11+trunk (b2344b3 )
Merge PR #12870: CI: stop testing 4.11+trunk (a442885 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by SkySkimmer (1), akr (1) and coqbot-app[bot] (1).
Change OUnit package name to ounit2. (2431bb8 )
Dockerfile: Update ounit (5a77616 )
Merge PR #12798: Change OUnit package name to ounit2. (ba3ff67 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by SkySkimmer (1), coqbot-app[bot] (1) and ppedrot (1).
Perform a few tweaks to make the bench script work properly. (bcde3d1 )
Bench: artifact logs (0b86f6e )
Merge PR #12882: Perform a few tweaks to make the bench script work properly. (fe56ac4 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Fix slow Print Universes Subgraph when many ambient universes. (e9956d7 )
Merge PR #12728: Fix slow Print Universes Subgraph when many ambient universes. (ae712c6 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Add /dev/bench to CODEOWNERS (1b2d2bd )
Merge PR #12888: Add /dev/bench to CODEOWNERS (60684d2 )
Zimmi48 pushed 11 commits to branch v8.12. Commits by Zimmi48 (6), herbelin (2), MSoegtropIMC (1) and others (2).
Windows CI: changed cygwin repo server (67a09e5 )
Backport PR #12748: Windows CI: changed cygwin repo server (666854e )
Document semantic restriction on patterns (53291fc )
Backport PR #12802: Document semantic restriction on patterns in Gallina match construct (f9bce47 )
Recommend replace as a replacement to cutrewrite. (333764b )
Backport PR #12841: Recommend replace as a replacement to cutrewrite. (d3cafc7 )
Fixes #10902 by adding a mention of the JSON extraction in the documentation. (12bda62 )
Backport PR #12856: Adding a mention of the JSON extraction in the documentation. (ad33275 )
Quick fix to #12787 (injection anomaly due to inconsistent comp. of free vars). (df9b7e9 )
Adding change log for PR #12816. (5620220 )
Backport PR #12816: Fixes #12787: anomaly of tactic injection in the presence of artificial dependencies disappearing by reduction (c193436 )
anton-trunov pushed 2 commits to branch master. Commits by VincentSe (1) and anton-trunov (1).
Put cyclic numbers in sort Set instead of Type (0c39f0b )
Merge PR #12801: Put cyclic numbers in sort Set instead of Type (83da5d4 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and herbelin (1).
Fixing a coercion entry transitivity bug. (80a95af )
Merge PR #12758: Fixing a coercion entry transitivity bug. (af5e7d4 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and gares (1).
[test-suite] close the proof (8e78a6d )
Merge PR #12897: [test-suite] close the proof added in #12857 (3365b1e )
coqbot-app[bot] pushed 4 commits to branch master. Commits by Alizter (3) and coqbot-app[bot] (1).
ppedrot pushed 2 commits to branch master. Commits by JasonGross (1) and ppedrot (1).
Require NsatzTactic: nsatz support for Z and Q (4ad36b5 )
Merge PR #12861: Require NsatzTactic: nsatz support for Z and Q (e01f9df )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and herbelin (1).
Documentation of coq_makefile: fix name of installation dir + help on option -f. (2a703eb )
Merge PR #12884: Documentation of coq_makefile: fix name of installation dir + help on using option -f (48bd653 )
ppedrot pushed 2 commits to branch master. Commits by JasonGross (1) and ppedrot (1).
Remove useless commit guessing logic (3fab804 )
Merge PR #12901: [bench] Remove useless commit guessing logic (c222a0d )
ppedrot pushed 6 commits to branch master. Commits by SkySkimmer (5) and ppedrot (1).
Make decide equality compatible with mangled names. (9b2979b )
elim.ml : stop using intro_using (5e4d696 )
funind: stop using intro_using (2eac36b )
omega: stop using intro_using (a9a0307 )
Deprecate intro_using (495466d )
Merge PR #12881: Deprecate intro_using (a3834f1 )
ppedrot pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Move bench job definition to its own file (c43b3c2 )
Merge PR #12904: Move bench job definition to its own file (69ed442 )
ppedrot pushed 3 commits to branch master. Commits by herbelin (2) and ppedrot (1).
A fix and two enhancements of trailing pattern factorization in rec. notations. (324e647 )
Moving production_level_eq to extend.ml for separation of concerns. (5d0c54e )
Merge PR #12764: A fix and two enhancements of trailing pattern factorization in recursive notations (4e6b029 )
coqbot-app[bot] pushed 4 commits to branch master. Commits by jfehrle (3) and coqbot-app[bot] (1).
Make local nonterminal definitions unique when necessary (b291704 )
Add tags in prodn indicating productions that are from plugins, (fa3d479 )
Convert ltac2 chapter to use prodn, update syntax (4a7e393 )
Merge PR #12085: Convert ltac2 chapter to use prodn, update syntax (748299d )
gares pushed 5 commits to branch master. Commits by affeldt-aist (4) and gares (1).
tentative backport of ssrbool from MathComp 1.11 (3405ab8 )
add contra lemmas introduced by MathComp's PR #499 (a334a94 )
fix notation-incompatible-format warnings (bfd384e )
address comments and fixups (40140bf )
Merge PR #12898: [ssr] backport ssrbool from Math Comp 1.11 (1797822 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ppedrot (1).
Use the lite variants of performance tests in the bench default packages. (0cd0d31 )
Merge PR #12911: Use the lite variants of performance tests in the bench default packages (350a9ab )
coqbot-app[bot] pushed 3 commits to branch master. Commits by ppedrot (2) and coqbot-app[bot] (1).
Add a heterogeneous map function over Dyn.Map. (3d430a4 )
Use a map function instead of a fold when freezing summaries. (72500ec )
Merge PR #12867: Fast freeze summary (79e91fe )
coqbot-app[bot] pushed 4 commits to branch master. Commits by herbelin (3) and coqbot-app[bot] (1).
Dead code in adjust_implicit_arguments. (8f01a45 )
Propagate in-context information for extra arguments of notations too. (7f82d13 )
The body of a let is considered to be "in context" if its type is present. (27c1b65 )
Merge PR #12877: Propagate in-context information for explicitation of extra arguments of notations (871efc2 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Avoid running configure when plugins/ modified (cd7b346 )
Merge PR #12850: Avoid running configure when plugins/ modified (0e70c44 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and jashug (1).
Modify lia to work with -mangle-names (179a23a )
Merge PR #12913: Modify lia to work with -mangle-names (829d7ac )
ppedrot pushed 6 commits to branch master. Commits by maximedenes (5) and ppedrot (1).
Better encapsulation of future goals (4e59a68 )
Move given_up goals to evar_map (46c0b7a )
Make future_goals stack explicit in the evarmap (6c2a5cb )
Add test for #10939 (4a9057d )
Wrap future goals into a module (bd00733 )
Merge PR #12499: Clean future goals (2062f9c )
ppedrot pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
tacinterp mini cleanup useless letin (2f2c720 )
Merge PR #12918: tacinterp mini cleanup useless letin (dd7306e )
ppedrot pushed 2 commits to branch master. Commits by JasonGross (1) and ppedrot (1).
[coqchk] Look inside inner modules as well (cfc5484 )
Merge PR #12862: [coqchk] Look inside inner modules as well (f140359 )
ppedrot pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Rename VM-related kernel/cfoo files to kernel/vmfoo (4ee0ced )
Merge PR #12849: Rename VM-related kernel/cfoo files to kernel/vmfoo (1abf7c9 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ppedrot (1).
Fix .gitignore after the merge of #12849. (dac417a )
Merge PR #12922: Fix .gitignore after the merge of #12849. (a87c09c )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ejgallego (1).
[state] A few nits after consolidation of state. (60d2e06 )
Merge PR #12632: [state] A few nits after consolidation of state. (9c0b8bf )
coqbot-app[bot] pushed 3 commits to branch master. Commits by ppedrot (2) and coqbot-app[bot] (1).
Remove a call to the old refiner in ssr. (4109b89 )
Remove the now unused Evarutil.mk_new_meta function. (ce02197 )
Merge PR #12924: Remove meta-based refiner code in ssr (911f33f )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
par: print relevant subgoal when failing (9d31987 )
Merge PR #12932: par: print relevant subgoal when failing (511c280 )
ppedrot pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Add test for past anomaly (0b4c7ed )
Merge PR #12933: Add test for past anomaly (bbe6006 )
coqbot-app[bot] pushed 6 commits to branch master. Commits by ejgallego (4), coqbot-app[bot] (1) and vbgl (1).
[numeral] [plugins] Switch from Big_int
to ZArith. (094e464 )
[zarith] [notation] Build less intermediate values (3fcd90f )
[numtok] [zarith] Simplifications (694afd3 )
[nsatz] num → zarith (5a28133 )
[zarith] Changelog (21dd85b )
Merge PR #11742: [numeral] [plugins] Remove Coq's Bigint
module in favor of ZArith. (165aca8 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
ring: generate fresh names for lemmas (2db5e30 )
Merge PR #12890: ring: generate fresh names for lemmas (c73c239 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Fix configure check for zarith (f7d45c6 )
Merge PR #12939: Fix configure check for zarith (94115a6 )
ppedrot pushed 4 commits to branch master. Commits by SkySkimmer (3) and ppedrot (1).
Make abstract compatible with mangle names (40f8632 )
Clarify variable names in abstract implementation (4341759 )
Name saved goals in name_mangling test (2269c97 )
Merge PR #12929: Make abstract compatible with mangle names (fd8da75 )
ppedrot pushed 2 commits to branch master. Commits by maximedenes (1) and ppedrot (1).
Enrich evar_map
printer with future goals stack (d1dc634 )
Merge PR #12934: Enrich evar_map
printer with future goals stack (94d9fe2 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by JasonGross (1) and coqbot-app[bot] (1).
Fix rendering of -> in micromega (921a56a )
Merge PR #12952: Fix rendering of -> in micromega (9c9bf13 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ppedrot (1).
Drop opaque bodies of abstracted definitions. (427e8ca )
Merge PR #12935: Drop opaque bodies of abstracted definitions. (b4ff2af )
coqbot-app[bot] pushed 8 commits to branch master. Commits by herbelin (7) and coqbot-app[bot] (1).
In "About", print all arguments, even if it is trailing list of _. (3df82e1 )
When reporting an implicit argument error on a rename argument, use the renaming. (699eb94 )
When printing the type in About, use the renamed arguments. (1a91771 )
Do not write "rename" for arguments in About, since these arguments are validated. (9cb28c3 )
Where there are several lists of implicit arguments, don't pretend names matter. (4b9a823 )
About: Add a mention that arguments have been renamed, if ever it is the case. (d07d14d )
Adding overlay for coq-elpi. (8262041 )
Merge PR #12875: Further extensions of About wrt Arguments and renaming (daca839 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Fix load_printers after zarith (129e935 )
Merge PR #12958: Fix load_printers after zarith (84a32bb )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and jashug (1).
Add zarith to the include path for ocamldebug-coq (c10f60a )
Merge PR #12962: Add zarith to the include path for ocamldebug-coq (d66dbf1 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ejgallego (1).
[declare] Return both declared constants in Derive path. (ec23372 )
Merge PR #12961: [declare] Return both declared constants in Derive path. (4676822 )
ppedrot pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Update update_global_env usage (576c115 )
Merge PR #12892: Update update_global_env usage (0d30f79 )
ppedrot pushed 2 commits to branch master. Commits by maximedenes (1) and ppedrot (1).
Unify the shelves (636fe1d )
Merge PR #12872: Unify the shelves (8666b46 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ppedrot (1).
Use a faster algorithm to check for class existence. (c3d8ab8 )
Merge PR #12883: Use a faster algorithm to check for class existence. (cc51e1f )
herbelin pushed 8 commits to branch master. Commits by ppedrot (7) and herbelin (1).
Move elim-specific code from Tacticals to Elim. (bb09af9 )
Remove unused API from Elim. (afb4e06 )
Further remove the type Elim.branch_assumptions. (007f760 )
Make the Elim.branch_args type opaque. (6060c63 )
Factorize the only uses of internal API in Elim for Inv. (1ab01e5 )
Code deduplication in Elim. (7628e20 )
Remove the opening of CErrors in Elim. (c36fd38 )
Merge PR #12943: Move Elim-specific code (e9b64e2 )
ppedrot pushed 2 commits to branch master. Commits by JasonGross (1) and ppedrot (1).
[bench] Update bench script with better urls and more info (dc01511 )
Merge PR #12899: [bench] Update bench script with better urls and more info (ce0c147 )
herbelin pushed 5 commits to branch master. Commits by ppedrot (4) and herbelin (1).
Use a dedicated type for equality elimination. (7b4f197 )
Do not look for a quantified inductive type in intropattern injection. (b1aa5d4 )
Remove redundant data from the equality eliminator datatype. (8f48421 )
Document the Equality.equality type in the ML file. (93ac07b )
Merge PR #12973: Random cleanup around the data structures used in Equality (8cd66c8 )
ppedrot pushed 2 commits to branch master. Commits by herbelin (1) and ppedrot (1).
Namegen.visible_ids: fixing what seems to be typos. (74ea550 )
Merge PR #12876: Namegen.visible_ids: fixing what seems to be typos (a2dfddb )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ppedrot (1).
Perform an inversion of control in hint validation for eapply. (80004f8 )
Merge PR #12956: Perform an inversion of control in hint validation for eapply. (5ea743e )
ppedrot pushed 6 commits to branch master. Commits by maximedenes (5) and ppedrot (1).
Replace frozen
by allowed
evars in evarconv, and delay them (fea073c )
Abstract type for allowed evars (cd37a10 )
More efficient data structure for allowed evars (4e0f9f5 )
Comment AllowedEvars API (2724016 )
Add Equations overlay (6f3d15a )
Merge PR #12968: Replace frozen
by allowed
evars in evarconv, and delay them (b3bf44f )
coqbot-app[bot] pushed 2 commits to branch master. Commits by JasonGross (1) and coqbot-app[bot] (1).
Add :math: around math (b0894f1 )
Merge PR #12953: Add :math: around math (b2b9080 )
ppedrot pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Fix algebraic comparison with sprop on one side (edd1166 )
Merge PR #12912: Fix algebraic comparison with sprop on one side (e5a1aaa )
ppedrot pushed 3 commits to branch master. Commits by JasonGross (2) and ppedrot (1).
[bench] Also upload the raw timing files, etc (f9c3787 )
[bench] Only upload some files (f9eeec7 )
Merge PR #12900: [bench] Also upload the raw timing files, etc (2000ba3 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Fix incorrect debruijn handling when Record calls maybe_unify_params_in (bacbd17 )
Merge PR #12893: Fix incorrect debruijn handling when Record calls maybe_unify_params_in (d6e8e8c )
coqbot-app[bot] pushed 3 commits to branch master. Commits by RalfJung (2) and coqbot-app[bot] (1).
CI: build Iris examples instead of lambda-Rust (2d5a04e )
fix grepping for the Iris commit (eec818e )
Merge PR #12969: CI: build Iris examples instead of lambda-Rust (99a9e6b )
herbelin pushed 5 commits to branch master. Commits by ppedrot (4) and herbelin (1).
Enforce the argument of elim functions to be a variable. (06d6dda )
Defunctionalize the mk_elim creation in Elim. (950da35 )
Restrict a spurious call to a reduction to a quantified inductive type. (f9b5e98 )
Statically enforce that elim is passed a fully applied inductive type. (146c760 )
Merge PR #12980: Simplify the implementation of Elim (b6e16a0 )
herbelin pushed 5 commits to branch master. Commits by ppedrot (4) and herbelin (1).
Remove a useless use of clenv_fchain in Equality. (57ef36d )
Inline the last use of apply_on_clause in Equality. (c50d7aa )
Remove the last use of clenv_fchain in Equality. (31a9ad1 )
Remove a unused function from the Clenv API. (be494f5 )
Merge PR #12976: Remove clenv chaining in Equality (48f465d )
herbelin pushed 2 commits to branch master. Commits by herbelin (1) and ppedrot (1).
Remove dead code in clenv-generating functions. (cd9ca8a )
Merge PR #12988: Remove dead code in clenv-generating functions. (b972cc5 )
Zimmi48 pushed 32 commits to branch v8.12. Commits by Zimmi48 (15), SkySkimmer (5), Alizter (3) and others (9).
CI: stop testing 4.11+trunk (75cd5e2 )
Backport PR #12870: CI: stop testing 4.11+trunk (809c989 )
Improve make approve-output
(983fcab )
Backport PR #12864: Improve make approve-output
(6d9905b )
Change OUnit package name to ounit2. (7a913ae )
Dockerfile: Update ounit (b604010 )
Bump nixpkgs to get ounit2. (97a0545 )
Backport PR #12798: Change OUnit package name to ounit2. (ec53fb2 )
added numeral_notation to META.coq.in (9e7ab79 )
added coq.vernac dependency to numeral_notations plugin (e63719c )
added coq.vernac dependency to string_notations plugin (e36becc )
Backport PR #12879: added numeral_notation to META.coq.in (0bd305f )
Documentation of coq_makefile: fix name of installation dir + help on option -f. (f6b3efe )
Backport PR #12884: Documentation of coq_makefile: fix name of installation dir + help on using option -f (df7ad4b )
Fix rendering of -> in micromega (de9e5b9 )
Backport PR #12952: Fix rendering of -> in micromega (415148e )
Add :math: around math (a073318 )
Backport PR #12953: Add :math: around math (1f39281 )
[ssr] when porting v8.2 code no backtracking point has to be added (bd702a4 )
Backport PR #12857: [ssr] when porting v8.2 code no backtracking point has to be added (180fa5c )
[and 12 more commit(s)]
ppedrot pushed 2 commits to branch master. Commits by Lasse Blaauwbroek (1) and ppedrot (1).
Fix printing of change
tactic, which was printed as change_no_check
and vice versa (5a417e9 )
Merge PR #12987: Fix printing of change
tactic (edb2cef )
ppedrot pushed 3 commits to branch master. Commits by SkySkimmer (1), herbelin (1) and ppedrot (1).
Fixes a freshness issue with induction (see comment in #12944). (4c3064c )
Fix mangle names issue in induction (e589070 )
Merge PR #12954: Fixes a freshness issue with destruct/induction (see comment in #12944). (dde607c )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and jfehrle (1).
Explain how selectors change the order of goals (f238af8 )
Merge PR #12927: Explain that tactics applied to multiple goals don't preserve the order (ebcfaf6 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by clementblaudeau (2) and coqbot-app[bot] (1).
[Small typo] Update match.rst (9315f07 )
Update doc/sphinx/language/extensions/match.rst (bfd9e79 )
Merge PR #12991: [Small typo] Update match.rst (bfcd647 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Proof using cleanup, small doc addition and fix using Type in collections (df6d411 )
Merge PR #12931: Proof using cleanup, small doc addition and fix using Type in collections (d19175c )
Zimmi48 pushed 2 commits to branch v8.12. Commits by Zimmi48 (1) and gares (1).
[vernac] refine check for unresolved evars (64ea7c0 )
Backport PR #12759: [vernac] refine check for unresolved evars (f5f684f )
Zimmi48 pushed 2 commits to branch v8.12. Commits by Zimmi48 (1) and herbelin (1).
Fixes reduction effect printing in the presence of non purely applicative stacks. (51adb58 )
Backport PR #12751: Fixes reduction effect printing in the presence of non purely applicative stacks (1c199b9 )
cpitclaudel pushed 2 commits to branch master. Commits by Zimmi48 (1) and cpitclaudel (1).
Remove deprecated tactic cutrewrite. (f3642ad )
Merge PR #12993: Remove deprecated tactic cutrewrite. (0ab3e7f )
coqbot-app[bot] pushed 27 commits to branch master. Commits by jashug (26) and coqbot-app[bot] (1).
Modify Init/Peano.v to compile with -mangle-names. (560b288 )
Modify Init/Wf.v to compile with -mangle-names (d6b1274 )
Modify Init/Tactics.v to compile with -mangle-names (20b6715 )
Modify Bool/Bool.v to compile with -mangle-names (afdfbcf )
Modify Classes/RelationClasses.v to compile with -mangle-names (062853d )
Modify Classes/Morphisms.v to compile with -mangle-names (774d72f )
Modify Classes/CRelationClasses.v to compile with -mangle-names (25d1767 )
Modify Classes/CMorphisms.v to compile with -mangle-names (a66a9cd )
Modify Setoids/Setoid.v to compile with -mangle-names (59d99eb )
Modify Relations/Operators_Properties.v to compile with -mangle-names (d5f04bd )
Modify Relations/Relations.v to compile with -mangle-names (e5880b6 )
Modify Structures/Orders.v to compile with -mangle-names (17ed93c )
Modify Structures/OrdersTac.v to compile with -mangle-names (2d01a47 )
Modify Structures/OrdersFacts.v to compile with -mangle-names (32240c4 )
Modify Structures/GenericMinMax.v to compile with -mangle-names (c16e4c2 )
Modify Numbers/NatInt/NZBase.v to compile with -mangle-names (1a7dfd1 )
Modify Numbers/NatInt/NZAdd.v to compile with -mangle-names (1b6b14b )
Modify Numbers/NatInt/NZMul.v to compile with -mangle-names (9cd62a4 )
Modify Numbers/NatInt/NZOrder.v to compile with -mangle-names (9a51c93 )
Modify Numbers/NatInt/NZMulOrder.v to compile with -mangle-names (ea5f723 )
[and 7 more commit(s)]
ppedrot pushed 3 commits to branch master. Commits by mattam82 (1), maximedenes (1) and ppedrot (1).
Refine test for unresolved evars: not reachable from initial evars (b6dabf6 )
Circumvent revealed bug of evar resolution for fixpoint (fbe0ea4 )
Merge PR #7825: [tactics] Refine test for unresolved evars: not reachable from initial evars (6f12c3e )
herbelin pushed 4 commits to branch master. Commits by edwardcwang (3) and herbelin (1).
Add iff variant for app_inj_tail (ad89d85 )
Add iff variants for other list lemmas (d79c6b1 )
Add changelog entry (f2ba2ad )
Merge PR #12094: Extend app_inj_tail and other list lemmas (3d22134 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot-app[bot] (1).
Fix docgram's dune file following #12085. (461e0d6 )
Merge PR #12994: Fix docgram's dune file following #12085. (cdfe69d )
mattam82 pushed 1 commit to branch link-wiki-install.
Zimmi48 pushed 17 commits to branch v8.12. Commits by Zimmi48 (7), herbelin (4), SkySkimmer (2) and others (4).
[Small typo] Update match.rst (1e0c13d )
Update doc/sphinx/language/extensions/match.rst (fe384b5 )
Backport PR #12991: [Small typo] Update match.rst (f349663 )
Explain how selectors change the order of goals (00a61a4 )
Backport PR #12927: Explain that tactics applied to multiple goals don't preserve the order (1f4a7f9 )
Fix printing of change
tactic, which was printed as change_no_check
and vice versa (3e0a9f7 )
Backport PR #12987: Fix printing of change
tactic (a3ba4e0 )
Proof using cleanup, small doc addition and fix using Type in collections (c30cf76 )
Backport PR #12931: Proof using cleanup, small doc addition and fix using Type in collections (ac04a46 )
Remaining bugs in PR#12223 which fixed location of tactic errors (issue #12152). (00464b2 )
Backport PR #12774: Fixing tactic loc updating in #12223 (5d33e68 )
In tacinterp.ml , renaming eval_tactic into eval_tactic_ist to match the API. (1c77c44 )
Prefer eval_tactic_ist, which has error localisation, to interp_tactic. (e24f383 )
Yet other tactic error location fixes (see PR#12223 and PR#12774). (f01e2c5 )
Backport PR #12853: Another tactic error location fix after PR#12223 and PR#12774 (1d81b92 )
Fix incorrect debruijn handling when Record calls maybe_unify_params_in (77e7bf7 )
Backport PR #12893: Fix incorrect debruijn handling when Record calls maybe_unify_params_in (7a7360c )
herbelin pushed 1 commit to branch master+patch-wit_natural.
Adding a wit_natural standard argument. (d4c6a20 )
Zimmi48 deleted the branch master+patch-wit_natural.
@Hugo Herbelin It seems like you accidentally pushed a branch to the main repo. Since there is no associated PR, I deleted it.
Ah sorry. It was anyway a temporary branch for @Pierre Roux who already took its content. So, it is good that you deleted it because I indeed did not pay attention that I mistakenly pushed to origin.
coqbot-app[bot] pushed 3 commits to branch master. Commits by gares (2) and coqbot-app[bot] (1).
changelog entry for 12857 (75ae147 )
Update doc/changelog/06-ssreflect/12857-changelog-for-12857.rst (6cdbbf2 )
Merge PR #12998: changelog entry for 12857 (73210d0 )
herbelin pushed 2 commits to branch master. Commits by herbelin (1) and ppedrot (1).
Add a fast-path to Tactics.e_change_in_hyps. (4f5026b )
Merge PR #12997: Add a fast-path to Tactics.e_change_in_hyps. (a764c64 )
Zimmi48 pushed 1 commit to branch link-wiki-install.
coqbot-app[bot] pushed 3 commits to branch master. Commits by Zimmi48 (1), coqbot-app[bot] (1) and mattam82 (1).
Zimmi48 deleted the branch link-wiki-install.
vbgl pushed 2 commits to branch master. Commits by Zimmi48 (1) and vbgl (1).
Add simple-io to dev/ci/nix. (0f92ad3 )
Merge PR #13005: Add simple-io to dev/ci/nix. (e1a8da8 )
Zimmi48 pushed 9 commits to branch v8.12. Commits by Zimmi48 (4), jfehrle (3) and gares (2).
changelog entry for 12857 (828a729 )
Update doc/changelog/06-ssreflect/12857-changelog-for-12857.rst (ab4df6d )
Backport PR #12998: changelog entry for 12857 (6895fe3 )
Fix docgram's dune file following #12085. (d36d5b1 )
Backport PR #12994: Fix docgram's dune file following #12085. (9f555ce )
Make local nonterminal definitions unique when necessary (62532a7 )
Add tags in prodn indicating productions that are from plugins, (48bb581 )
Convert ltac2 chapter to use prodn, update syntax (3ba978e )
Backport PR #12085: Convert ltac2 chapter to use prodn, update syntax (5ca824a )
coqbot-app[bot] pushed 3 commits to branch master. Commits by Zimmi48 (2) and coqbot-app[bot] (1).
Minimal changes to make the refman compatible with Sphinx 3. (6abc0f4 )
Remove outdated references to productionlist. (795af93 )
Merge PR #13011: Minimal changes to make the refman compatible with Sphinx 3. (5b62a69 )
coqbot-app[bot] pushed 12 commits to branch master. Commits by proux01 (10), coqbot-app[bot] (1) and herbelin (1).
[refman] Replace num by int (35a84b3 )
[parsing] Rename token NUMERAL to NUMBER (b4d1189 )
[parsing] Simplify bigint (f61d7d1 )
[refman] Rename num to natural (46b9480 )
[refman] Rename numeral to number (754e138 )
[refman] Rename int to integer (724966f )
[refman] Explicit integer and natural (031cc2b )
Turn integer into natural in several mlgs (92bc869 )
Adding a wit_natural standard argument. (d5eb564 )
Rename Numeral Notation command to Number Notation (6551f14 )
[numeral notation] Improve documentation (ad7140a )
Merge PR #12979: Uniformize names for number literals between parsing and refman (e0696ef )
Zimmi48 pushed 13 commits to branch v8.12. Commits by Zimmi48 (7), SkySkimmer (4), jashug (1) and others (1).
Update INSTALL.md (192b6f2 )
Fix typos. (cd17f64 )
Backport PR #13001: Update INSTALL.md (153b933 )
Minimal changes to make the refman compatible with Sphinx 3. (bf7f2fe )
Remove outdated references to productionlist. (fd7f314 )
Backport PR #13011: Minimal changes to make the refman compatible with Sphinx 3. (2bc6433 )
Use properly fresh names for Scheme Equality (87d2513 )
Backport PR #12866: Less fragile scheme equality (59586ee )
Make decide equality compatible with mangled names. (69b0f4c )
elim.ml : stop using intro_using (77377ea )
funind: stop using intro_using (aaf5ed0 )
omega: stop using intro_using (5258b91 )
Backport PR #12881: Deprecate intro_using (282bf58 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and herbelin (1).
Fixing documentation relatively to example of use of extra spaces in notations. (d7d41be )
Merge PR #13022: Fixing documentation relatively to example of use of extra spaces in notations (9278a6e )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and gares (1).
[ci] [mathcomp] run the test suite (f6ab4e9 )
Merge PR #13014: [ci] [mathcomp] run the test suite (0905502 )
coqbot-app[bot] pushed 4 commits to branch master. Commits by ejgallego (3) and coqbot-app[bot] (1).
[ci] [docker] Up testing to OCaml 4.11.1 (4892543 )
[ocamlformat] Update to ocamlformat 0.15.0 (1f1ac8a )
[nix] Update ref for ocamlformat 0.15 (739c8dc )
Merge PR #12972: [ci] [docker] Up testing to OCaml 4.11.1 (6096028 )
ppedrot pushed 2 commits to branch master. Commits by jfehrle (1) and ppedrot (1).
Remove deprecated Extraction Language command value "Ocaml" (56ff177 )
Merge PR #13016: Remove deprecated Extraction Language command value "Ocaml" (d6b6e1d )
Zimmi48 pushed 6 commits to branch v8.12. Commits by ejgallego (3), Zimmi48 (2) and herbelin (1).
Fixing documentation relatively to example of use of extra spaces in notations. (16c8d98 )
Backport PR #13022: Fixing documentation relatively to example of use of extra spaces in notations (2d03e2e )
[ci] [docker] Up testing to OCaml 4.11.1 (2565d7c )
[ocamlformat] Update to ocamlformat 0.15.0 (827991f )
[nix] Update ref for ocamlformat 0.15 (4ae4b75 )
Backport PR #12972: [ci] [docker] Up testing to OCaml 4.11.1 (186e9ea )
fajb pushed 7 commits to branch master. Commits by ejgallego (5) and fajb (2).
[micromega] call csdpcert using path. (685f43d )
[micromega] Migrate from num to zarith (79aac95 )
[micromega] [test-suite] Update csdp cache for num -> zarith migration (43ad95f )
Updated .csdp.cache.test-suite and minor fixes (6b379b2 )
[zarith] [micromega] Bump to 1.10 and remove some hacks (7bf884b )
[micromega] Use minus_one
built-in zarith constant. (acb24a1 )
Merge PR #8743: [micromega] Switch from Big_int
to ZArith. (7edb2d3 )
vbgl pushed 2 commits to branch master. Commits by Zimmi48 (1) and vbgl (1).
Propagate zarith dependency. (4093277 )
Merge PR #13015: Propagate zarith dependency. (95f7839 )
herbelin pushed 2 commits to branch master. Commits by herbelin (1) and jashug (1).
Use fresher names in eqschemes. (172dbc8 )
Merge PR #13008: Use fresher names in eqschemes (3ff6af3 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by JasonGross (1) and coqbot-app[bot] (1).
[CI] Always upload artifacts (d0d2857 )
Merge PR #13024: [CI] Always upload artifacts (14f0e50 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by ejgallego (2) and coqbot-app[bot] (1).
[build] Don't link num
anymore in Coq (2eb7780 )
[install] Rewording of primitive floats. (29b8aae )
Merge PR #13007: [build] Don't link num
anymore in Coq (0879115 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ejgallego (1).
[vernac] Don't allow attributes on print / check (0022a52 )
Merge PR #13027: [vernac] Don't allow attributes on print / check (fdacb14 )
ppedrot pushed 3 commits to branch master. Commits by ejgallego (2) and ppedrot (1).
[leminv] Remove unused catch. (3658ae2 )
[leminv] Use higher-level Declare API. (9cc65e5 )
Merge PR #12610: [leminv] [declare] Use higher-level Declare API. (ff508ba )
coqbot-app[bot] pushed 3 commits to branch master. Commits by gares (2) and coqbot-app[bot] (1).
[ci] call dmesg after quick/async jobs to detect OOM (09a8989 )
[ci] [dmesg] save as artifact (37b16d6 )
Merge PR #13043: [ci] call dmesg after quick/async jobs to detect OOM (5bdd954 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by maximedenes (2) and coqbot-app[bot] (1).
Improve simple apply
example (286a518 )
Make simple apply in ...
point to simple apply
(b6a9258 )
Merge PR #13051: Improve simple apply
example (6b991f6 )
herbelin pushed 2 commits to branch master. Commits by herbelin (1) and ppedrot (1).
Formally deprecate the double induction tactic. (3466c08 )
Merge PR #12963: Formally deprecate the double induction tactic. (5c08a31 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot-app[bot] (1).
Fix Removed in Sphinx 4 deprecations. (ba7de02 )
Merge PR #13055: Fix Removed in Sphinx 4 deprecations. (9809e48 )
herbelin pushed 4 commits to branch master. Commits by ppedrot (3) and herbelin (1).
Remove dead code in dnets. (a00a51f )
Clean up a bit the implemenation of dnets. (41b4073 )
Remove unused API from Dn. (f50bbdc )
Merge PR #13052: Clean up Dnet implementation (fff4fe1 )
herbelin pushed 1 commit to branch master+mini-improvement-incompatible-evar-candidates.
More precise information when unification fails because of incompatible candidates. (f95ffc2 )
Zimmi48 deleted the branch master+mini-improvement-incompatible-evar-candidates.
@Hugo Herbelin You've accidentally pushed a branch to the main repo. I've deleted it since it was not associated with any PR.
Théo Zimmermann said :
Hugo Herbelin You've accidentally pushed a branch to the main repo. I've deleted it since it was not associated with any PR.
Oups, sorry. Thanks.
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
dune: pass -bin-annot to configure (cbb2efc )
Merge PR #12723: dune: pass -bin-annot to configure (84d5475 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and herbelin (1).
Adding debugging printers for Intmap. (17aa50c )
Merge PR #13057: Adding debugging printers for Intmap (4ebdfae )
coqbot-app[bot] pushed 2 commits to branch master. Commits by JasonGross (1) and coqbot-app[bot] (1).
Make print-pretty-timed robust against non-output-sync logs (fef5b75 )
Merge PR #13063: Make print-pretty-timed robust against non-output-sync logs (16813b5 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by Zimmi48 (1), coqbot-app[bot] (1) and ejgallego (1).
[configure] Fix version checks for lablgtk and zarith (21366f8 )
Bump nixpkgs to get zarith 1.10. (febcda9 )
Merge PR #13049: [configure] Fix version checks for lablgtk and zarith (5a9538e )
coqbot-app[bot] pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot-app[bot] (1).
[ci/gitlab/cachix] Avoid running in trouble when calling git fetch --unshallow. (73db4e3 )
Merge PR #13050: [ci/gitlab/cachix] Avoid running in trouble when calling git fetch --unshallow (c7e7265 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by ppedrot (2) and coqbot-app[bot] (1).
Do not allocate intermediate sets in universe refreshing. (1be0936 )
Be more efficient when generating the merge of ltle maps in AcyclicGraph. (60a55b1 )
Merge PR #13046: Small optimization of acyclic graph merge operation (c3a73c5 )
Zimmi48 pushed 3 commits to branch v8.12. Commits by Zimmi48 (2) and SkySkimmer (1).
Use tag v2.6 for VST, like in the platform. (97f7319 )
CI: Use bundled compcert for VST (a7d3c12 )
Merge PR #13056: [v8.12] Use tag v2.6 for VST, like in the platform. (5899d2a )
coqbot-app[bot] pushed 3 commits to branch master. Commits by herbelin (2) and coqbot-app[bot] (1).
Fixes #9403 and #10803 (missing flattening of nested applications in notations). (d680b80 )
Adding change log for #12960. (899e3cd )
Merge PR #12960: Fixes #9403 and #10803: missing flattening of nested applications in notations (46bc7d0 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by herbelin (2) and coqbot-app[bot] (1).
Setting default value for Display Parentheses off in CoqIDE. (b1fe1a3 )
Adding change log for #12794 and #13067. (c6a27e8 )
Merge PR #13067: Setting default value for Display Parentheses off in CoqIDE (c66919b )
ejgallego pushed 3 commits to branch v8.12. Commits by herbelin (2) and ejgallego (1).
A temporary fix of #13018 and #12775 for branch 8.2. (4f4842c )
Adding change log for #13026. (79b6ae0 )
Merge PR #13026: A temporary fix of #13018 and #12775 for branch 8.12 (b086bf6 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
fix build:quick and build:base+async artifacts (14aaac2 )
Merge PR #13061: fix build:quick and build:base+async artifacts (193ea58 )
ppedrot pushed 4 commits to branch master. Commits by herbelin (3) and ppedrot (1).
Tactic inversion: adding support for registration of an equality in Type. (93d9f3e )
Tactic replace: adding support for registration of an equality in Type. (d14abd0 )
Adding change log for #12847. (ac3b1c0 )
Merge PR #12847: Tactics inversion and replace work with eq in type (23b0dbb )
ppedrot pushed 4 commits to branch master. Commits by herbelin (3) and ppedrot (1).
Fixes #9716, #13004: don't drop the qualifier of quotations at printing time. (d286c36 )
Adding change log for #13028. (58cb7d8 )
Add overlay for Equations. (fb144f8 )
Merge PR #13028: Fixes #9716 and #13004: don't drop the qualifier of quotations at printing time (bb6e78e )
Zimmi48 pushed 20 commits to branch v8.12. Commits by Zimmi48 (10), herbelin (5), maximedenes (2) and others (3).
Use fresher names in eqschemes. (a833798 )
Backport PR #13008: Use fresher names in eqschemes (d1d4211 )
[ci/gitlab/cachix] Avoid running in trouble when calling git fetch --unshallow. (f5865a4 )
Backport PR #13050: [ci/gitlab/cachix] Avoid running in trouble when calling git fetch --unshallow (cd9febc )
Improve simple apply
example (4cfacc5 )
Make simple apply in ...
point to simple apply
(cac7310 )
Backport PR #13051: Improve simple apply
example (d6f1613 )
[vernac] Don't allow attributes on print / check (ee483c4 )
Backport PR #13027: [vernac] Don't allow attributes on print / check (53cf212 )
Fix Removed in Sphinx 4 deprecations. (6a2bd38 )
Backport PR #13055: Fix Removed in Sphinx 4 deprecations. (a4e6d0b )
Make print-pretty-timed robust against non-output-sync logs (8e819c1 )
Backport PR #13063: Make print-pretty-timed robust against non-output-sync logs (809fd50 )
Setting default value for Display Parentheses off in CoqIDE. (ec5befe )
Adding change log for #12794 and #13067. (b79620a )
Backport PR #13067: Setting default value for Display Parentheses off in CoqIDE (d20cd30 )
Tactic inversion: adding support for registration of an equality in Type. (719594d )
Tactic replace: adding support for registration of an equality in Type. (b78572d )
Adding change log for #12847. (c198010 )
Backport PR #12847: Tactics inversion and replace work with eq in type (3333dbb )
coqbot-app[bot] pushed 3 commits to branch master. Commits by herbelin (2) and coqbot-app[bot] (1).
A temporary fix of #13018 and #12775 for branch 8.2. (ec30b85 )
Adding change log for #13026. (c55f520 )
Merge PR #13073: A temporary fix of #13018 and #12775 for branch 8.12 (bis) (d9d89ad )
coqbot-app[bot] pushed 3 commits to branch master. Commits by ppedrot (2) and coqbot-app[bot] (1).
Statically ensure that only polymophic hint terms come with a context. (674dcda )
Add overlays. (69c92f7 )
Merge PR #12977: Statically ensure that only polymophic hint terms come with a context. (d7b2da0 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by MSoegtropIMC (1) and coqbot-app[bot] (1).
Fix issue #13065 - Windows CI broken (768af57 )
Merge PR #13077: Fix issue #13065 - Windows CI broken (8a149d0 )
coqbot-app[bot] pushed 4 commits to branch master. Commits by silene (3) and coqbot-app[bot] (1).
Modify bytecode representation of closures to please OCaml's GC (fix #12636). (5aa6d99 )
Use the same memory layout as closures for accumulators. (2d63a61 )
Use the closure tag for accumulators. (27695b5 )
Merge PR #12894: Modify bytecode representation of closures to please OCamls GC (fix #12636). (39fe247 )
Zimmi48 pushed 3 commits to branch v8.12.
Document incompatibility with OCaml 4.12. (ac65fe5 )
Check OCaml version upper bound in configure. (ff1b4fa )
Merge PR #12919: [v8.12] Document incompatibility with OCaml 4.12. (3d21f16 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and herbelin (1).
More improvements in locating tactic errors. (fc0aa1e )
Merge PR #12999: More improvements in locating tactic errors (9c2228f )
ppedrot pushed 2 commits to branch master. Commits by gares (1) and ppedrot (1).
[lib] make canonical_path_name always absolute (fix #13031) (2b258e9 )
Merge PR #13053: [lib] make canonical_path_name always absolute (fix #13031) (b9f385c )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and maximedenes (1).
CI script wrapper now requires Python (424ae42 )
Merge PR #13105: [nix] CI script wrapper now requires Python (bd24f72 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by herbelin (2) and coqbot-app[bot] (1).
Fixes part 1 of #12908 (collision involving a lonely notation). (dffe222 )
Adding change log for #12946. (a0090dc )
Merge PR #12946: Fixes part 1 of #12908: undetected collision involving a lonely notation at printing time. (982c282 )
coqbot-app[bot] pushed 32 commits to branch master. Commits by jashug (31) and coqbot-app[bot] (1).
Modify Numbers/Natural/Abstract/NBase.v to compile with -mangle-names (c662664 )
Modify Numbers/Natural/Abstract/NAdd.v to compile with -mangle-names (ecb2931 )
Modify Numbers/Natural/Abstract/NOrder.v to compile with -mangle-names (71a199d )
Modify Numbers/Natural/Abstract/NAddOrder.v to compile with -mangle-names (f8449f4 )
Modify Numbers/Natural/Abstract/NSub.v to compile with -mangle-names (fd20085 )
Modify Numbers/Natural/Abstract/NMaxMin.v to compile with -mangle-names (ffd6a5d )
Modify Numbers/Natural/Abstract/NParity.v to compile with -mangle-names (978a2ac )
Modify Numbers/Natural/Abstract/NPow.v to compile with -mangle-names (6b677ba )
Modify Numbers/Natural/Abstract/NDiv.v to compile with -mangle-names (2128f62 )
Modify Numbers/Natural/Abstract/NGcd.v to compile with -mangle-names (13a9a7f )
Modify Numbers/Natural/Abstract/NLcm.v to compile with -mangle-names (8710a94 )
Modify Numbers/Natural/Abstract/NBits.v to compile with -mangle-names (389cea0 )
Modify Arith/PeanoNat.v to compile with -mangle-names (4950ed3 )
Modify Arith/Le.v to compile with -mangle-names (0991de1 )
Modify Arith/Plus.v to compile with -mangle-names (a75bf2d )
Modify Arith/Mult.v to compile with -mangle-names (d0aea47 )
Modify Arith/Between.v to compile with -mangle-names (d9ce5d4 )
Modify Logic/EqdepFacts.v to compile with -mangle-names (fb1405e )
Modify Logic/Eqdep_dec.v to compile with -v (5238889 )
Modify Arith/Peano_dec.v to compile with -mangle-names (0f6f3ee )
[and 12 more commit(s)]
coqbot-app[bot] pushed 4 commits to branch master. Commits by silene (3) and coqbot-app[bot] (1).
Make "xxx:{{" always start a quotation, whether registered or not. (cb1a23c )
Recognize only ":{{" as a sentence-gobbling quotation. (27601f5 )
Avoid lookup up too many characters. (a5abb5d )
Merge PR #13097: Modify how quotations handle whole sentences. (b74339d )
cpitclaudel pushed 2 commits to branch master. Commits by Zimmi48 (1) and cpitclaudel (1).
Reduce nitpick_ignore list a little. (c571af2 )
Merge PR #13101: Reduce nitpick_ignore list a little. (a34e213 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by akr (2) and coqbot-app[bot] (1).
Type{i} should be Type(i). (9995c44 )
Wf.v defines Fix_eq, not fix_eq. (a497cab )
Merge PR #13111: Small document fixes. (2c802aa )
ppedrot pushed 2 commits to branch master. Commits by herbelin (1) and ppedrot (1).
More precise information when unification fails because of incompatible candidates. (772aa6b )
Merge PR #13032: More precise information when unification fails because of incompatible candidates (c63f7c8 )
ppedrot pushed 4 commits to branch master. Commits by herbelin (3) and ppedrot (1).
Adding a few tacticals for the purpose of porting funind to new proof engine. (bee9998 )
Almost fully moving funind to new proof engine. (5cac244 )
Applying ocamlformat. (be3a5ac )
Merge PR #13021: Almost fully moving funind to new proof engine (1c919ed )
Zimmi48 pushed 5 commits to branch v8.12. Commits by Zimmi48 (3) and herbelin (2).
Fixes part 1 of #12908 (collision involving a lonely notation). (9c7ea0e )
Adding change log for #12946. (ad934a1 )
Backport PR #12946: Fixes part 1 of #12908: undetected collision involving a lonely notation at printing time. (c27d8ac )
Reduce nitpick_ignore list a little. (59e6122 )
Backport PR #13101: Reduce nitpick_ignore list a little. (58e936a )
Zimmi48 pushed 4 commits to branch v8.12. Commits by Zimmi48 (3) and herbelin (1).
Patch OCaml 4.07.1 for latest Mingw. (f33cb0c )
More improvements in locating tactic errors. (18496b5 )
Backport PR #12999: More improvements in locating tactic errors (d40adb2 )
Merge PR #13085: Patch OCaml 4.07.1 for latest Mingw. (2df85ee )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and jashug (1).
Fix combining uniform parameters and mutual inductives. (afe7005 )
Merge PR #13123: Fix combining uniform parameters and mutual inductives. (7ffb5e6 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
interp_context_evars: removed unused [shift] argument (0fa5751 )
Merge PR #13116: interp_context_evars: removed unused [shift] argument (b842e83 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Reimplement Admit Obligations using standard Admitted code (4cc71d0 )
Merge PR #13114: Reimplement Admit Obligations using standard Admitted code (2855ede )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and herbelin (1).
Getting rid of temerarious EConstr.to_constr in Himsg. (d6fcf08 )
Merge PR #13108: Getting rid of temerarious EConstr.to_constr in Himsg (42a5e33 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by ppedrot (2) and coqbot-app[bot] (1).
Remove the forward class hint feature. (e3a1cf3 )
Further simplification of the typeclass registration API. (f162900 )
Merge PR #13106: Remove the forward class hint feature. (bb2d0d5 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and maximedenes (1).
{new,setoid_}ring -> ring (4476f64 )
Merge PR #13054: {new,setoid_}ring -> ring (214215e )
Zimmi48 pushed 4 commits to branch v8.12. Commits by silene (3) and Zimmi48 (1).
Make "xxx:{{" always start a quotation, whether registered or not. (661564f )
Recognize only ":{{" as a sentence-gobbling quotation. (c907430 )
Avoid lookup up too many characters. (bfe7b97 )
Backport PR #13097: Modify how quotations handle whole sentences. (2c37025 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by VincentSe (1) and coqbot-app[bot] (1).
More details in the documentation of native arrays (1347abe )
Merge PR #13125: More details in the documentation of native arrays (706ec6e )
Zimmi48 pushed 4 commits to branch v8.12. Commits by Zimmi48 (2), herbelin (1) and jashug (1).
Fix combining uniform parameters and mutual inductives. (6eac887 )
Backport PR #13123: Fix combining uniform parameters and mutual inductives. (49f9361 )
Getting rid of temerarious EConstr.to_constr in Himsg. (171c79f )
Backport PR #13108: Getting rid of temerarious EConstr.to_constr in Himsg (5fb4e89 )
coqbot-app[bot] pushed 4 commits to branch master. Commits by ppedrot (3) and coqbot-app[bot] (1).
Remove the ocamlformat git hook. (7b28475 )
Remove the linter ocamlformat pass. (3a88c57 )
Document the ocamlformat changes. (4a51746 )
Merge PR #12985: Remove ocamlformat from the linter and the pre-commit hook. (e596bbb )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and jfehrle (1).
Remove prefixes on nonterminal names, e.g. "constr:" and "Prim." (5b194f6 )
Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" -> "constr" (6d3a922 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot-app[bot] (1).
Document the removal of forward class hints. (753a0fd )
Merge PR #13141: Document the removal of forward class hints. (bd57c1a )
ppedrot pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Fix retyping anomaly in rewrite (9b27bd5 )
Merge PR #13119: Fix retyping anomaly in rewrite (ab70eb0 )
ppedrot pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Derive Inversion does not allow leftover evars (5135153 )
Merge PR #13115: Derive Inversion does not allow leftover evars (51c1b46 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by ppedrot (2) and coqbot-app[bot] (1).
Algorithmically faster implementation of Evarconv.apply_on_subterm. (7f75bc3 )
Explicitly pass around a state in Evarconv.second_order_matching. (120992d )
Merge PR #13152: Algorithmically faster implementation of Evarconv.apply_on_subterm (1d4f660 )
ppedrot pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Define a new type instance_flag instead of using [unit option] (ee92670 )
Merge PR #13128: Define a new type instance_flag instead of using [unit option] (69e3df2 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by RalfJung (1) and coqbot-app[bot] (1).
update for Iris build system changes (29cb5ec )
Merge PR #13159: update for Iris build system changes (e85f6b3 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and herbelin (1).
When a notation is only parsing, do not attach to it a specific format. (a2733be )
Merge PR #12949: When a notation is only parsing, do not attach to it a specific format. (022632c )
ppedrot pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Put type-in-type flag in ugraph. (316592a )
Merge PR #13087: Put type-in-type flag in ugraph. (cc3ef68 )
coqbot-app[bot] pushed 4 commits to branch master. Commits by herbelin (3) and coqbot-app[bot] (1).
Add a check of empty list of arguments in xmlprotocol where relevant. (e18ed35 )
Dropping the misleading int argument of Pp.h. (db27892 )
Add overlays for Coq-Equations, aac-tactics. (f7fabd3 )
Merge PR #13143: Drop misleading argument of Pp.h box (ac7c197 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by gares (2) and coqbot-app[bot] (1).
[stm] move par: implementation to vernac/comTactic and stm/partac (a023009 )
overlay for mtac2 (391e751 )
Merge PR #13088: [stm] move par: to comTactic (516a700 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ppedrot (1).
[bench] Dump the vo size difference. (c7294a4 )
Merge PR #13164: [bench] Dump the vo size difference. (03d55f9 )
coqbot-app[bot] pushed 9 commits to branch master. Commits by herbelin (8) and coqbot-app[bot] (1).
Print Scope & cie: Add parentheses around notation interpretation. (0d11cdd )
Notation.ml : Move interpretation_eq earlier for future use. (561fd5a )
Splitting ssrbool's multi-printing notations into parsing and printing. (2a50e04 )
Notations: reworking the treatment of only-parsing and only-printing notations. (8d27b12 )
Adding a warning in case a notation is used neither for parsing nor printing. (5ef7598 )
New spacing/formatting in Locate Notation, Print Scopes, Print Visibility. (4c090da )
Documenting the new only-parsing only-printing model. (a1df081 )
Adding change log for #12950. (3e32cf5 )
Merge PR #12950: Notations: reworking the treatment of only-parsing and only-printing notations (a78b394 )
coqbot-app[bot] pushed 4 commits to branch master. Commits by SkySkimmer (3) and coqbot-app[bot] (1).
Minimize Prop <= i to i := Set (f53f84d )
No bidirectionality when expected type for lambda is an evar. (cada5ca )
overlay for minim-prop-toset (9fb630a )
Merge PR #12449: Minimize Prop <= i to i := Set (71a23e6 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and gares (1).
coqbot-app[bot] pushed 4 commits to branch master. Commits by gares (3) and coqbot-app[bot] (1).
[printing] make detyping resilient to "let x : _ := t in" (1363a6f )
improve comment (a96f086 )
Update pretyping/detyping.ml (e586426 )
Merge PR #13163: [printing] make detyping resilient to "let x : _ := t in" (60e8fa2 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by coqbot-app[bot] (1), gares (1) and jfehrle (1).
fix ide/.merlin (6c5608a )
Add an XML message for "Show Proof Diffs" (1d4bbef )
Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocol (2ff70d8 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ppedrot (1).
Store the resolver of required modules as functor parameters in safe_env. (32e2609 )
Merge PR #13156: Store the resolver of required modules as functor parameters in safe_env (07a199f )
Zimmi48 pushed 8 commits to branch v8.12. Commits by Zimmi48 (4), SkySkimmer (3) and herbelin (1).
Fix retyping anomaly in rewrite (09d7266 )
Backport PR #13119: Fix retyping anomaly in rewrite (991df91 )
Derive Inversion does not allow leftover evars (34c2ec6 )
Backport PR #13115: Derive Inversion does not allow leftover evars (0a808de )
When a notation is only parsing, do not attach to it a specific format. (a584f66 )
Backport PR #12949: When a notation is only parsing, do not attach to it a specific format. (19eb033 )
Put type-in-type flag in ugraph. (720c5e1 )
Backport PR #13087: Put type-in-type flag in ugraph. (94cab62 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and jfehrle (1).
Add missing ";" in record grammar (bdc5db8 )
Merge PR #13185: Add missing ";" in Record grammar (420368a )
ppedrot pushed 4 commits to branch master. Commits by herbelin (3) and ppedrot (1).
Adding and using locations on identifiers in constr_expr where they were missing. (2cf0287 )
Add location in existential variable names (CEvar/GEvar). (b7c9ba2 )
Prim.pattern_ident takes a location and its synonymous pattern_identref is deprecated. (a6d52d2 )
Merge PR #13099: Locating pattern identifiers (?id) by default at parsing time and use location in some typing error messages (471da91 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ppedrot (1).
Fix #13169: vm_compute has existential crisis. (bdd2b32 )
Merge PR #13172: Fix #13169: vm_compute has existential crisis. (9fa5174 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and proux01 (1).
Use OCaml floating-point operations on 64 bits arch (6fe8c44 )
Merge PR #13147: Use OCaml floating-point operations on 64 bits arch (4110258 )
Zimmi48 pushed 4 commits to branch v8.12. Commits by Zimmi48 (2), jfehrle (1) and ppedrot (1).
Add missing ";" in record grammar (e3f98f8 )
Backport PR #13185: Add missing ";" in Record grammar (b682adc )
Fix #13169: vm_compute has existential crisis. (99db0bc )
Backport PR #13172: Fix #13169: vm_compute has existential crisis. (3af65ea )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and herbelin (1).
Closes #13142 (more standardized pretty-printing of records). (d98cca6 )
Merge PR #13144: Closes #13142: more standardized pretty-printing of Coq records (56384cc )
coqbot-app[bot] pushed 3 commits to branch master. Commits by herbelin (2) and coqbot-app[bot] (1).
Documenting option Set Printing Goal Name. (3b8252d )
Fixing redundant outputs when printing goals, especially in non-"pr_first" mode. (6acd4e8 )
Merge PR #13140: Documenting Set Printing Goal Names + a small goal display fix (fc0ee01 )
ppedrot pushed 3 commits to branch master. Commits by SkySkimmer (2) and ppedrot (1).
Guard unify_leq_delay calls in Typing (9324cc5 )
Catch more errors in Unification.abstract_list_all (34e1aee )
Merge PR #13181: Guard unify_leq_delay calls in Typing (4bf4345 )
ppedrot pushed 2 commits to branch master. Commits by herbelin (1) and ppedrot (1).
Deprecating wit_var to the benefit of its synonymous wit_hyp. (92ddd42 )
Merge PR #13098: Deprecating wit_var to the benefit of its synonymous wit_hyp (476520a )
Zimmi48 pushed 2 commits to branch v8.12. Commits by Zimmi48 (1) and gares (1).
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ejgallego (1).
[declare] Fix types of mutual lemmas when using Admitted. (2a2ce21 )
Merge PR #12925: [declare] Fix types of mutual lemmas when using Admitted. (2db3d50 )
ppedrot pushed 2 commits to branch master. Commits by jfehrle (1) and ppedrot (1).
For "Typeclasses eauto", search depth should be a natural, not an (cd9d1d7 )
Merge PR #13196: For "Typeclasses eauto", search depth should be a natural, not an integer (671262d )
ppedrot pushed 2 commits to branch master. Commits by jfehrle (1) and ppedrot (1).
Add support for "typeclasses eauto bfs <int_or_var_opt> (f24aa02 )
Merge PR #13195: Add support for "typeclasses eauto bfs <int_or_var_opt>" (e583be6 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Fix algebraic on the right when using bidi hints (276ad0f )
Merge PR #13192: Fix algebraic on the right when using bidi hints (e6a00dd )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and jfehrle (1).
Use list notation in nsatz examples referenced in the doc (8c6ed2f )
Merge PR #13207: Use list notation in examples referenced by "nsatz" documentation (4cb8a7c )
coqbot-app[bot] pushed 5 commits to branch master. Commits by herbelin (4) and coqbot-app[bot] (1).
Generalizing and exporting interp_assumption/interp_definition. (12ea331 )
Fixes/enhancements with local definitions in records. (0f40337 )
Add change log for #13166. (259471c )
Overlay for elpi. (2b8a111 )
Merge PR #13166: Fixes #13165: implicit arguments in defined fields of record types not taken into account (5be9faa )
coqbot-app[bot] pushed 4 commits to branch master. Commits by ppedrot (3) and coqbot-app[bot] (1).
Remove the compare_graph field from the conversion API. (9a026fc )
Pick the universe graph out of the environment in conversion API. (eb5a67d )
Similarly remove the explicit graph argument in the ~evar conversion API. (7320cd8 )
Merge PR #13151: Remove the compare_graph field from the conversion API. (33f6551 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and herbelin (1).
Consistent indentation + a few bullets in RIneq.v. (61e13c3 )
Merge PR #13204: Consistent indentation + a few bullets in RIneq.v. (9f07cf2 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and herbelin (1).
Add flag -open Gramlib so that merlin works in gramlib with make. (678aaa1 )
Merge PR #13194: Add flag -open Gramlib so that merlin works in gramlib with make (3690c28 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and jfehrle (1).
Require at least one reference for Typeclasses Opaque/Transparent (122cfab )
Merge PR #13197: Require at least one reference for Typeclasses Opaque/Transparent (6ac6f43 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and jfehrle (1).
Support "Solve Obligations of <ident>" option (2b79914 )
Merge PR #13208: Support "Solve Obligations of <ident>" (48319ad )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Respect Print Universes when printing primitive arrays (5da6b8c )
Merge PR #13180: Respect Print Universes when printing primitive arrays (1111093 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by fajb (2) and coqbot-app[bot] (1).
[zify] Add support for Int63.int (a2f5cc2 )
[zify] Use flag for Z.to_euclidean_division_equations. (031af73 )
Merge PR #12648: [zify] support for int63 (554bdc2 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and jfehrle (1).
Better message and avoid an infinite SPLICE loop (48e0d41 )
Merge PR #13214: Better message for doc_grammar; avoid an infinite SPLICE loop (91e7863 )
coqbot-app[bot] pushed 4 commits to branch master. Commits by silene (3) and coqbot-app[bot] (1).
Reroot primitive arrays on access (fix #12947). (ddd7371 )
Remove occurrences of Parray.reroot. (e3764e1 )
Check complexity of primitive arrays. (c3cfb3c )
Merge PR #12955: Reroot primitive arrays on access (6376578 )
ppedrot pushed 2 commits to branch master. Commits by ppedrot (1) and tchajed (1).
Report a useful error for dependent destruction (cc06679 )
Merge PR #13201: Report a useful error for dependent destruction (1356772 )
ppedrot pushed 5 commits to branch master. Commits by SkySkimmer (4) and ppedrot (1).
First list in cl_context is just booleans (c8c1723 )
Simplify Implicit_quantifiers.combine_params a bit (661d842 )
Implicit_quantifiers don't use precomputed is_class data (07b7bd7 )
Remove unused is_class info from cl_context (e23be6e )
Merge PR #13118: [type classes] Simplify cl_context (3f0b709 )
ppedrot pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Bench: move variables to the script (65f32df )
Merge PR #13222: Bench: move variables to the script (9db73ef )
coqbot-app[bot] pushed 3 commits to branch master. Commits by ejgallego (2) and coqbot-app[bot] (1).
[coqinit] Respect order of ML includes (f8a0b47 )
[coqinit] Cosmetics on long list append. (0730062 )
Merge PR #13198: [coqinit] Respect order of ML includes (235c550 )
Zimmi48 pushed 2 commits to branch v8.12.
Use more tags for Windows add-ons and bump some of them. (1b19185 )
Merge PR #13200: [v8.12] Use more tags for Windows add-ons and bump some of them. (be198e1 )
ppedrot pushed 3 commits to branch master. Commits by SkySkimmer (2) and ppedrot (1).
Cleanup rewrite.ml (d3b965c )
setoid_rewrite: record generated name when rewriting under lambda (0c1265f )
Merge PR #13130: setoid_rewrite: record generated name when rewriting under lambda (7118100 )
vbgl pushed 2 commits to branch master. Commits by Zimmi48 (1) and vbgl (1).
[default.nix] Propagate OCaml and findlib to user env. (a2ee2a6 )
Merge PR #13245: [default.nix] Propagate OCaml and findlib to user env. (0d45ff2 )
ppedrot pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Fix bench variables (f0ce03e )
Merge PR #13243: Fix bench variables (fe095cd )
Zimmi48 pushed 6 commits to branch v8.12. Commits by SkySkimmer (2), Zimmi48 (2) and ejgallego (2).
[coqinit] Respect order of ML includes (34c69bd )
[coqinit] Cosmetics on long list append. (8a3d1b7 )
Backport PR #13198: [coqinit] Respect order of ML includes (7a67d79 )
Cleanup rewrite.ml (d084102 )
setoid_rewrite: record generated name when rewriting under lambda (b700d00 )
Backport PR #13130: setoid_rewrite: record generated name when rewriting under lambda (c02105d )
coqbot-app[bot] pushed 3 commits to branch master. Commits by Zimmi48 (2) and coqbot-app[bot] (1).
Add style for smallcaps. (7b07bc9 )
Add some missing smallcaps. (3230c56 )
Merge PR #11924: Add style for smallcaps. (00b82b7 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by SkySkimmer (2) and coqbot-app[bot] (1).
Lowercase variables in git_download (6a0aad2 )
Automatically merge overlays with most recent upstream version (c4f5d75 )
Merge PR #13177: Automatically merge overlays with most recent upstream version (16180bf )
Zimmi48 pushed 2 commits to branch v8.12. Commits by Zimmi48 (1) and ejgallego (1).
[declare] Fix types of mutual lemmas when using Admitted. (2393487 )
Merge PR #13252: [declare] Fix types of mutual lemmas when using Admitted. (8.12) (4981678 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Fix overlay merge command (7a8e49a )
Merge PR #13261: Fix overlay merge command (c86f919 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Correct doc using :>> (feaee68 )
Merge PR #13263: Correct doc using :>> (d397f10 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by jfehrle (2) and coqbot-app[bot] (1).
Make no match/multiple match for tacn/cmd an error (703d2c9 )
Convert misc chapters to prodn (7a57a23 )
Merge PR #12936: Convert misc chapters to prodn, update syntax (a12112c )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and jfehrle (1).
Avoid magic numbers (71fe84d )
Merge PR #13137: [ltac] Avoid magic numbers (716299d )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ejgallego (1).
[declare] Remove recursive declaration from non-recursive functions (8137ab9 )
Merge PR #13223: [declare] Remove recursive declaration from non-recursive functions (689e86b )
coqbot-app[bot] pushed 2 commits to branch master. Commits by RalfJung (1) and coqbot-app[bot] (1).
adjust Search deprecation warning (a2ce4da )
Merge PR #13257: adjust Search deprecation warning (9e7b0f9 )
coqbot-app[bot] pushed 5 commits to branch master. Commits by herbelin (4) and coqbot-app[bot] (1).
Wish #12762: warning on duplicated catch-all pattern with unused named variable. (571834b )
Adapting theories to unused pattern-matching variable warning. (2fb42ce )
Change log for #12768. (ed8c756 )
Documenting warning about unused variables in pattern clauses. (3c73900 )
Merge PR #12768: Granting wish #12762: warning on duplicated catch-all pattern-matching clause with unused named variable (970d9be )
coqbot-app[bot] pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot-app[bot] (1).
Force-delete pr branches. (f3a6929 )
Merge PR #13260: [CI cachix] Force-delete pr branches. (82f7cc4 )
Zimmi48 pushed 7 commits to branch v8.12. Commits by Zimmi48 (4), jfehrle (2) and RalfJung (1).
Make no match/multiple match for tacn/cmd an error (aa8a64a )
Convert misc chapters to prodn (f338300 )
Backport PR #12936: Convert misc chapters to prodn, update syntax (19bf55b )
adjust Search deprecation warning (cef0e46 )
Backport PR #13257: adjust Search deprecation warning (831dee2 )
Force-delete pr branches. (9e6afad )
Backport PR #13260: [CI cachix] Force-delete pr branches. (48114e0 )
ppedrot pushed 3 commits to branch master. Commits by SkySkimmer (2) and ppedrot (1).
Improve tactic interpreter registration API a bit (5146b2f )
Ltac2: use ComTactic infrastructure (30f97be )
Merge PR #13167: Ltac2: use ComTactic infrastructure (b87fd6c )
coqbot-app[bot] pushed 12 commits to branch master. Commits by ppedrot (11) and coqbot-app[bot] (1).
Introduce a dummy name quotient API. (8f16b1c )
Deprecate the non-qualified equality functions on kerpairs. (2b91a89 )
Same little game with Projection. (0590764 )
Rename the GlobRef comparison modules following the standard pattern. (0a46af1 )
Introduce an Ind module in the Names API. (bc108fd )
Similar introduction of a Construct module in the Names API. (aa3d78f )
Code factorization in Names. (b71a363 )
Introduce the missing dual name quotient modules in Environ. (70ca8c4 )
Document the signatures of quotient names in the API. (373376b )
Add missing deprecations in Projection API. (9a3d4e2 )
Add overlays. (375fc70 )
Merge PR #13075: Introducing the foundations for a name-alias-agnostic API (5f5cdda )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ppedrot (1).
coqbot-app[bot] pushed 6 commits to branch master. Commits by jfehrle (5) and coqbot-app[bot] (1).
Rename operconstr -> term (b402adc )
Rename tactic_expr -> ltac_expr (ede77b7 )
Rename misc nonterminals (41b0780 )
Rename tac2type -> ltac2_type, (6620c74 )
Change a few nonterminal names in mlgs and update doc to match (480d34f )
Merge PR #13219: Rename mlg grammar nonterminals to make documented and mlg grammars more consistent (c8110e1 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by LasseBlaauwbroek (1) and coqbot-app[bot] (1).
Fix printing of wit_constr and some ssr problems with printing empty lists (67089b3 )
Merge PR #13238: Fix some tactic print bugs (473160e )
Zimmi48 pushed 4 commits to branch v8.12. Commits by Zimmi48 (2), LasseBlaauwbroek (1) and ppedrot (1).
Restore the List.Smart.map original implementation. (e5b3ecb )
Backport PR #13226: Restore the List.Smart.map original implementation. (e06458a )
Fix printing of wit_constr and some ssr problems with printing empty lists (3f3fc99 )
Backport PR #13238: Fix some tactic print bugs (a517679 )
ppedrot pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
universes_of_constr: don't ignore CaseInvert universes (e901ce8 )
Merge PR #13273: universes_of_constr: don't ignore CaseInvert universes (4ab2522 )
ppedrot pushed 2 commits to branch master. Commits by herbelin (1) and ppedrot (1).
Use same code for "Print Ltac foo" and "Print foo" when "foo" is an Ltac. (c1e7b28 )
Merge PR #13254: Adopt the same format for "Print Ltac foo" and "Print foo" when "foo" is an Ltac (a392b02 )
ppedrot pushed 3 commits to branch master. Commits by herbelin (2) and ppedrot (1).
Adding support for printing goal names in CoqIDE. (c3dcb5a )
Add change log for #13145. (05f8308 )
Merge PR #13145: Adding support for printing goal names in CoqIDE (e4575cb )
ppedrot pushed 3 commits to branch master. Commits by herbelin (2) and ppedrot (1).
Fixes #13241 (nested Ltac functions were wrongly reporting error on the inner calls). (f4adca7 )
Adding changelog for #13247. (4057fe2 )
Merge PR #13247: Fixes #13241: nested Ltac functions wrongly reporting error on the inner calls (acf9cd0 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot-app[bot] (1).
Update screenshot of shield icon (shown in CONTRIBUTING). (ed8d9db )
Merge PR #13294: Update screenshot of shield icon (shown in CONTRIBUTING). (a89ac22 )
coqbot-app[bot] pushed 4 commits to branch master. Commits by ppedrot (3) and coqbot-app[bot] (1).
Fix bug in conversion of primitive values. (5601879 )
Yet another normal / neutral bug in primitive conversion. (786f3b7 )
Adding a test for the second bug. (42c1887 )
Merge PR #13274: Fix two bugs in conversion of primitive values (35354fc )
coqbot-app[bot] pushed 6 commits to branch master. Commits by gares (5) and coqbot-app[bot] (1).
attribute #[using] for Definition and Fixpoint (39e45f2 )
document Proof.compact (a464fdc )
[stm] support #[using] attribute (fd9d10f )
add changelog (bd4d201 )
[doc] attribute #[using] (7de7fe6 )
Merge PR #13183: attribute #[using] for Definition and Fixpoint (dc244ad )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ppedrot (1).
Micro-optimization in Control.check_for_interrupt. (f315ebd )
Merge PR #13250: Micro-optimization in Control.check_for_interrupt. (dfdecf2 )
Zimmi48 pushed 2 commits to branch v8.12.
Revert Coq-Elpi to 1.5.1. (3958208 )
Merge PR #13282: [v8.12] Revert Coq-Elpi to 1.5.1. (dbf2cf8 )
coqbot-app[bot] pushed 4 commits to branch master. Commits by herbelin (3) and coqbot-app[bot] (1).
Fixing printing part of #13078 (anomaly with binding notations in patterns). (26a456c )
Addressing parsing part #13078. (116e82b )
Adding change log for #13092. (74fc0e6 )
Merge PR #13092: Fixing #13078: stack overflow and anomalies with binding notations in patterns (d08be3f )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Remove test-suite/bugs/opened/bug_3395.v: not a bug (13cfe62 )
Merge PR #13256: Remove test-suite/bugs/opened/bug_3395.v: not a bug (c8a00cc )
coqbot-app[bot] pushed 3 commits to branch master. Commits by SkySkimmer (2) and coqbot-app[bot] (1).
Fix printing for empty primitive arrays (1280a49 )
Nicer spacing when printing array literals (225a4ee )
Merge PR #13179: Fix printing for empty primitive arrays (008f6eb )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Understand Mangle Names in implicit generalization (2c092c7 )
Merge PR #13132: Understand Mangle Names in implicit generalization (077d479 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by fakusb (2) and coqbot-app[bot] (1).
Doc: added "Arguments" removing implicit arguments (d7f87ac )
improved documentation of arguments command (87be983 )
Merge PR #13293: Doc: added "Arguments" removing implicit arguments (5a25287 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot-app[bot] (1).
Fix test-suite in async mode. (2812f83 )
Merge PR #13302: Fix test-suite in async mode. (4f8e14a )
coqbot-app[bot] pushed 3 commits to branch master. Commits by ppedrot (2) and coqbot-app[bot] (1).
Add a fast path in CClosure stack zipping. (a53eeff )
Eagerly reduce rigid/flex conversion problems. (af6a928 )
Merge PR #13258: Eagerly reduce rigid / flex conversion problems (11cb6dd )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ejgallego (1).
[build] [native] Don't assume installed native libraries are in custom output path (f3cc5b6 )
Merge PR #13193: [build] [native] Don't assume installed native libraries are in custom output path (7f90e6e )
MSoegtropIMC pushed 4 commits to branch master. Commits by ppedrot (3) and MSoegtropIMC (1).
Adding an if-then-else syntax to Ltac2. (f661944 )
Document the syntax addition. (2559f04 )
Regenerate the grammar description file. (1b0e754 )
Merge PR #13232: Adding an if-then-else syntax to Ltac2. (b65e9e9 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Check types when converting irrelevant terms in old unification (64b56ee )
Merge PR #13182: Check types when converting irrelevant terms in old unification (81eecfc )
Zimmi48 pushed 16 commits to branch v8.12. Commits by Zimmi48 (7), ppedrot (3), fakusb (2) and others (4).
Fix bug in conversion of primitive values. (9403c34 )
Yet another normal / neutral bug in primitive conversion. (fe6ad95 )
Adding a test for the second bug. (7156031 )
Backport PR #13274: Fix two bugs in conversion of primitive values (ecd4ba7 )
Fixes #13241 (nested Ltac functions were wrongly reporting error on the inner calls). (b3fd279 )
Adding changelog for #13247. (986976c )
Backport PR #13247: Fixes #13241: nested Ltac functions wrongly reporting error on the inner calls (13c4e4c )
Fix test-suite in async mode. (885e033 )
Backport PR #13302: Fix test-suite in async mode. (99555bd )
Doc: added "Arguments" removing implicit arguments (9af8547 )
improved documentation of arguments command (dfa6664 )
Backport PR #13293: Doc: added "Arguments" removing implicit arguments (9f0e970 )
[build] [native] Don't assume installed native libraries are in custom output path (2d8c415 )
Backport PR #13193: [build] [native] Don't assume installed native libraries are in custom output path (07ca395 )
Understand Mangle Names in implicit generalization (aaf0400 )
Backport PR #13132: Understand Mangle Names in implicit generalization (b50de9e )
coqbot-app[bot] pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot-app[bot] (1).
Remove warning on SSR Search having moved. (e047599 )
Merge PR #13231: Remove warning on SSR Search having moved. (5af74f7 )
ppedrot pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Fix anomaly when importing a functor (ffebade )
Merge PR #13191: Fix anomaly when importing a functor (812e2fd )
coqbot-app[bot] pushed 3 commits to branch master. Commits by herbelin (2) and coqbot-app[bot] (1).
Fixes #13298: primitive projections needs a correct typing environment. (091bfff )
Adding change log for #13301. (77959d9 )
Merge PR #13301: Fixes #13298: Search applied to primitive projections needs a correct typing environment (b95c38d )
coqbot-app[bot] pushed 28 commits to branch master. Commits by proux01 (27) and coqbot-app[bot] (1).
Renaming Numeral.v into Number.v (2d44c82 )
Renaming numnotoption into number_modifier (3a25b96 )
Renaming Numeral into Number (da72faf )
Add kernel/float64.ml to gitignore (814c16e )
Add functions Smartlocate.global_{constant,constructor} (3f04bd0 )
[numeral notation] Add a pre/postprocessing (dfcb151 )
[numeral notation] Adding the via ... using ... option (11a8997 )
[numeral notation] Add tests for the via ... using ... option (14f3014 )
[numeral notation] Document the via ... using ... option (c217bbe )
[numeral notation] Remove proofs for Q (7ea7834 )
[numeral notation] Q (ec24b26 )
[numeral notation] Specify Q (398dc5e )
[numeral notation] Prove Q (11f8d8f )
[numeral notation] R (b6c13af )
[numeral notation] Specify R (edea770 )
[numeral notation] Prove R (b51a8a0 )
[numeral notation] Allow to put/ignore holes during pre/postprocessing (9082af8 )
[numeral notation] Handle implicit arguments (0520dec )
[numeral notation] Add tests for implicit arguments (036117f )
[numeral notation] Add support for parameterized inductives (e728a1e )
[and 8 more commit(s)]
coqbot-app[bot] pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot-app[bot] (1).
Changelog for 8.12.1. (a6b5a5a )
Merge PR #13311: Changelog for 8.12.1. (d276a49 )
coqbot-app[bot] pushed 21 commits to branch master. Commits by Zimmi48 (20) and coqbot-app[bot] (1).
Move some content to a new page on term rewriting and simplification. (fdb8ef8 )
Remove everything after term rewriting and simplification. (643f13e )
Remove everything before term rewriting and simplification. (4a22c83 )
Add new page to writing proof index. (a5aee12 )
Move some content to a new page on automation. (d425851 )
Keep only content about auto. (e5e4f44 )
Move some content to a new page on solvers for logic and equality. (e293fe4 )
Keep only the content on solvers for logic and equality. (da4641d )
Remove parts of Tactics that were moved elsewhere. (32e5107 )
Move some content on goal management to the proof mode page. (d437390 )
Remove everything after the content on goal management. (e7aaf58 )
Remove everything before goal management. (97b5fd3 )
Octopus merge to preserve history of content split over multiple files. (c13b917 )
Move proof handling chapter in new location. (a549211 )
Merge content from two origins into the same file. (ee92aac )
Various fixes. (b6f3e76 )
Add new sections to automatic tactic chapter. (d517069 )
Change the title of the automatic tactic chapter and of its sections. (4130c67 )
Improve title of first proof chapter. (892cb35 )
Add a redirection from previous location of the proof handling chapter. (3a1bea8 )
[and 1 more commit(s)]
ejgallego pushed 8 commits to branch master. Commits by herbelin (7) and ejgallego (1).
Notations: Giving a consistent role to global references occurring patterns. (cb105b6 )
Passing full interning env to pattern interning, for better control. (4b8a87b )
Accept section variables in notations with mixed terms and binders. (c893dc5 )
Accept local variables in mixed terms and binders of notations. (8376231 )
Regression tests for the various combinations of mixed terms and binders in notations. (eaa25fb )
Minor cut elimination in the code of constrintern.ml . (7dcd829 )
Added change log for #12099. (6521021 )
Merge PR #12099: More parsing/printing notation/abbreviation consistency for mixed terms and pattern (16144a4 )
Zimmi48 pushed 7 commits to branch v8.12. Commits by Zimmi48 (4), herbelin (2) and SkySkimmer (1).
Fix anomaly when importing a functor (578fba1 )
Backport PR #13191: Fix anomaly when importing a functor (dce4538 )
Fixes #13298: primitive projections needs a correct typing environment. (2c35328 )
Adding change log for #13301. (83fbf4a )
Backport PR #13301: Fixes #13298: Search applied to primitive projections needs a correct typing environment (e367a01 )
Changelog for 8.12.1. (27d9145 )
Backport PR #13311: Changelog for 8.12.1. (8397986 )
ppedrot pushed 2 commits to branch master. Commits by herbelin (1) and ppedrot (1).
Fixing interpretation of rewrite_strat argument in Ltac. (c233a13 )
Merge PR #13284: Fixing interpretation of rewrite_strat argument in Ltac (d7bf4b4 )
coqbot-app[bot] pushed 4 commits to branch master. Commits by herbelin (3) and coqbot-app[bot] (1).
Adding a typed interpretation of patterns. (011de69 )
Typing patterns and using type constraints in Search. (2355b3e )
Adding change log for #13255. (3515988 )
Merge PR #13255: Fixes #13244: support for coercions in Search (e5dc6e5 )
coqbot-app[bot] pushed 8 commits to branch master. Commits by ppedrot (7) and coqbot-app[bot] (1).
Further API cleanup after the removal of forward hints. (ae4346d )
Encapsulate the last use of IsConstr in the Hints API. (511a3ea )
Opacify the Hints.hint_term type. (be33260 )
Do not try to be clever for term-as-hint interpretation. (f4c1b8b )
Further code simplification in arbitrary hint interpretation. (ab6ebfc )
Document the changes. (be51c8e )
Add overlays. (1241353 )
Merge PR #13139: Clean the constr-as-hint API (6cebd41 )
coqbot-app[bot] pushed 46 commits to branch master. Commits by jashug (45) and coqbot-app[bot] (1).
Modify Numbers/Integer/Abstract/ZAdd.v to compile with -mangle-names (d0be4a3 )
Modify Numbers/Integer/Abstract/ZAddOrder.v to compile with -mangle-names (9a55d46 )
Modify Numbers/Integer/Abstract/ZMulOrder.v to compile with -mangle-names (f960474 )
Modify Numbers/Integer/Abstract/ZMaxMin.v to compile with -mangle-names (f02b3e5 )
Modify Numbers/Integer/Abstract/ZSgnAbs.v to compile with -mangle-names (d2e0606 )
Modify Numbers/Integer/Abstract/ZParity.v to compile with -mangle-names (c5f7670 )
Modify Numbers/Integer/Abstract/ZPow.v to compile with -mangle-names (4ffac2e )
Modify Numbers/Integer/Abstract/ZDivTrunc.v to compile with -mangle-names (806421f )
Modify Numbers/Integer/Abstract/ZDivFloor.v to compile with -mangle-names (8c3231d )
Modify Numbers/Integer/Abstract/ZGcd.v to compile with -mangle-names (460a9bb )
Modify Numbers/Integer/Abstract/ZLcm.v to compile with -mangle-names (dd66aba )
Modify Numbers/Integer/Abstract/ZBits.v to compile with -mangle-names (fb073d9 )
Modify ZArith/BinInt.v to compile with -mangle-names (2d3eb55 )
Modify setoid_ring/Ring_polynom.v to compile with -mangle-names (ef71158 )
Modify ZArith/Zorder.v to compile with -mangle-names (d5c202a )
Modify Bool/Sumbool.v to compile with -mangle-names (6e0585f )
Modify ZArith/ZArith_dec.v to compile with -mangle-names (8773467 )
Modify setoid_ring/InitialRing.v to compile with -mangle-names (6b04433 )
Modify setoid_ring/Ring.v to compile with -mangle-names (f136bcf )
Modify Arith/Even.v to compile with -mangle-names (17ba1c4 )
[and 26 more commit(s)]
ppedrot pushed 3 commits to branch master. Commits by herbelin (2) and ppedrot (1).
Fixes #13216 (use of type classes in the return clause of a match). (a9745d9 )
Adding change log for #13217. (1a36a0e )
Merge PR #13217: Addresses #13216: use of type classes in the return clause of a match. (07472bc )
coqbot-app[bot] pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot-app[bot] (1).
Fix macOS CI / disable bundle generation. (602af83 )
Merge PR #13310: Fix macOS CI on Azure. (d2047c6 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by Zimmi48 (2) and coqbot-app[bot] (1).
Fix indentation of todo in Ltac chapter. (c0b4899 )
Fix #5226: Add index entry for ::=. (3f5f5cf )
Merge PR #13327: Fix documentation of Ltac ::= (fa8d3d7 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by Zimmi48 (2) and coqbot-app[bot] (1).
Remove virtually unused replace rule. (87523f1 )
[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina. (a3869e5 )
Merge PR #13329: [refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina. (e38d3ba )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ppedrot (1).
Remove the native symbol registering from the safe environment. (fb5aa52 )
Merge PR #13297: Remove the native symbol registering from the safe environment. (449aef5 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ejgallego (1).
[obligation] Proper handle no obligations on Next Obligation
(b1cb26e )
Merge PR #13322: [obligation] Properly handle no obligations on Next Obligation
(2676541 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and gares (1).
[compat] remove 8.10 (a028e70 )
Merge PR #13325: [compat] remove 8.10 (fa6c67d )
Zimmi48 pushed 5 commits to branch v8.12.
Fix macOS CI / disable bundle generation. (3722ed8 )
Backport PR #13310: Fix macOS CI on Azure. (4f9b497 )
Fix indentation of todo in Ltac chapter. (b7052b2 )
Fix #5226: Add index entry for ::=. (8ce14dd )
Backport PR #13327: Fix documentation of Ltac ::= (8264f46 )
coqbot-app[bot] pushed 4 commits to branch master. Commits by jfehrle (3) and coqbot-app[bot] (1).
Add global version of OPTINREF (a9658f2 )
Add additional escape sequences for notations (7d8389d )
Convert logic.rst to prodn (da9fd81 )
Merge PR #13315: Convert logic chapter to prodn (417e8c5 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Fix running unit tests with dune compiled coq (400f852 )
Merge PR #13335: Fix running unit tests with dune compiled coq (af42e1b )
coqbot-app[bot] pushed 4 commits to branch master. Commits by CohenCyril (3) and coqbot-app[bot] (1).
Intro pattern extensions for dup, swap and apply (79c45ec )
Update doc/changelog/06-ssreflect/13317-ssr_dup_swap_apply_ipat.rst (54c3b49 )
fixup (7bd93b0 )
Merge PR #13317: [ssr] intro pattern extensions for dup, swap and apply (9dfc627 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by herbelin (2) and coqbot-app[bot] (1).
Clarifying the role of Add ML Path vs -I (see #13344). (f821fca )
Add changelog for #13345. (b7200b1 )
Merge PR #13345: Addressing #13344: clarifying the role of Add ML Path vs -I (0245aa2 )
ppedrot pushed 5 commits to branch master. Commits by herbelin (4) and ppedrot (1).
Cosmetic cleaning of uState.ml and related: a bit of doc, more unity in naming. (404a041 )
Moving interpretation of user-level universes in constrintern.ml . (78e600a )
Factorizing UState.make* through UState.from_env, to highlight the similarity. (4814c48 )
Documentation of the main entry points of uState.mli. (e7b39c7 )
Merge PR #13289: Cosmetic cleaning of uState.ml : a bit of doc, more unity in naming (c53abd9 )
coqbot-app[bot] pushed 4 commits to branch master. Commits by ppedrot (3) and coqbot-app[bot] (1).
Fix #13330: Kernel messes with polymorphic side-effects. (0ca6641 )
Add documentation about the soundness bug. (aa6d64c )
Add the test as a misc script. (332bb8c )
Merge PR #13331: Fix #13330: Kernel messes with polymorphic side-effects. (2414063 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Fix Iris CI script (18db1c0 )
Merge PR #13355: Fix Iris CI script (7ba0985 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by herbelin (2) and coqbot-app[bot] (1).
Addressing #13349: accept Search on subparts of ident, not only on subidents. (696b979 )
Add changelog for #13351. (b9f4ed8 )
Merge PR #13351: Fixes #13349: accept Search on subparts of an identifier, not only on subidentifiers of an identifier (6d78778 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Print failed test suite logs in CI (0cbd6c2 )
Merge PR #13359: Print failed test suite logs in CI (176faf1 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot-app[bot] (1).
Move last changelog entry for 8.12.1. (0e318ee )
Merge PR #13361: Move last changelog entry for 8.12.1. (8246730 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and herbelin (1).
The "( X in t )" hack used in the syntax of ssr rewrite may be only parsing. (c470b92 )
Merge PR #13318: Turn ssr proxy notation for supporting second-order/contextual pattern abbreviations to only parsing (dedf3f4 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by LasseBlaauwbroek (1) and coqbot-app[bot] (1).
Change Dumpglob.pause and Dumpglob.continue into push and pop (954f278 )
Merge PR #13253: Change Dumpglob.pause and Dumpglob.continue into push and pop (a10e7b3 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and liyishuai (1).
[stdlib] Decidable instance for negation (9d63d29 )
Merge PR #12420: [stdlib] Decidable instance for negation (51e759f )
Zimmi48 pushed 9 commits to branch v8.12. Commits by Zimmi48 (4), ppedrot (3) and herbelin (2).
Fix #13330: Kernel messes with polymorphic side-effects. (3b16563 )
Add documentation about the soundness bug. (ee98750 )
Add the test as a misc script. (bf05654 )
Backport PR #13331: Fix #13330: Kernel messes with polymorphic side-effects. (2277895 )
Addressing #13349: accept Search on subparts of ident, not only on subidents. (e0e7e82 )
Add changelog for #13351. (99e8b2b )
Backport PR #13351: Fixes #13349: accept Search on subparts of an identifier, not only on subidentifiers of an identifier (b3fa585 )
Move last changelog entry for 8.12.1. (3fa99fe )
Backport PR #13361: Move last changelog entry for 8.12.1. (056d6d8 )
coqbot-app[bot] pushed 4 commits to branch master. Commits by ppedrot (3) and coqbot-app[bot] (1).
Statically ensure that native update locations are of form Linked*. (a0080f1 )
Statically ensure that the native interactive flag is always set to true. (c12471f )
Merge the Linked and LinkedInteractive constructors. (9cf4248 )
Merge PR #13358: Merge the Linked / LinkedInteractive native link information constructors (9a93f58 )
Zimmi48 pushed 2 commits to branch v8.12.
Bump version number to 8.12.1. (fedf4ff )
Merge PR #13367: [v8.12] Bump version number to 8.12.1. (b745140 )
Zimmi48 pushed tag V8.12.1.
coqbot-app[bot] pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot-app[bot] (1).
Move destructuring let syntax closer to its documentation. (15183aa )
Merge PR #13369: Move destructuring let syntax closer to its documentation. (6b7d6be )
ppedrot pushed 3 commits to branch master. Commits by SkySkimmer (2) and ppedrot (1).
Remove unused CClosure.FNativeEntries.farray (e733f11 )
Make the universe of primitive arrays irrelevant (89f5d25 )
Merge PR #13356: Make the universe of primitive arrays irrelevant (ecea6ed )
ppedrot pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Fix incorrect "avoid" set in globenv extra data (7648316 )
Merge PR #13350: Fix incorrect "avoid" set in globenv extra data (a237a3d )
ppedrot pushed 5 commits to branch master. Commits by Zimmi48 (4) and ppedrot (1).
Add support for Proof using in -noinit mode. (3fa2430 )
Revert to "using" not being a keyword in -noinit mode. (1117058 )
Test case for Proof using in -noinit mode. (403a905 )
Add changelog entry for Proof using in -noinit mode. (8ed2d80 )
Merge PR #13339: In -noinit mode, add support for Proof using, using is not a keyword. (a118b90 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and jfehrle (1).
Distinguish one_pattern and one_term nonterminals (5c51dc7 )
Merge PR #13375: Distinguish one_pattern and one_term nonterminals, improve description of Instance command (e476ded )
coqbot-app[bot] pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot-app[bot] (1).
Fix dune rules for @check-gram following recent changes. (53aa272 )
Merge PR #13368: Fix dune rules for @check-gram following recent changes. (3ea3da2 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by herbelin (2) and coqbot-app[bot] (1).
Avoiding encapsulating exceptions w/o a handler in NotFoundInstance. (c385322 )
Add changelog for #13376. (bad1d9a )
Merge PR #13376: Fixes #13266: Avoiding encapsulating exceptions w/o a handler in NotFoundInstance (010dfd5 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by herbelin (2) and coqbot-app[bot] (1).
Fixes #11816: using {wf ...} in a local fixpoint is an error, not an anomaly. (d0ed43b )
Add changelog for #13383. (3687c3f )
Merge PR #13383: Fixes #11816: using {wf ...} in a local fixpoint is an error, not an anomaly (93ee640 )
Lysxia pushed 6 commits to branch master. Commits by herbelin (5) and Lysxia (1).
Reorganizing the printing of warnings; fixing line count. (a9e3dbd )
Dead code in coqdoc. (b01fb01 )
Addressing #13304: how to verbatim an expression mentioning >>. (7923bb5 )
Documenting one-line verbatim. (0b12bb8 )
Coqdoc: we move a newline at a better place. (696df50 )
Merge PR #13308: Address #13304: in coqdoc, clearly distinguish block verbatim from inline verbatim (5ec45d7 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ejgallego (1).
[dune] [opam] Generate opam files automatically using Dune. (061998b )
Merge PR #13374: [dune] [opam] Generate opam files automatically using Dune. (4152392 )
coqbot-app[bot] pushed 7 commits to branch master. Commits by ejgallego (6) and coqbot-app[bot] (1).
[record] Cleanup of data structure and functions [1/2] (b341b58 )
[record] Cleanup of data structure and functions [2/2] (e47d394 )
[record] Refactor nested functions. (d4ce120 )
[record] Options API cleanup. (df19ab7 )
[record] [ci] Overlay for elpi (593e995 )
[record] Some documentation + minor refactoring (94048f8 )
Merge PR #12611: [record] Cleanup of data structure and functions (db3a056 )
coqbot-app[bot] pushed 5 commits to branch master. Commits by herbelin (4) and coqbot-app[bot] (1).
Useless evar type for typing impossible case. (391898b )
Fine-tuning the sort of the predicate obtained by small inversion. (710f749 )
Closes #13278: take into account elimination constraints in small inversion. (f8f915d )
Adding overlay for PR #13290. (7b8ed62 )
Merge PR #13290: Grant #13278: computation of return predicate takes care of sort elimination constraints (779d2b9 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by Lysxia (2) and coqbot-app[bot] (1).
Fix proof of Coq.Program.Wf.Fix_F_inv to be axiom-free (e3a6e5f )
Add changelog for #13365 (dafb535 )
Merge PR #13365: Fix proof of Coq.Program.Wf.Fix_F_inv to be axiom-free (4775fd7 )
coqbot-app[bot] pushed 4 commits to branch master. Commits by ppedrot (3) and coqbot-app[bot] (1).
Implement export locality for the remaining Hint commands. (ae56bbe )
Adding an output test to check that the hint commands respect their locality. (46d0d39 )
Document the new export locality for the remaining hint commands. (7e55f48 )
Merge PR #13388: Export locality for all hint commands (57fb6f1 )
ppedrot pushed 3 commits to branch master. Commits by herbelin (2) and ppedrot (1).
Propagating scope information in indirect application to a reference. (69a3d31 )
Adding change log for #12685. (4a6a7ea )
Merge PR #12685: Propagating scope information in indirect application to a reference. (abde113 )
ppedrot pushed 4 commits to branch master. Commits by SkySkimmer (3) and ppedrot (1).
Default disable automatic generalization of Instance type (bb3f884 )
Doc and changelog for Instance Generalized Output (59ea396 )
Update compate Coq812.v (f8f3ea0 )
Merge PR #13188: Default disable automatic generalization of Instance type (deb4206 )
coqbot-app[bot] pushed 4 commits to branch master. Commits by herbelin (3) and coqbot-app[bot] (1).
Locating the Ill-typed evar instance error. (4b4ae13 )
Fixes #12348: long-standing de Bruijn indices bug in imitation (solve_simple_eqn). (6ae2994 )
Add changelog for #13387. (603023b )
Merge PR #13387: Fixes #12348: de Bruijn indices bug in the imitation part of unification (8a1e9bb )
coqbot-app[bot] pushed 3 commits to branch master. Commits by Zimmi48 (1), coqbot-app[bot] (1) and jfehrle (1).
Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto" (51ddbbe )
Slight improvement to the changelog entry. (7b8da8c )
Merge PR #13381: Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto" (c3e7b6b )
ppedrot pushed 3 commits to branch master. Commits by ppedrot (2) and maximedenes (1).
Deprecate Grab Existential Variables
and Existential
commands (e348b1b )
Document the deprecation of the commands. (1670638 )
Merge PR #12516: Deprecate Grab Existential Variables
and Existential
commands (8b156dc )
coqbot-app[bot] pushed 3 commits to branch master. Commits by herbelin (2) and coqbot-app[bot] (1).
Fixes #13363: case of a meta not paying attention to being under binders. (c6529d8 )
Add changelog for #13373. (6600493 )
Merge PR #13373: Fixes #13363: in pose_all_metas_as_evars, use the context of the definition of the metas (89a4b7e )
coqbot-app[bot] pushed 3 commits to branch master. Commits by herbelin (2) and coqbot-app[bot] (1).
Avoid exposing an internal names when "intros _ H" fails. (eae015f )
Add changelog for #13337. (5ded9ca )
Merge PR #13337: Avoid exposing an internal name when "intros _ H" fails because of _ being dependent in H (1369d14 )
coqbot-app[bot] pushed 6 commits to branch master. Commits by herbelin (5) and coqbot-app[bot] (1).
Indentation. (534d440 )
Moving the analysis of notation strings in notation.ml . (3ac39cd )
Fixing Locate for recursive notations with names. (60d15dc )
Adding support for Locate "( x , y )". (5b7a1d7 )
Ensuring the body of the notation in Locate is printed at level 0. (35ea105 )
Merge PR #12690: Mini-fix of Locate for recursive notations using named variables. (fb186f2 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and herbelin (1).
Fixing the "IllTypedInstance" anomaly part of #5512. (daba2d7 )
Merge PR #13380: Fixing the "IllTypedInstance" anomaly part of #5512 (58b24bd )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and herbelin (1).
Suggesting to use injection when an injection pattern is given to destruct. (cf41055 )
Merge PR #13212: Suggesting to use injection when an injection pattern is given to destruct (wish #13205) (a400dbf )
coqbot-app[bot] pushed 6 commits to branch master. Commits by ppedrot (5) and coqbot-app[bot] (1).
Warning on hint commands that have no explicit locality. (7daf04e )
Explicitly annotate all hint declarations of the standard library. (68cd077 )
Fix test-suite. (3c9908f )
Tentative fix for the refman. (3fe5f96 )
Document the new warning. (4f28dd4 )
Merge PR #13384: Warn on hints without an explicit locality (af96434 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ejgallego (1).
[gc] Set GC policy as best-fit in OCaml >= 4.10.0 (6a6069d )
Merge PR #13040: [gc] Set GC policy as best-fit in OCaml >= 4.10.0 (29dc0d5 )
coqbot-app[bot] pushed 4 commits to branch master. Commits by herbelin (3) and coqbot-app[bot] (1).
Fixing a (known) "bugged" part of imitation in unification. (47c05b2 )
Checking type in unification imitation: avoid raising a non-located error. (a8b2525 )
Overlay for Coq-Equations. (6f31bee )
Merge PR #12873: Unification: A type-checking fix in imitation + an error locating fix (04b25a7 )
gares pushed the branch v8.13.
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and tchajed (1).
[ci] Use lite target for Perennial (7c6ebab )
Merge PR #13402: [ci] Use lite target for Perennial (81ff5b8 )
coqbot-app[bot] pushed 8 commits to branch master. Commits by SkySkimmer (6), coqbot-app[bot] (1) and jfehrle (1).
Infrastructure for cumulative inductive syntax (no grammar extension yet) (9990bea )
Syntax for specifying cumulative inductives (3c8fd95 )
Doc for variance syntax (a947a60 )
Overlays for cumulative inductive syntax (ed6bee7 )
Changelog for variance syntax (e511ef1 )
Update grammar in doc (19f7d82 )
Improve bad variance error message: mention expected and actual variances (f3c24a6 )
Merge PR #12653: Syntax for specifying cumulative inductives (60f25e2 )
ppedrot pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Persistent_cache.t is always Open (cdbda92 )
Merge PR #13404: Persistent_cache.t is always Open (f1b7a37 )
ppedrot pushed 2 commits to branch master. Commits by herbelin (1) and ppedrot (1).
Adding heterogeneous map on named contexts. (05cf3fc )
Merge PR #13397: Adding heterogeneous map on named contexts. (7c79a0d )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Intern application arguments in left-to-right order (81a3f81 )
Merge PR #13390: Intern application arguments in left-to-right order (396de34 )
gares pushed 2 commits to branch v8.13. Commits by gares (1) and tchajed (1).
[ci] Use lite target for Perennial (8e878e0 )
Backport PR #13402: [ci] Use lite target for Perennial (d570b09 )
ppedrot pushed 2 commits to branch master. Commits by LasseBlaauwbroek (1) and ppedrot (1).
Make sure that setoid_rewrite passes state to subgoals (a9e0805 )
Merge PR #13251: Make sure that setoid_rewrite passes state to subgoals (54e65eb )
ppedrot pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Finish fixing setoid rewrite under anonymous lambdas (hopefully) (bffa084 )
Merge PR #13341: Finish fixing setoid rewrite under anonymous lambdas (hopefully) (73a068c )
gares pushed 2 commits to branch v8.13.
[ci] pin user developments (702da63 )
Merge PR #13401: [ci] pin user developments (7b2f311 )
coqbot-app[bot] pushed 4 commits to branch master. Commits by herbelin (3) and coqbot-app[bot] (1).
In recursive notations, accept partial application over the recursive pattern. (ca0e42c )
Adding change log for #12765. (5b3b6ee )
Ref. man.: showing the x ⪯ y ⪯ .. ⪯ z ⪯ t example of recursive notation. (1826974 )
Merge PR #12765: In recursive notations, accept partial application over the recursive pattern (4a56d4d )
coqbot-app[bot] pushed 3 commits to branch master. Commits by herbelin (2) and coqbot-app[bot] (1).
We move the example of Makefile wrapper next to the explanations about CoqMakefile. (5326939 )
Update doc/sphinx/practical-tools/utilities.rst (3fb5c77 )
Merge PR #13220: Give a typical example of Makefile wrapper for coq_makefile (addresses #12903) (162c19c )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and gares (1).
[doc] add a link to v8.13 (16c3545 )
Merge PR #13400: [doc] add a link to v8.13 (e633413 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and gares (1).
[configure] check that zarith dev files are available (c3ea4b4 )
Merge PR #13410: [configure] check that zarith dev files are available (e2f2966 )
MSoegtropIMC pushed 2 commits to branch master. Commits by MSoegtropIMC (1) and Zimmi48 (1).
[ci/gitlab/windows] Do not load user overlays. (c023016 )
Merge PR #13389: [ci/gitlab/windows] Do not load user overlays. (fea83b0 )
coqbot-app[bot] pushed 8 commits to branch master. Commits by ejgallego (5), Zimmi48 (2) and coqbot-app[bot] (1).
[attributes] Allow boolean, single-value attributes. (e0380f3 )
[attributes] Deprecate attr(true)
syntax in favor of booelan attributes. (c609c05 )
[attributes] Add overlays for #13312 (0af10d8 )
Run doc_grammar for #13312. (3b47935 )
Review commit: improving the doc of boolean attributes. (ca42305 )
[attributes] Update error message referring to deprecated syntax. (6aeee2e )
[attributes] Add output test suite for errors, improve error printing. (efa6673 )
Merge PR #13312: [attributes] Allow boolean, single-value attributes. (7ebdf6b )
gares pushed 11 commits to branch v8.13. Commits by SkySkimmer (6), gares (4) and jfehrle (1).
Infrastructure for cumulative inductive syntax (no grammar extension yet) (8feb553 )
Syntax for specifying cumulative inductives (7f67dc8 )
Doc for variance syntax (aba745c )
Overlays for cumulative inductive syntax (6e45878 )
Changelog for variance syntax (739830e )
Update grammar in doc (e8aeb9b )
Improve bad variance error message: mention expected and actual variances (3ffd04c )
Backport PR #12653: Syntax for specifying cumulative inductives (50f3662 )
[ci] update pins after 12653 (a5bb6fc )
[doc] add a link to v8.13 (c7053e2 )
Backport PR #13400: [doc] add a link to v8.13 (bc1358c )
coqbot-app[bot] pushed 9 commits to branch master. Commits by herbelin (8) and coqbot-app[bot] (1).
Fixing alpha-equality of notation interpretations with recursive patterns. (22c8fcf )
Adding Array.iter3. (213207a )
For printing, ordering notations by precision of the pattern. (2823c88 )
Documenting the preference given to more precise notations at printing time. (849a450 )
Add changelog for #12986. (857b8eb )
A reimport of notations now put the corresponding notations again in front. (748458d )
Documenting priority given to most recently declared/imported notations. (5e87ba2 )
Adding change log for #12984. (73a2675 )
Merge PR #12984: [printing] Order notations by matching precision first, and then by last imported (01dea07 )
ppedrot pushed 16 commits to branch master. Commits by silene (14), ppedrot (1) and proux01 (1).
Optimize handling of the VM stack with respect to the GC. (930e51c )
Remove unchecked arithmetic operations from VM, as they are not used. (fdd1611 )
Remove some unused opcodes from VM. (aebc10a )
Restore discard_dead_code and use it to simplify match-with constructs. (2032110 )
Remove unused if-then-else construct from VM. (2d3e012 )
Turn Ksequence into a unary opcode, as its binary structure was never used. (4e2bd77 )
Improve documentation of closure representations. (0d6f8e4 )
Optimize Is_accu a bit. (20c511d )
Make callback opcodes more generic. (b6fadbf )
Inline the functions from coq_float64.h. (136454f )
Turn coq_float64.h into a .c file as it is no longer needed by coq_interp.c. (5b2d1c0 )
Remove floating-point comparison operators as they are no longer needed. (c9cf844 )
Add allocation-free variants of the nextup and nextdown floating-point operations. (5c7f63f )
Hardcode next_up and next_down instead of relying on nextafter. (ef3ec53 )
Add more explicit tests for next_up and next_down. (9815b59 )
Merge PR #12959: Improve the bytecode interpreter (3037172 )
gares pushed 35 commits to branch v8.13. Commits by herbelin (13), gares (11), ejgallego (5) and others (6).
We move the example of Makefile wrapper next to the explanations about CoqMakefile. (eba48cd )
Update doc/sphinx/practical-tools/utilities.rst (40059b6 )
Backport PR #13220: Give a typical example of Makefile wrapper for coq_makefile (addresses #12903) (4191117 )
[attributes] Allow boolean, single-value attributes. (6c8413d )
[attributes] Deprecate attr(true)
syntax in favor of booelan attributes. (3f21c76 )
[attributes] Add overlays for #13312 (3b1a787 )
Run doc_grammar for #13312. (f36a343 )
Review commit: improving the doc of boolean attributes. (fc69da3 )
[attributes] Update error message referring to deprecated syntax. (37bd076 )
[attributes] Add output test suite for errors, improve error printing. (374d80d )
Backport PR #13312: [attributes] Allow boolean, single-value attributes. (be206c1 )
[ci] update pin after 13312 (2f0b75e )
Intern application arguments in left-to-right order (9d1d606 )
Backport PR #13390: Intern application arguments in left-to-right order (2f933f2 )
Make sure that setoid_rewrite passes state to subgoals (3bf91da )
Backport PR #13251: Make sure that setoid_rewrite passes state to subgoals (dd5c0b3 )
Finish fixing setoid rewrite under anonymous lambdas (hopefully) (4322c28 )
Backport PR #13341: Finish fixing setoid rewrite under anonymous lambdas (hopefully) (c52bbf3 )
In recursive notations, accept partial application over the recursive pattern. (b0348d6 )
Adding change log for #12765. (4dab2e5 )
[and 15 more commit(s)]
coqbot-app[bot] pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot-app[bot] (1).
Fix typo in rst link syntax. (ff1fe87 )
Merge PR #13421: Fix typo in rst link syntax. (c7686fe )
coqbot-app[bot] pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot-app[bot] (1).
[changelog] Indicate a replacement for deprecated syntax of debug / info_eauto. (c63c397 )
Merge PR #13423: [changelog] Indicate a replacement for deprecated syntax of debug / info_eauto. (345328c )
gares pushed 20 commits to branch v8.13. Commits by silene (14), gares (3), Zimmi48 (2) and others (1).
Optimize handling of the VM stack with respect to the GC. (dd25e1a )
Remove unchecked arithmetic operations from VM, as they are not used. (deff48a )
Remove some unused opcodes from VM. (c62b0db )
Restore discard_dead_code and use it to simplify match-with constructs. (5c59538 )
Remove unused if-then-else construct from VM. (3585cc4 )
Turn Ksequence into a unary opcode, as its binary structure was never used. (3c923eb )
Improve documentation of closure representations. (f6d941b )
Optimize Is_accu a bit. (e323765 )
Make callback opcodes more generic. (d18fa76 )
Inline the functions from coq_float64.h. (c4c95d0 )
Turn coq_float64.h into a .c file as it is no longer needed by coq_interp.c. (853bb4f )
Remove floating-point comparison operators as they are no longer needed. (7083b2c )
Add allocation-free variants of the nextup and nextdown floating-point operations. (ce830fc )
Hardcode next_up and next_down instead of relying on nextafter. (f795900 )
Add more explicit tests for next_up and next_down. (c2afd90 )
Backport PR #12959: Improve the bytecode interpreter (2fbf77b )
Fix typo in rst link syntax. (444d89b )
Backport PR #13421: Fix typo in rst link syntax. (fca9227 )
[changelog] Indicate a replacement for deprecated syntax of debug / info_eauto. (1a5a973 )
Backport PR #13423: [changelog] Indicate a replacement for deprecated syntax of debug / info_eauto. (9bd3c44 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Extend hack to use postponed constraints in retyping to template poly (0fff401 )
Merge PR #13371: Extend hack to use postponed constraints in retyping to template poly (f264aab )
coqbot-app[bot] pushed 5 commits to branch master. Commits by herbelin (4) and coqbot-app[bot] (1).
Fixes #9971: expand_projections failing on primitive projections of unknown type. (a27fb3c )
Use a proper canonical structure entry for projections. (115fe6b )
Add changelog for #13386. (216f4f1 )
Add overlays for elpi and unicoq. (7265df1 )
Merge PR #13386: Fixes #9971: a useless situation where the type of a primitive projection was wrongly supposed to be already inferred (57c85b0 )
gares pushed 1 commit to branch gares-patch-ssr-doc-reflect.
[doc] [ssr] fix documentation of reflect (fe56bc9 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and jfehrle (1).
Use only nats for occs_nums rather than ints (00003b6 )
Merge PR #13403: Use only nats for occs_nums rather than ints (122aef5 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Fix incorrect name refreshing when interning a generalized binder (f6a8c25 )
Merge PR #13360: Fix incorrect name refreshing when interning a generalized binder (a8a0285 )
ppedrot pushed 3 commits to branch master. Commits by SkySkimmer (2) and ppedrot (1).
Small cleanup in ComInductive (41840f9 )
Only lower inductives to Prop if the type is syntactically an arity. (f09eef2 )
Merge PR #13305: Only lower inductives to Prop if the type is syntactically an arity. (1fd6af1 )
ppedrot pushed 3 commits to branch master. Commits by herbelin (2) and ppedrot (1).
Fixes #13235: remove fragile tolerance for degenerate in-hyps clause. (f1e1f81 )
Adding changelog for #13237. (6adbb8b )
Merge PR #13237: Address #13235: avoid passing degenerate in-hyps clauses (04186f8 )
gares pushed 12 commits to branch v8.13. Commits by gares (5), herbelin (4), SkySkimmer (2) and others (1).
Fixes #9971: expand_projections failing on primitive projections of unknown type. (d72dde8 )
Use a proper canonical structure entry for projections. (84d6fed )
Add changelog for #13386. (be39bc2 )
Add overlays for elpi and unicoq. (8a289e4 )
Backport PR #13386: Fixes #9971: a useless situation where the type of a primitive projection was wrongly supposed to be already inferred (25c4f8d )
Extend hack to use postponed constraints in retyping to template poly (df47d65 )
Backport PR #13371: Extend hack to use postponed constraints in retyping to template poly (3a912d1 )
Use only nats for occs_nums rather than ints (7330277 )
Backport PR #13403: Use only nats for occs_nums rather than ints (a733a72 )
Fix incorrect name refreshing when interning a generalized binder (d3bc422 )
Backport PR #13360: Fix incorrect name refreshing when interning a generalized binder (25c1e12 )
[ci] update pins after 13386 (0031972 )
ppedrot pushed 4 commits to branch master. Commits by herbelin (2), VincentSe (1) and ppedrot (1).
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and gares (1).
[doc] [ssr] fix documentation of reflect (fe56bc9 )
Merge PR #13426: [doc] [ssr] fix documentation of reflect (1aca82b )
gares deleted the branch gares-patch-ssr-doc-reflect.
coqbot-app[bot] pushed 3 commits to branch master. Commits by ejgallego (2) and coqbot-app[bot] (1).
[stm] [declare] Try to propagate safe bits of proof information (36aeb43 )
[stm] [declare] Remove pinfo internals hack. (b832d48 )
Merge PR #13425: [stm] [declare] Try to propagate safe bits of proof information (614675f )
coqbot-app[bot] pushed 5 commits to branch master. Commits by herbelin (4) and coqbot-app[bot] (1).
Fix #9569 (notations collect the spine binding variables at printing time). (094c395 )
Add change log for #12965. (cd8aefc )
Using labels to document match_notation_constr. (55389f1 )
Update doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst (d13abaf )
Merge PR #12965: Fixes #9569: in notations with binders, prevent collisions between variable and non-qualified global references (6479926 )
gares pushed 6 commits to branch v8.13. Commits by SkySkimmer (2), gares (2) and herbelin (2).
Small cleanup in ComInductive (ea5be4b )
Only lower inductives to Prop if the type is syntactically an arity. (03a9df3 )
Backport PR #13305: Only lower inductives to Prop if the type is syntactically an arity. (188f553 )
Fixes #13235: remove fragile tolerance for degenerate in-hyps clause. (e593d76 )
Adding changelog for #13237. (265295b )
Backport PR #13237: Address #13235: avoid passing degenerate in-hyps clauses (ce9fb85 )
ppedrot pushed 2 commits to branch master. Commits by RalfJung (1) and ppedrot (1).
add perennial to benchmark suite (6188353 )
Merge PR #13233: add perennial to benchmark suite (1a97ab1 )
gares pushed 8 commits to branch v8.13. Commits by herbelin (4), ejgallego (2) and gares (2).
[stm] [declare] Try to propagate safe bits of proof information (b762060 )
[stm] [declare] Remove pinfo internals hack. (9d5fc59 )
Backport PR #13425: [stm] [declare] Try to propagate safe bits of proof information (fa39254 )
Fix #9569 (notations collect the spine binding variables at printing time). (61947d4 )
Add change log for #12965. (7b2211f )
Using labels to document match_notation_constr. (1775a2f )
Update doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst (67231d3 )
Backport PR #12965: Fixes #9569: in notations with binders, prevent collisions between variable and non-qualified global references (030d0de )
coqbot-app[bot] pushed 7 commits to branch master. Commits by proux01 (6) and coqbot-app[bot] (1).
Configure default value of -native-compiler (1596cdb )
Add default value of -native-compiler to coqc -config
(04b5b2e )
[CI] Update coq_makefile (146415f )
[CI] Deactivate native-compiler for a few tests that fail with it (787c458 )
[CI] Deactivate native-compiler in some jobs (673849e )
Add changelog (c95512b )
Merge PR #13352: Configure default value of -native-compiler (87a59a8 )
coqbot-app[bot] pushed 8 commits to branch master. Commits by herbelin (7) and coqbot-app[bot] (1).
Rewriting convoluted code of set_var_scope in constrintern.ml . (a61f437 )
Add preliminary support for notations with large class (non-recursive) binders. (52b93b5 )
A step towards supporting pattern cast deeplier. (23924af )
Enforcing when a binding variable has no explicit type in constr_notation. (93654a0 )
Documentation of the support for general single binders in notations. (7508be4 )
Tests for notations with general single (non-recursive) binders. (3e6b9a0 )
Add changelog for #13265. (345bcc5 )
Merge PR #13265: Add support for general non-necessarily-recursive binders in notations (23d30fa )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Build all_stdlib.v in test suite makefile (76ab524 )
Merge PR #13248: Build all_stdlib.v in test suite makefile (5b15fce )
gares pushed 8 commits to branch v8.13. Commits by proux01 (6) and gares (2).
Configure default value of -native-compiler (c6f1f89 )
Add default value of -native-compiler to coqc -config
(f143a08 )
[CI] Update coq_makefile (d0848cd )
[CI] Deactivate native-compiler for a few tests that fail with it (b21882c )
[CI] Deactivate native-compiler in some jobs (14194d8 )
Add changelog (998d2ab )
Backport PR #13352: Configure default value of -native-compiler (7f6a29a )
[ci] update pins after 13352 (775af46 )
gares pushed 8 commits to branch v8.13. Commits by herbelin (7) and gares (1).
Rewriting convoluted code of set_var_scope in constrintern.ml . (74bffac )
Add preliminary support for notations with large class (non-recursive) binders. (5c6678a )
A step towards supporting pattern cast deeplier. (15acb16 )
Enforcing when a binding variable has no explicit type in constr_notation. (d209383 )
Documentation of the support for general single binders in notations. (44a6472 )
Tests for notations with general single (non-recursive) binders. (51ec6d5 )
Add changelog for #13265. (b441696 )
Backport PR #13265: Add support for general non-necessarily-recursive binders in notations (c090cc5 )
coqbot-app[bot] pushed 4 commits to branch master. Commits by silene (3) and coqbot-app[bot] (1).
Make sure accumulators do not exceed the minor heap (partly fix #11170). (2535afa )
Add a testcase. (5db79a4 )
Remove dependency on BinNat. (8e152ab )
Merge PR #13431: Make sure accumulators do not exceed the minor heap (partly fix #11170). (9d36da1 )
ppedrot pushed 3 commits to branch master. Commits by herbelin (2) and ppedrot (1).
Granting #9816: apply in takes several hypotheses. (efeccea )
Adding change log. (f4b5369 )
Merge PR #12246: Adding support for applying in several hypotheses at the same time (granting #9816) (9c84110 )
gares pushed 7 commits to branch v8.13. Commits by silene (3), gares (2) and herbelin (2).
Make sure accumulators do not exceed the minor heap (partly fix #11170). (9c5eeb7 )
Add a testcase. (f7d44cd )
Remove dependency on BinNat. (735fcd3 )
Backport PR #13431: Make sure accumulators do not exceed the minor heap (partly fix #11170). (c190825 )
Granting #9816: apply in takes several hypotheses. (c7485cc )
Adding change log. (b1a928d )
Backport PR #12246: Adding support for applying in several hypotheses at the same time (granting #9816) (2aa915b )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and jfehrle (1).
Use nat_or_var where negative values don't make sense (e74d328 )
Merge PR #13417: Use nat_or_var in grammar where negative values don't make sense (0326d06 )
ppedrot pushed 2 commits to branch master. Commits by LasseBlaauwbroek (1) and ppedrot (1).
Fix timeout by ensuring signal exceptions are not erroneously caught (6eb6f55 )
Merge PR #13377: Fix timeout by ensuring signal exceptions are not erroneously caught (8b3ad4d )
ppedrot pushed 2 commits to branch master. Commits by herbelin (1) and ppedrot (1).
Adding debugging printer for stacks of EConstr. (4b2ae1c )
Merge PR #13446: Adding debugging printer for stacks on EConstr (94d5798 )
coqbot-app[bot] pushed 5 commits to branch master. Commits by herbelin (4) and coqbot-app[bot] (1).
Renaming "ident" into "name" in grammar entries, to prevent confusions. (83e22b5 )
Uniformizing indentation in ppvernac.ml . (5ee4141 )
Adapting standard library, doc and test suite to ident->name renaming. (df8b5c7 )
Updating doc wrt addition of grammar subentry "name" and deprecation of "ident". (87c46c5 )
Merge PR #11841: Distinguishing entry "ident" from entry "name" in term notations. (5fce39e )
gares pushed tag V8.14+alpha.
gares pushed 9 commits to branch v8.13. Commits by gares (4), herbelin (4) and jfehrle (1).
Use nat_or_var where negative values don't make sense (bb20c08 )
Backport PR #13417: Use nat_or_var in grammar where negative values don't make sense (a80fc00 )
Renaming "ident" into "name" in grammar entries, to prevent confusions. (62c23ae )
Uniformizing indentation in ppvernac.ml . (3cb35d1 )
Adapting standard library, doc and test suite to ident->name renaming. (405aa80 )
Updating doc wrt addition of grammar subentry "name" and deprecation of "ident". (2c9d4b5 )
Backport PR #11841: Distinguishing entry "ident" from entry "name" in term notations. (1815977 )
pin compcert to tag v3.8 (3f49ef7 )
pin flocq to tag flocq-3.3.1 (cf3676d )
gares pushed 1 commit to branch v8.13.
pin extlib to tag v0.11.3 (790b41c )
gares pushed 1 commit to branch v8.13.
pin quickchick to tag v1.5.0 (b7dbb4e )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ppedrot (1).
Rename the confusing neutral annotation in CClosure. (969bed1 )
Merge PR #13411: Rename the confusing neutral annotation in CClosure. (f672ac2 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ppedrot (1).
Modular printing algorithm for bench/render_results. (5bda98c )
Merge PR #13420: Modular printing algorithm for bench/render_results. (fa70203 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and herbelin (1).
Fixes another instance of bug #7967: restriction of universes in "Context". (f5ccc82 )
Merge PR #13444: Fixes another instance of bug #7967 and #8076: restriction of universes in "Context" (90cb2b0 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Fix comparison of extracted array literals (60ed425 )
Merge PR #13455: Fix comparison of extracted array literals (b4cc5fa )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Fix linter: incorrect commit was picked in CI (c3b260c )
Merge PR #13466: Fix linter: incorrect commit was picked in CI (80110dc )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and herbelin (1).
Fixes #13432: regression with notations involving coercions caused by #11172. (d7446a6 )
Merge PR #13436: Fixes #13432: typo in #11172 causing notations mentioning a coercion not being used (9993147 )
gares pushed 2 commits to branch v8.13.
pin mtac2 to tag v1.4-coq8.13 (b873247 )
pin unicoq to tag v1.5-8.13 (111bea8 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by jfehrle (2) and coqbot-app[bot] (1).
Add COPYALL and APPENDALL edit ops, drop unneeded code (250ffd2 )
Convert auto chapter to prodn (b1846e8 )
Merge PR #13343: Update syntax in auto.rst chapter (6377fbe )
vbgl pushed 7 commits to branch master. Commits by ppedrot (6) and vbgl (1).
Add an explicit signature to the MakeCache functor in Micromega. (98dab0b )
Preserve sharing in the Micromega cache. (24da187 )
Alternative implementation of the Micromega persistent cache. (82a7e66 )
Regenerate the csdp cache for the test-suite. (f384a91 )
Keep accessed objects in memory in Persistent_cache. (8796546 )
Add a changelog. (132171c )
Merge PR #13405: Alternative implementation of the Micromega persistent cache (bde2235 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by CohenCyril (1) and coqbot-app[bot] (1).
Fixing [dup] and [swap] (5eb1828 )
Merge PR #13459: [ssr] Fixing [dup] and [swap] working around a bug (075811d )
ppedrot pushed 7 commits to branch master. Commits by fajb (6) and ppedrot (1).
[micromega/zify] expose more API for plugin users (0a6507a )
[micromega] Optimised cnf in case an hypothesis is trivially False. (8aa451b )
[micromega] More pre-procesing (d18fadb )
[micromega] Simplex uses alternatively Gomory cuts and case splits (06a7088 )
[micromega] Sort constraints before performing subst
(38e836a )
[micromega] Updated test-suite (0f0581b )
Merge PR #13228: [micromega] Performance of lia (bfd6a47 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and jfehrle (1).
Remove unused parsing code (2ca8fd3 )
Merge PR #13447: Remove unused parsing code (270b2be )
gares pushed 11 commits to branch v8.13. Commits by gares (6), jfehrle (2), CohenCyril (1) and others (2).
Fixing [dup] and [swap] (5ea9661 )
Backport PR #13459: [ssr] Fixing [dup] and [swap] working around a bug (1af757b )
Add COPYALL and APPENDALL edit ops, drop unneeded code (fd8ebe6 )
Convert auto chapter to prodn (ed7ecf1 )
Backport PR #13343: Update syntax in auto.rst chapter (688d695 )
Fixes #13432: regression with notations involving coercions caused by #11172. (0b96bbc )
Backport PR #13436: Fixes #13432: typo in #11172 causing notations mentioning a coercion not being used (7a48fc0 )
Fix comparison of extracted array literals (d1cc4dc )
Backport PR #13455: Fix comparison of extracted array literals (4f62d7e )
pin coquelicot to tag coquelicot-3.1.0 (ed90ec2 )
pin interval to tag interval-4.1.0 (d36c21e )
coqbot-app[bot] pushed 5 commits to branch master. Commits by gares (4) and coqbot-app[bot] (1).
[ci] variable CI_INSTALL_DIR to use with --prefix (572f48a )
[ci] job for menhir (94abc3d )
[ci] make compcert use flocq and menhir (dc8e605 )
[docker] don't install ocamlformat (e809ef5 )
Merge PR #13464: [CI] Compcert uses system libs (bef0e54 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and herbelin (1).
Add a new evar source to refer to evars which are types of evars. (4791000 )
Merge PR #13379: Add a new evar source to refer to evars which are types of evars (02a04a2 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by herbelin (2) and coqbot-app[bot] (1).
MacOS X install: accepting both dylib and so extensions for gtk immodules. (7020c7c )
tmp deactivation test-suite (8b66dc4 )
Merge PR #13476: MacOS X install: accepting both dylib and so extensions for gtk im modules (66429ec )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and gares (1).
[ci] bump elpi to 1.12.0 (f3f813a )
Merge PR #13481: [ci] elpi 1.12 (5c7f71a )
coqbot-app[bot] pushed 7 commits to branch master. Commits by SkySkimmer (6) and coqbot-app[bot] (1).
Reserve "sort_expr" for uninterned universes (2b80095 )
Separate interning and pretyping of universes (8106386 )
Clean UnivBinders test (1b49ddc )
Add tests for #13303 (fe597de )
Changelog for #13415 (817c3ed )
Overlays for #13415 (4011a91 )
Merge PR #13415: Separate interning and pretyping of universes (0fc82e9 )
coqbot-app[bot] pushed 7 commits to branch master. Commits by gares (6) and coqbot-app[bot] (1).
[ci] coquelicot, run make install (e794301 )
[ci] add job for interval (6637004 )
[ci] separate oddorder and fourcolor from mathcomp (fdf2f92 )
[ci] avoid always rebuilding jobs that use remake (0c3b900 )
[ci] coquelicot, depend on ssr proper (0c49f8c )
[ci] interval, disable native-compute (8ee0c8f )
Merge PR #13467: [ci] add job for interval (7f3c46a )
Zimmi48 pushed 3 commits to branch v8.12. Commits by herbelin (2) and Zimmi48 (1).
MacOS X install: accepting both dylib and so extensions for gtk immodules. (bc3d308 )
tmp deactivation test-suite (a3b6796 )
Backport PR #13476: MacOS X install: accepting both dylib and so extensions for gtk im modules (79c0e0d )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and herbelin (1).
Reactivate test-suite on MacOS X, accidently merged in #13476. (405e63c )
Merge PR #13491: Reactivate test-suite on MacOS X, accidently merged in #13476 (c294664 )
coqbot-app[bot] pushed 4 commits to branch master. Commits by gares (3) and coqbot-app[bot] (1).
Bump version numbers (d41bb0c )
Update compat infrastructure for 8.14 (17da7c4 )
update default.nix (f29decc )
Merge PR #13457: [RM] Update magicno & compat (bebd86f )
ppedrot pushed 2 commits to branch master. Commits by herbelin (1) and ppedrot (1).
Fixes #13456: regression where tactic exists started to check evars incrementally. (e353fe4 )
Merge PR #13468: Fixes #13456: regression in tactic exists which started to check resolution of evars more incrementally (4ca9cb8 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by CohenCyril (1) and coqbot-app[bot] (1).
Testing {in _, _} and {pred _} from ssrbool (36664ba )
Merge PR #13473: Testing {in _, _} and {pred _} from ssrbool (79d088f )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and fakusb (1).
Improved error message on nested proofs (c6cabd1 )
Merge PR #13482: Improved error message on nested proofs (2a21e55 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and gares (1).
[RM] script to notify "platform" projects to tag (d309974 )
Merge PR #13449: [RM] script to notify "platform" projects to tag (f733414 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and fakusb (1).
Fix #13283: improved error on clear implicit
flag (ce8569a )
Merge PR #13483: Fix #13283: improved error on clear implicit
flag (0501761 )
gares pushed 33 commits to branch v8.13. Commits by gares (23), SkySkimmer (6) and herbelin (4).
[ci] variable CI_INSTALL_DIR to use with --prefix (093e789 )
[ci] job for menhir (e5bae8b )
[ci] make compcert use flocq and menhir (e0ed28b )
[docker] don't install ocamlformat (e77a27e )
Backport PR #13464: [CI] Compcert uses system libs (05b3d99 )
MacOS X install: accepting both dylib and so extensions for gtk immodules. (b44de3c )
tmp deactivation test-suite (e806480 )
Backport PR #13476: MacOS X install: accepting both dylib and so extensions for gtk im modules (2e91bde )
[ci] bump elpi to 1.12.0 (4569e6b )
Backport PR #13481: [ci] elpi 1.12 (5334f33 )
Reserve "sort_expr" for uninterned universes (226f753 )
Separate interning and pretyping of universes (ffc4f87 )
Clean UnivBinders test (78039f4 )
Add tests for #13303 (983af71 )
Changelog for #13415 (ced00f8 )
Overlays for #13415 (67aff31 )
Backport PR #13415: Separate interning and pretyping of universes (1bb6ad7 )
[ci] coquelicot, run make install (f376ac1 )
[ci] add job for interval (a068228 )
[ci] separate oddorder and fourcolor from mathcomp (d77b573 )
[and 13 more commit(s)]
coqbot-app[bot] pushed 9 commits to branch master. Commits by ejgallego (8) and coqbot-app[bot] (1).
[declare] Allow custom typing flags when declaring constants. (b531ef3 )
[kernel] Allow to set typing flags in add_constant (b78f642 )
[kernel] Allow to set typing flags in add_mind [inductive] (5a9e90e )
[vernac] Allow to control typing flags with attributes. (1415024 )
[proofs] Support per-definition typing-flags in interactive proofs. (454a10d )
[environ] [typing_flags] Introduce helper function to remove duplicate code (2ac3d11 )
[attributes] [doc] Documentation review by Théo. (50af46a )
[attributes] [typing] Rename typing
to bypass_check
(1f0f1ae )
Merge PR #12586: [declare] Allow custom typing flags when declaring constants. (79946db )
coqbot-app[bot] pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot-app[bot] (1).
Revert "Remove deprecated tactic cutrewrite." (058ac64 )
Merge PR #13496: Revert "Remove deprecated tactic cutrewrite." (7f1b417 )
gares pushed 15 commits to branch v8.13. Commits by ejgallego (8), gares (4), fakusb (2) and others (1).
Improved error message on nested proofs (701e0ae )
Backport PR #13482: Improved error message on nested proofs (aadb979 )
Fix #13283: improved error on clear implicit
flag (e77d2af )
Backport PR #13483: Fix #13283: improved error on clear implicit
flag (ca60658 )
[declare] Allow custom typing flags when declaring constants. (bf3974a )
[kernel] Allow to set typing flags in add_constant (5483e27 )
[kernel] Allow to set typing flags in add_mind [inductive] (ed3188b )
[vernac] Allow to control typing flags with attributes. (73844ae )
[proofs] Support per-definition typing-flags in interactive proofs. (7d0b4a1 )
[environ] [typing_flags] Introduce helper function to remove duplicate code (8c1f408 )
[attributes] [doc] Documentation review by Théo. (b1ac7aa )
[attributes] [typing] Rename typing
to bypass_check
(1f91a2a )
Backport PR #12586: [declare] Allow custom typing flags when declaring constants. (4108808 )
Revert "Remove deprecated tactic cutrewrite." (fcf3cdb )
Backport PR #13496: Revert "Remove deprecated tactic cutrewrite." (187cc69 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by beta-ziliani (1) and coqbot-app[bot] (1).
extracting API for comparing universes of constants/inductives/constructors (7395f5a )
Merge PR #13479: extracting API for comparing universes of constants/inductives/constructors (16ebc10 )
gares pushed 3 commits to branch v8.13.
[docker] install boost, mpfr, flex, bison, autoconf-archive (a6fc199 )
[ci] add job for gappa (b13174c )
Backport PR #13472: [ci] Add job for gappa (24f5f1d )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
CI: Use hash of dockerfile in CACHEKEY (ea795d1 )
Merge PR #13487: CI: Use hash of dockerfile in CACHEKEY (7514bc2 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and jashug (1).
A small fix for freshness in the change
tactic (a1daae8 )
Merge PR #13502: A small fix for freshness in the change
tactic (9992bb1 )
ppedrot pushed 2 commits to branch master. Commits by herbelin (1) and ppedrot (1).
Fixing printing of apply in (continuation of #12246). (223c86e )
Merge PR #13514: Fixing printing of apply in (continuation of #12246) (ca8ee04 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and jfehrle (1).
Add missing print registration for wit_nat_or_var (54c1203 )
Merge PR #13510: Add missing print registration for wit_nat_or_var (db13ff6 )
gares pushed 6 commits to branch v8.13. Commits by gares (3), herbelin (1), jashug (1) and others (1).
Add missing print registration for wit_nat_or_var (a0281ad )
Backport PR #13510: Add missing print registration for wit_nat_or_var (cd3f90c )
Fixing printing of apply in (continuation of #12246). (890f6e6 )
Backport PR #13514: Fixing printing of apply in (continuation of #12246) (ea4c68b )
A small fix for freshness in the change
tactic (a48e83e )
Backport PR #13502: A small fix for freshness in the change
tactic (db75fe7 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and mattam82 (1).
[kernel] Fix #13495: incompleteness in cases typing for cumulative inductive types (d1fe597 )
Merge PR #13501: [kernel] Fix #13495: incompleteness in cases typing for cumulative inductive types (0ae001e )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ppedrot (1).
Micro-optimizations of the tight loop in Hashset. (d3777b5 )
Merge PR #13506: Micro-optimizations of the tight loop in Hashset. (0af89e4 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by SkySkimmer (1), coqbot-app[bot] (1) and mattam82 (1).
Use ~l2r:true to restore previous order of unfolding when typing predicates of cases. (36e2df3 )
Added comment about l2r in check_correct_arity (baaa28f )
Merge PR #13531: [kernel]Use ~l2r:true to restore previous order of unfolding (3eb730c )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
dune: Don't echo "$(pwd)" when creating the shims (81bc69d )
Merge PR #13526: dune: Don't echo "$(pwd)" when creating the shims (b39b559 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and pi8027 (1).
Backport ssrbool lemmas from MathComp 1.12.0 (86a3d1a )
Merge PR #13490: [ssr] Backport ssrbool from MathComp 1.12.0 (2eeeba7 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by gares (2) and coqbot-app[bot] (1).
[docker] install boost, mpfr, flex, bison, autoconf-archive (ee9e06d )
[ci] add job for gappa (c79677a )
Merge PR #13472: [ci] Add job for gappa (b3b4d64 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ppedrot (1).
Fix a bug in funind. (64de97e )
Merge PR #13543: Fix a bug in funind. (ff8155b )
gares pushed 7 commits to branch v8.13. Commits by gares (4), mattam82 (2) and SkySkimmer (1).
[kernel] Fix #13495: incompleteness in cases typing for cumulative inductive types (cd79c56 )
Backport PR #13501: [kernel] Fix #13495: incompleteness in cases typing for cumulative inductive types (297c2b3 )
Use ~l2r:true to restore previous order of unfolding when typing predicates of cases. (f9e917f )
Added comment about l2r in check_correct_arity (e5133d1 )
Backport PR #13531: [kernel]Use ~l2r:true to restore previous order of unfolding (687cb8e )
pin equations v1.2.3-8.13 (7a08884 )
pin bignums V8.13+beta1 (7e8cf3d )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
gitlab CI: remove redundant "dependencies" info (61a784a )
Merge PR #13471: gitlab CI: remove redundant "dependencies" info (ad8cf01 )
vbgl pushed 2 commits to branch master. Commits by proux01 (1) and vbgl (1).
Put all Int63 primitives in a separate file (853b838 )
Merge PR #13275: Put all Int63 primitives in a separate file (11730fa )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and jfehrle (1).
Split long lines in errors and warning index (af0276f )
Merge PR #13554: Split long lines in errors and warning index (a88568e )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ppedrot (1).
Move *_with_full_binders variants out of the kernel. (056245e )
Merge PR #13548: Move *_with_full_binders variants out of the kernel. (afbc39d )
coqbot-app[bot] pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot-app[bot] (1).
[refman] Fix error names. (6a3586d )
Merge PR #13558: [refman] Fix error names. (632b960 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and gares (1).
[coqide] fix procedure to parse arguments (065913e )
Merge PR #13546: [coqide] fix procedure to parse arguments (88f23b3 )
coqbot-app[bot] pushed 12 commits to branch master. Commits by mattam82 (9), gares (2) and coqbot-app[bot] (1).
Changes for Coq 8.13 (3c4d2c9 )
Add an anchor in syntax-extensions (2dbc0f2 )
[changelog] update markup (c8fc6b8 )
Apply suggestions from @jfehrle code review (554a3b1 )
Changes without PR references fixes (e9b3040 )
Fixes in the summary by Jim Fehrle (f23ccdd )
Update doc/sphinx/changes.rst (002ab0b )
Apply suggestions from code review (73eb97c )
Apply suggestions from code review (dba9b80 )
Implement suggestions by Théo Zimmermann (d6f4235 )
Implement review corrections by Théo Zimmermann (d20e4ed )
Merge PR #13527: Changes for Coq 8.13 (b01b5fc )
coqbot-app[bot] pushed 3 commits to branch master. Commits by gares (2) and coqbot-app[bot] (1).
[rm] update git commands to push tags (54abd3d )
[rm] clarify process for is_a_released_version = true (ca9b6c0 )
Merge PR #13497: [rm] update release notes (4830993 )
gares pushed 18 commits to branch v8.13. Commits by mattam82 (9), gares (7), Zimmi48 (1) and others (1).
Split long lines in errors and warning index (b7e9bae )
Backport PR #13554: Split long lines in errors and warning index (f334490 )
[refman] Fix error names. (3f627d2 )
Backport PR #13558: [refman] Fix error names. (ab34fdb )
[coqide] fix procedure to parse arguments (c83d89a )
Backport PR #13546: [coqide] fix procedure to parse arguments (9fff24e )
Changes for Coq 8.13 (75f70ba )
Add an anchor in syntax-extensions (b698b4e )
[changelog] update markup (bfac146 )
Apply suggestions from @jfehrle code review (d8d840e )
Changes without PR references fixes (0f85087 )
Fixes in the summary by Jim Fehrle (4010e3c )
Update doc/sphinx/changes.rst (c04cd8a )
Apply suggestions from code review (477a38f )
Apply suggestions from code review (b05f69c )
Implement suggestions by Théo Zimmermann (4f2a9db )
Implement review corrections by Théo Zimmermann (3332dc7 )
Backport PR #13527: Changes for Coq 8.13 (e974541 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Stop calling Id.Map.domain on univ binders every individual universe (ecb23dc )
Merge PR #13551: Stop calling Id.Map.domain on univ binders every individual universe (53d5b2d )
coqbot-app[bot] pushed 5 commits to branch master. Commits by ppedrot (4) and coqbot-app[bot] (1).
Store Ltac2 valexpr instead of unevaluated code inside Ltac1 value embedding. (b2d3d5f )
Add an abstraction function in the LtacX FFI. (bb97b0f )
Add test for this new function. (bf111ba )
Adding a changelog for Ltac1.lambda. (3ae0e24 )
Merge PR #13442: Add an abstraction function in the LtacX FFI. (4d21a08 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ybertot (1).
ppedrot pushed 3 commits to branch master. Commits by SkySkimmer (2) and ppedrot (1).
compute_instance_binders: use prebuilt reverse map (b399887 )
Delay inventing names for monomorphic universes (40f6ecf )
Merge PR #13552: Delay inventing names for monomorphic universes (157a6c1 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and proux01 (1).
Document Number Notation for primitive integers (fcfa007 )
Merge PR #13553: Document Number Notation for primitive integers (aa05724 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and gares (1).
[doc] update changes after 13501 (8e7b1ad )
Merge PR #13585: [RM] Update changes 13501 (d8ba0f8 )
gares pushed 18 commits to branch v8.13. Commits by gares (13), SkySkimmer (3), proux01 (1) and others (1).
[coq_makefile] honor environment for OCAMLFIND (9f5e14d )
[coq_makefile] use Envars for COQMF_WINDRIVE (bf7df23 )
[doc] coq_environment.txt (74924c8 )
[win] [envars] honor file "coq_environment.txt" (eba2e6a )
[test-suite] improve ocaml_pwd (34ccd54 )
[dune] [test-suite] pass BIN= as the regular makefile does (793fc13 )
Backport PR #13523: [envars] honor file "coq_environment.txt" (842bed6 )
Stop calling Id.Map.domain on univ binders every individual universe (bbcddb4 )
Backport PR #13551: Stop calling Id.Map.domain on univ binders every individual universe (0b58e3d )
compute_instance_binders: use prebuilt reverse map (d5b8456 )
Delay inventing names for monomorphic universes (3e99ae6 )
Backport PR #13552: Delay inventing names for monomorphic universes (04a4a57 )
typo (af86ebe )
Backport PR #13569: typo (403eafc )
Document Number Notation for primitive integers (d688bc2 )
Backport PR #13553: Document Number Notation for primitive integers (cee89c8 )
[doc] update changes after 13501 (60d8b04 )
Backport PR #13585: [RM] Update changes 13501 (e619810 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and paldepind (1).
Fix spelling in warning entry (a996fb7 )
Merge PR #13556: Fix spelling in warning entry (bfd3dac )
gares pushed tag V8.13+beta1.
gares pushed 5 commits to branch v8.13.
[rm] bump version to 8.13+beta1 (516c497 )
[rm] this is a released version (18c7781 )
[osx] disable brew cleanup (564b8b3 )
Merge PR #13587: Tag 8.13 beta1 (5f7bf8d )
[rm] first commit after tag V8.13+beta1 (d7d132d )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and erikmd (1).
Add depopts:coq-native in coq.opam.docker (55f49d3 )
Merge PR #13588: Add depopts: coq-native
in coq.opam.docker (0369080 )
mattam82 pushed 1 commit to branch fix-case-arity-typing.
Improve type-checking of case predicates (a5ce898 )
mattam82 deleted the branch fix-case-arity-typing.
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ppedrot (1).
Add a test for cbv over inductive types which feature let-bindings. (e5a5fdb )
Merge PR #13596: Add a test for cbv over inductive types which feature let-bindings. (c79e503 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ejgallego (1).
[dune] [opam] Disable dune subst in opam files until the upstream fix is propagated (92ea613 )
Merge PR #13572: [dune] [opam] Disable dune subst in opam files until the upstream fix is propagated (eed93da )
coqbot-app[bot] pushed 3 commits to branch master. Commits by SkySkimmer (2) and coqbot-app[bot] (1).
Reindent Cctac.cc_tactic (bec752e )
Congruence: don't replace error messages by "congruence failed" (f4af5d4 )
Merge PR #13597: Congruence: don't replace error messages by "congruence failed" (6cac4e1 )
coqbot-app[bot] pushed 5 commits to branch master. Commits by gares (4) and coqbot-app[bot] (1).
[rm] update instructions for windows signing (9d878c3 )
[rm] manual is uploaded by CI (39b4eb9 )
Update dev/doc/release-process.md (5f11345 )
[rm] announcements to discourse (fc758c0 )
Merge PR #13591: [rm] update instructions for windows signing (9e0ca70 )
coqbot-app[bot] pushed 8 commits to branch master. Commits by ppedrot (7) and coqbot-app[bot] (1).
Cleanup substitution API. (d6f1694 )
More efficient implementation for substitutions. (de1beef )
Optimization: take advantage that we don't use arrays anymore in substitutions. (88f8f53 )
Compact representation of identity substitutions. (2064a5d )
Adding overlays. (afd653e )
Document Esubst API and implementation. (bb9486b )
Please the god of nitpicking by renaming the shift monoid operations. (e0a943d )
Merge PR #13537: More efficient implementation for substitutions. (4fbc04b )
cpitclaudel pushed 2 commits to branch master. Commits by cpitclaudel (1) and jfehrle (1).
Allow any character in a tacn, cmd, ... name (231bcf5 )
Merge PR #13564: Allow all characters in tacn, cmd, ... names. Report duplicate names. (cc9f22d )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and gares (1).
[osx] disable brew cleanup (d5ce3e8 )
Merge PR #13605: [osx] disable brew cleanup (358e923 )
Zimmi48 pushed 8 commits to branch v8.12. Commits by Zimmi48 (4), herbelin (2), CohenCyril (1) and others (1).
[osx] disable brew cleanup (6190b31 )
Pin metacoq to a proper tag. (176c040 )
Fixes #13432: regression with notations involving coercions caused by #11172. (33ccc0d )
Backport PR #13436: Fixes #13432: typo in #11172 causing notations mentioning a coercion not being used (ef1f5bb )
Testing {in _, _} and {pred _} from ssrbool (831c47d )
Backport PR #13473: Testing {in _, _} and {pred _} from ssrbool (eb6c0e9 )
Fixes #13456: regression where tactic exists started to check evars incrementally. (279e320 )
Backport PR #13468: Fixes #13456: regression in tactic exists which started to check resolution of evars more incrementally (eabaf95 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot-app[bot] (1).
Move Azure jobs to GitHub Actions. (b481ae1 )
Merge PR #13590: Move Azure jobs to GitHub Actions. (c3ba8ed )
coqbot-app[bot] pushed 14 commits to branch master. Commits by herbelin (13) and coqbot-app[bot] (1).
Constrintern: shortcut in cases pattern interning. (ae2c4b5 )
Constrintern: As in terms, accept @C for C abbreviation in cases patterns. (6e884b0 )
Removing a useless explicit use of subscopes in interpreting arguments of a notation. (0f43420 )
Move addition of parameters in asymmetric mode to first phase of pat interning. (a386c2f )
Adding functions to returning the def/decl status of an inductive arity. (3f286f3 )
Fixing support for argument scopes and let-ins while interning cases patterns. (c8c93bf )
Constrintern cleanup: Centralizing calls to find_appl_head. (df45fe3 )
Constrintern: Grouping together functions about reference locating. (ba1b332 )
Constrintern: Code factorization in interning of record fields. (da2ce98 )
Fixing some indentations in constrintern.ml . (0c243ac )
Some documentation in constrintern.ml . (eb7eed3 )
Constrintern.ml : some naming uniformity. (a33172c )
Using self-documenting argument names in two exceptions of cases.ml . (dc7a4f0 )
Merge PR #12100: Fixing use of argument scopes in patterns + a further cleanup of constrintern.ml (71031ef )
coqbot-app[bot] pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot-app[bot] (1).
Changelog for 8.12.2. (1e37c52 )
Merge PR #13608: Changelog for 8.12.2. (1918f19 )
Zimmi48 pushed 3 commits to branch v8.12.
Changelog for 8.12.2. (ea9af74 )
Bump version number to 8.12.2. (fb22a68 )
Merge PR #13607: [v8.12] 8.12.2 release (e64a5ad )
Zimmi48 pushed tag V8.12.2.
gares pushed 5 commits to branch v8.13. Commits by SkySkimmer (2), gares (2) and paldepind (1).
Reindent Cctac.cc_tactic (08af47e )
Fix spelling in warning entry (820f185 )
Congruence: don't replace error messages by "congruence failed" (b14b305 )
Backport PR #13556: Fix spelling in warning entry (b96c591 )
Backport PR #13597: Congruence: don't replace error messages by "congruence failed" (0d76fb4 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and shinnar (1).
Redefines exp_ineq1 to hold for all non-zero numbers. (29d2ffb )
Merge PR #13582: Generalize exp_ineq1 and add exp_ineq1_le, which holds forall Reals. (d40ef24 )
ppedrot pushed 5 commits to branch master. Commits by silene (4) and ppedrot (1).
Avoid compiler warnings. (33c4220 )
Make the code clearer and faster by calling mask63 explicitly at the end. (9ca7e76 )
Greatly simplify the conversion functions between Z.t and Uint63.t. (2422d7d )
Make sure the msb is clear. (f4dcd1d )
Merge PR #13540: Clean support of primitive integers (6ce1c1d )
cpitclaudel pushed 2 commits to branch master. Commits by Zimmi48 (1) and cpitclaudel (1).
Bump reference to 8.12 refman following unexpected 8.12.2 release. (9cb6d07 )
Merge PR #13612: Bump reference to 8.12 refman following unexpected 8.12.2 release. (edc599b )
cpitclaudel pushed 2 commits to branch master. Commits by Zimmi48 (1) and cpitclaudel (1).
Clarify changelog categories. (1605ae8 )
Merge PR #13611: Clarify changelog categories. (c8d2248 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and fakusb (1).
Better primitive type support in custom string and numeral notations. (0d1da88 )
Merge PR #13519: Better primitive type support in custom string and numeral notations. (5a77078 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and herbelin (1).
Removing non relevant argument binding_kind of GLocalDef. (f7004c5 )
Merge PR #13492: Removing non relevant argument binding_kind of GLocalDef. (fe72ccc )
gares pushed 13 commits to branch v8.13. Commits by gares (5), silene (4), Zimmi48 (3) and others (1).
Allow any character in a tacn, cmd, ... name (8c33055 )
Backport PR #13564: Allow all characters in tacn, cmd, ... names. Report duplicate names. (f077785 )
Changelog for 8.12.2. (be8156c )
Backport PR #13608: Changelog for 8.12.2. (51da571 )
Avoid compiler warnings. (595a3d4 )
Make the code clearer and faster by calling mask63 explicitly at the end. (acd0563 )
Greatly simplify the conversion functions between Z.t and Uint63.t. (d943e69 )
Make sure the msb is clear. (13b1211 )
Backport PR #13540: Clean support of primitive integers (8465bbb )
Bump reference to 8.12 refman following unexpected 8.12.2 release. (20c33b6 )
Backport PR #13612: Bump reference to 8.12 refman following unexpected 8.12.2 release. (5427eef )
Clarify changelog categories. (c6eab77 )
Backport PR #13611: Clarify changelog categories. (7a1f6b2 )
coqbot-app[bot] pushed 5 commits to branch master. Commits by gares (4) and coqbot-app[bot] (1).
[ci] function to declare projects (84e87cf )
[ci] simplify overlay scripts (3f4d646 )
[ci] remove old overlays so that people don't copy them (28d2f8d )
[ci] update url of autosubst (050a09a )
Merge PR #13603: [ci] function to declare projects (233629e )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ppedrot (1).
Use a registered printer for tactic coercion failure. (7615b53 )
Merge PR #13620: Use a registered printer for tactic coercion failure. (81d0936 )
gares pushed 1 commit to branch v8.13.
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and cpitclaudel (1).
doc: Clarify the status of simpl vs cbn (b668248 )
Merge PR #13619: doc: Clarify the status of simpl vs cbn (a819eee )
ppedrot pushed 4 commits to branch master. Commits by herbelin (3) and ppedrot (1).
Removing flag "Bracketing Last Introduction Pattern". (1b43dfc )
Removing unused internal introduction-patterns flag assert_style. (79518cc )
Add changelog for #13509. (5ff1626 )
Merge PR #13509: Remove compatibility flag Set Bracketing Last Introduction Pattern (2648803 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and gares (1).
[changes] mark #12765 as experimental (92204c4 )
Merge PR #13613: [changes] mark #12765 as experimental (d0667eb )
coqbot-app[bot] pushed 3 commits to branch master. Commits by gares (2) and coqbot-app[bot] (1).
[ci] update doc for overlays (b927bb3 )
Update dev/ci/user-overlays/README.md (1c667f5 )
Merge PR #13626: [ci] update doc for overlays (d5ca91c )
ppedrot pushed 7 commits to branch master. Commits by gares (6) and ppedrot (1).
[coq_makefile] honor environment for OCAMLFIND (f720f0d )
[coq_makefile] use Envars for COQMF_WINDRIVE (4c4715b )
[doc] coq_environment.txt (1b39124 )
[win] [envars] honor file "coq_environment.txt" (823a5a0 )
[test-suite] improve ocaml_pwd (957fba5 )
[dune] [test-suite] pass BIN= as the regular makefile does (9fb840f )
Merge PR #13523: [envars] honor file "coq_environment.txt" (8fc6494 )
coqbot-app[bot] pushed 3 commits to branch master. Commits by ppedrot (2) and coqbot-app[bot] (1).
Remove most of Reductionops.*_state functions. (78a0d0a )
Do not rely on Reductionops to recognize canonical projections. (d3d4bb6 )
Merge PR #13630: Cleanup reductionops (6c35e25 )
coqbot-app[bot] pushed 4 commits to branch master. Commits by gares (3) and coqbot-app[bot] (1).
[ci] fix code to check if the overlay is valid (c95058a )
[ci] simplify script to pin ci projects (8817a18 )
Update dev/tools/pin-ci.sh (477cba2 )
Merge PR #13632: [ci] Update pin ci script (46c55ce )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ppedrot (1).
Fast path in tclPROGRESS. (cade097 )
Merge PR #13621: Fast path in tclPROGRESS. (f78f812 )
coqbot-app[bot] pushed 5 commits to branch master. Commits by ppedrot (4) and coqbot-app[bot] (1).
Generalize the type of red_expr w.r.t. the type of flags they contain. (b7ec355 )
Split the intepretation of red_exprs in two phases. (35ead41 )
Extrude the computation of redexp flags in reduce. (12d53dc )
Small API encapsulation inside Redexpr. (421ed6b )
Merge PR #13609: Extrude the computation of redexp flags in reduce. (c605832 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and gares (1).
[ci] uniform name of projects w.r.t. opam packages (806ac6f )
Merge PR #13633: [ci] uniform name of projects w.r.t. opam packages (83d225f )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ppedrot (1).
Tweak constr_matching so as to make it tail-rec on projection expansion. (213f84e )
Merge PR #13625: Tweak constr_matching so as to make it tail-rec on projection expansion. (0e29b59 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot-app[bot] (1).
Document the manual tasks that I need to do at each release. (1173e09 )
Merge PR #13615: Document the manual tasks that I need to do at each release. (1c400a1 )
ppedrot pushed 2 commits to branch master. Commits by SkySkimmer (1) and ppedrot (1).
Bench: add .log extension to .stdout/stderr files (b98d434 )
Merge PR #13616: Bench: add .log extension to .stdout/stderr files (7c183ac )
ppedrot pushed 3 commits to branch master. Commits by herbelin (2) and ppedrot (1).
Add checks for invalid occurrences in setoid rewrite. (e3968a2 )
Adding change log for #13568. (f3e05c1 )
Merge PR #13568: Fix #13566: Add checks for invalid occurrences in several tactics. (88c77bf )
coqbot-app[bot] pushed 2 commits to branch master. Commits by SkySkimmer (1) and coqbot-app[bot] (1).
Fix overlay system: projects need to be loaded before overlays. (faafe8b )
Merge PR #13644: Fix overlay system: projects need to be loaded before overlays. (41cf9c1 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by LasseBlaauwbroek (1) and coqbot-app[bot] (1).
Add -q flag to coqrst python invocation of coqtop (4081777 )
Merge PR #13643: Add -q flag to coqrst python invocation of coqtop (70ea750 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and ppedrot (1).
Add a test for change over case nodes. (2ecba80 )
Merge PR #13652: Add a test for change over case nodes. (8013852 )
gares pushed 7 commits to branch v8.13. Commits by gares (6) and cpitclaudel (1).
pin bugnums V8.13.0 (9c4a390 )
pin aac-tactics v8.13.0 (c20016c )
pin HB v1.0.0 (efcde91 )
[changes] mark #12765 as experimental (8abcb23 )
Backport PR #13613: [changes] mark #12765 as experimental (bfd6dbe )
doc: Clarify the status of simpl vs cbn (f0ede76 )
Backport PR #13619: doc: Clarify the status of simpl vs cbn (14e0b15 )
coqbot-app[bot] pushed 5 commits to branch master. Commits by ppedrot (4) and coqbot-app[bot] (1).
Cache meta access in meta_instance. (981146b )
Make the clenv type private and provide a creation function. (161b7b4 )
Store the metasubst cache in clenvs. (bc9a22f )
Reuse the cache everywhere possible in Clenv. (7a8761b )
Merge PR #13628: Cache meta instances in Clenv (82d0a57 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and jfehrle (1).
Revert removal of eoi_entry in #13447 (5510629 )
Merge PR #13530: Revert removal of eoi_entry in #13447 (687fff6 )
coqbot-app[bot] pushed 8 commits to branch master. Commits by herbelin (7) and coqbot-app[bot] (1).
Deduce Stack.decomp from Stack.strip_n_app. (35ff578 )
Unification: documenting eta for pi-types and record types. (a20d731 )
Documenting module Reductionops.Stack. (82fffac )
Short documentation of solve_simple_eqn. (e9da1fe )
Some partial documentation of evar_conv_x. (dc5a992 )
Unification: renamings in ise_stack2 to get a more explicit idea of its semantic. (3e78772 )
More documentation about the situation ?ev := C[?ev'] in solve_simple_eqn. (c213d57 )
Merge PR #13138: Towards a documentation / cleanup of evarconv (9d596d1 )
gares pushed 2 commits to branch v8.13. Commits by LasseBlaauwbroek (1) and gares (1).
Add -q flag to coqrst python invocation of coqtop (dc4048c )
Backport PR #13643: Add -q flag to coqrst python invocation of coqtop (a0e4b1d )
coqbot-app[bot] pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot-app[bot] (1).
Shorten/improve intro of "Basic proof writing" chapter. (9c31858 )
Merge PR #13651: Shorten/improve intro of "Basic proof writing" chapter. (7b8f73e )
coqbot-app[bot] pushed 19 commits to branch master. Commits by jashug (18) and coqbot-app[bot] (1).
Catch up to where I was last time. (03ebf86 )
Modify QArith/QArith_base.v to compile with -mangle-names (063aa71 )
Modify setoid_ring/Field_theory.v to compile with -mangle-names (96ad23e )
Modify QArith/Qreduction.v to compile with -mangle-names (b987bce )
Modify micromega/ZMicromega.v to compile with -mangle-names (6076823 )
Modify ZArith/Zpower.v to compile with -mangle-names (84da55b )
Modify ZArith/Zpow_facts.v to compile with -mangle-names (ecc7f59 )
Modify ZArith/Zgcd_alt.v to compile with -mangle-names (25b41bb )
Modify Numbers/Cyclic/Int63/Int63.v to compile with -mangle-names (0f8d574 )
Modify Bool/BoolEq.v to compile with -mangle-names (4c4fb14 )
Modify Bool/DecBool.v to compile with -mangle-names (303b167 )
Modify Bool/IfProp.v to compile with -mangle-names (7f6883f )
Modify Bool/Zerob.v to compile with -mangle-names (051f55b )
Modify Classes/CEquivalence.v to compile with -mangle-names (511a81a )
Modify Classes/DecidableClass.v to compile with -mangle-names (29c8814 )
Modify Logic/FunctionalExtensionality.v to compile with -mangle-names (c53cd87 )
Modify Program/Wf.v to compile with -mangle-names (cd3d7e1 )
Modify Logic/JMeq.v to compile with -mangle-names (ef7dbd8 )
Merge PR #13649: Lint stdlib with -mangle-names #5 (532cbed )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and jfehrle (1).
Clean ALL sphinx output files (09a2bec )
Merge PR #13673: Clean ALL sphinx output files (015310b )
coqbot-app[bot] pushed 3 commits to branch master. Commits by Zimmi48 (2) and coqbot-app[bot] (1).
[ci/gitlab/windows] Bump OCaml to 4.10.2 to fix Windows CI. (e11d3f6 )
Do not load overlay data (workaround to fix CI). (c99cf10 )
Merge PR #13650: [ci/gitlab/windows] Bump OCaml to 4.10.2 to fix Windows CI. (61089d8 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by MSoegtropIMC (1) and coqbot-app[bot] (1).
CoqIDE: Fix CC reference in makefile (ced3425 )
Merge PR #13677: CoqIDE: Fix CC reference in makefile (bcb2f47 )
coqbot-app[bot] pushed 4 commits to branch master. Commits by LasseBlaauwbroek (3) and coqbot-app[bot] (1).
Make ssr datastructures cpattern and rpattern public (a84ff98 )
Make ssrtermkind algebraic instead of a char (d1af000 )
Refactor cpattern into a record (857f840 )
Merge PR #13659: Make ssr datastructures cpattern and rpattern public (52154bf )
gares pushed 2 commits to branch v8.13. Commits by gares (1) and proux01 (1).
[CI] Update paramcoq branch to v8.13 (15e16b5 )
Merge PR #13679: [v8.13] [CI] Update paramcoq branch to v8.13 (af98399 )
gares pushed 1 commit to branch v8.13.
Revert "[CI] Update paramcoq branch to v8.13" (f43711e )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and herbelin (1).
Fixes #13657: vscoq needs goal uid. (74ccd94 )
Merge PR #13662: Fixes #13657: vscoq needs goal uid. (ba0a277 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and jfehrle (1).
Set the locale in Docker so Python's default output encoding is utf-8 (6e2b31a )
Merge PR #13665: Set Python's default output encoding to utf-8 (942fb01 )
gares pushed 5 commits to branch v8.13. Commits by gares (3), Zimmi48 (1) and herbelin (1).
Shorten/improve intro of "Basic proof writing" chapter. (31cdc7f )
pin MC, 4CT, OO and paramcoq (18fca01 )
update autosubst url (6557755 )
Fixes #13657: vscoq needs goal uid. (4dce091 )
Backport PR #13662: Fixes #13657: vscoq needs goal uid. (fcd318e )
coqbot-app[bot] pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot-app[bot] (1).
[refman] Clarify meaning of goal in documentation of instantiate. (627dcd7 )
Merge PR #13686: [refman] Clarify meaning of goal in documentation of instantiate. (810e915 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and proux01 (1).
Document the -native-compiler option (8a0986f )
Merge PR #13684: Document the -native-compiler option (30f648d )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and silene (1).
Fix broken HTML rendering of inference rules (fix #12783). (aed648a )
Merge PR #13682: Fix broken HTML rendering of inference rules (fix #12783). (d338a65 )
coqbot-app[bot] pushed 4 commits to branch master. Commits by ppedrot (3) and coqbot-app[bot] (1).
Remove the artificial dependency of Heads on evaluable_global_reference. (a714abe )
Move evaluable_global_reference from Names to Tacred. (63332cb )
Add overlays. (1be5dcc )
Merge PR #13321: Move evaluable_global_reference from Names to Tacred. (d633121 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot-app[bot] (1).
Fix failing Windows CI builds. (83bce17 )
Merge PR #13692: Fix failing Windows CI builds. (039f04c )
gares pushed 4 commits to branch v8.13. Commits by gares (2), Zimmi48 (1) and proux01 (1).
[refman] Clarify meaning of goal in documentation of instantiate. (97360c4 )
Backport PR #13686: [refman] Clarify meaning of goal in documentation of instantiate. (3f72687 )
Document the -native-compiler option (bc733f8 )
Backport PR #13684: Document the -native-compiler option (4d9394a )
coqbot-app[bot] pushed 2 commits to branch master. Commits by Zimmi48 (1) and coqbot-app[bot] (1).
[ci] Switch to testing the maintenance branch for Flocq 3. (f4fb8a1 )
Merge PR #13693: [ci] Switch to testing the maintenance branch for Flocq 3. (6e18c48 )
coqbot-app[bot] pushed 2 commits to branch master. Commits by coqbot-app[bot] (1) and jfehrle (1).
Convert rewriting and proof-mode chapters to prodn (e02120e )
Merge PR #13470: Convert rewriting and proof-mode chapters to prodn (66e24a2 )
gares pushed 2 commits to branch v8.13. Commits by gares (1) and jfehrle (1).
Convert rewriting and proof-mode chapters to prodn (5c4abd8 )
Backport PR #13470: Convert rewriting and proof-mode chapters to prodn (b8f1f11 )
Coq Github Bot