aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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-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
2021-01-28Document how rewrite works regarding occurrence selection.Théo Zimmermann
2021-01-27Merge PR #13418: [sysinit] new componentcoqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: JasonGross
2021-01-27Typo in commentGaëtan Gilbert
Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>
2021-01-27Add sysinit to load_printer listsGaëtan Gilbert
2021-01-27make the linter happyEnrico Tassi
2021-01-27[coqargs] use standard option injection for -print-emacsEnrico Tassi
2021-01-27[coqargs] use standard option injection for -type-in-typeEnrico Tassi
2021-01-27[coqargs] use standard option injection for -mangle-namesEnrico Tassi
2021-01-27[coqtop] handle -print-module-uid after initializationEnrico Tassi
2021-01-27[coqc] move -output-context from sysinit/coqargs to coqc properEnrico Tassi
2021-01-27[sysinit] move initialization code from coqtop to hereEnrico Tassi
We also spill (some) non-generic arguments and initialization code out of coqargs and to coqtop, namely colors for the terminal. There are more of these, left to later commits.
2021-01-27[sysinit] new component for system initializationEnrico Tassi
This component holds the code for initializing Coq: - parsing arguments not specific to the toplevel - initializing all components from vernac downwards (no stm) This commit moves stm specific arguments parsing to stm/stmargs.ml
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:35:11 +0000