aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-02-11Merge PR #13844: [vernac] pass the loc of the whole command to the interp ↵coqbot-app[bot]
function Reviewed-by: ejgallego
2021-02-11[ci] overlay for elpiEnrico Tassi
2021-02-11Merge PR #13640: Add ounit2 to with-test dependenciescoqbot-app[bot]
Reviewed-by: ejgallego
2021-02-11Merge PR #13642: Add build dependency of conf-python-3 to coq-doccoqbot-app[bot]
Reviewed-by: ejgallego
2021-02-11Merge PR #13823: Update release process following coq/ceps#52.coqbot-app[bot]
Reviewed-by: ejgallego Ack-by: gares
2021-02-11Merge PR #13831: Properly document the local and global locality attributes.coqbot-app[bot]
Reviewed-by: gares Reviewed-by: jfehrle Ack-by: SkySkimmer
2021-02-11[vernac] pass the loc of the whole command to the interp functionEnrico Tassi
2021-02-11Merge PR #13847: [ci] elpi 1.13.0coqbot-app[bot]
Reviewed-by: SkySkimmer
2021-02-11overlay for coq-elpiEnrico Tassi
2021-02-11[ci] elpi 1.13.0Enrico Tassi
2021-02-11Merge PR #13826: [micromega] Fixes #13794Vincent Laporte
Reviewed-by: vbgl
2021-02-10Merge PR #13818: [bench] Re-enable coq-performance-testscoqbot-app[bot]
Reviewed-by: SkySkimmer
2021-02-10Merge PR #13821: Properly handle ordering of -w and -native-compilercoqbot-app[bot]
Reviewed-by: gares
2021-02-10[micromega/nia] Improve sharing of proofsBESSON Frederic
Closes #13794
2021-02-09Merge PR #13822: Remove deprecated command line argumentscoqbot-app[bot]
Reviewed-by: gares
2021-02-09Merge PR #13810: ide: shift+enter to find backwardscoqbot-app[bot]
Reviewed-by: herbelin
2021-02-08Properly document the local and global locality attributes.Théo Zimmermann
2021-02-06Merge PR #13829: Fix hierarchy of sections in module chapter.coqbot-app[bot]
Reviewed-by: jfehrle
2021-02-05Fix hierarchy of sections in module chapter.Théo Zimmermann
2021-02-04Update release process following coq/ceps#52.Théo Zimmermann
2021-02-04Changelog for #13822Gaëtan Gilbert
2021-02-04Remove deprecated -inputstate command line argumentGaëtan Gilbert
Deprecated since 6dd9e003c289a79b0656e7c6f2cc59935997370c (2014)
2021-02-04Remove deprecated -sprop-cumulative command line argumentGaëtan Gilbert
Deprecated since #12034 (8.12)
2021-02-04Merge PR #13731: vernac/declaremods: make object collection tail-recursivecoqbot-app[bot]
Reviewed-by: SkySkimmer
2021-02-04Properly handle ordering of -w and -native-compilerGaëtan Gilbert
Warnings are handled as injection commands, interleaved with options and requires. Native compiler impacts require, so we must convert "yes" to "no" before handling injections. As such the semantic handling of the native command line argument must be separated from the emission of the warning message, which this PR implements. Fix #13819 In principle the other 2 cwarning in coqargs (deprecated spropcumul and inputstate) should be moved to injections too, but since they're deprecated I can't be bothered.
2021-02-04Merge PR #13528: [RM] Script to list the contributors between two git revisionscoqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: gares
2021-02-04Use release branch instead of master.Théo Zimmermann
2021-02-03Merge PR #13817: CI: Switch coqhammer job to edge ocamlcoqbot-app[bot]
Reviewed-by: Zimmi48
2021-02-03Merge PR #13776: Fix #13739 - disable some warnings when calling Function.coqbot-app[bot]
Reviewed-by: gares Ack-by: Zimmi48 Ack-by: SkySkimmer
2021-02-03Fix #13739 - disable some warnings when calling Function.Pierre Courtieu
Also added a generic way of temporarily disabling a warning. Also added try_finalize un lib/utils.ml.
2021-02-03[bench] Re-enable coq-performance-testsJason Gross
Partial revert of 6f4c61d152ad801bd571088ab99eb276b0085a04. coq-performance-tests was fixed in https://github.com/coq-community/coq-performance-tests/commit/ae8385b9471409387d0f47f01e38b866ba70bda1. Note that the current state is not optimal, as the bench does not test the native compiler at all (see #13807).
2021-02-03CI: Switch coqhammer job to edge ocamlGaëtan Gilbert
This fixes CI from their using the Stdlib module.
2021-02-02Merge PR #13814: Add VST to the set of default bench packages.coqbot-app[bot]
Reviewed-by: SkySkimmer
2021-02-02Add VST to the set of default bench packages.Pierre-Marie Pédrot
2021-02-02Merge PR #13805: Bench: remove broken packagesPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-02-02Merge PR #13791: Bench: don't uselessly rely on initialized opamPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-02-02ide: lablgtk fixesslrnsc
2021-02-02Bench: don't uselessly rely on initialized opamGaëtan Gilbert
AFAICT this init.sh call is useless.
2021-02-01Add changelog entryslrnsc
2021-02-01ide: shift+enter to find backwardsslrnsc
2021-01-29Bench: remove broken packagesGaëtan Gilbert
performance-tests and sf-plf have been failing for a long time without updates, there's no point wasting time partally building them.
2021-01-28Merge PR #13799: Replace : term with : type in open binders.coqbot-app[bot]
Reviewed-by: jfehrle
2021-01-28Merge PR #13789: Document limitation of rewrite regarding occurrence selection.coqbot-app[bot]
Reviewed-by: jfehrle Reviewed-by: silene
2021-01-28Update doc/sphinx/proofs/writing-proofs/rewriting.rstJim Fehrle
2021-01-28Merge PR #13781: [micromega] Deprecate hopefully useless options and flagscoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: jfehrle
2021-01-28Replace : term with : type in open binders.Théo Zimmermann
And update the doc_grammar files.
2021-01-28Apply suggestions from code reviewThéo Zimmermann
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2021-01-28vernac/declaremods: make object collection tail-recursiveGabriel Scherer
This patch is trying to upstream a jsCoq patch that was written to solve Stack Overflow issues: https://github.com/jscoq/jscoq/blob/v8.12/etc/patches/cps.patch It turns List.fold_right in vernac/declaremods into List.fold_left on a reversed lit.
2021-01-28Merge PR #13763: Remove the SearchHead command (deprecated in 8.12)coqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2021-01-28Merge PR #13790: [vernac] Check that no proofs do remain open at ↵coqbot-app[bot]
section/module closing time Reviewed-by: SkySkimmer
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 10:15:19 +0000