aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* | | | | | | | | | | | | | | | | | Merge PR #6743: Add notation {x & P} for sigTGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6927: Add some missing flushes in configure.Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6909: Deprecate Focus and UnfocusGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6899: [compat] Remove "Standard Proposition Elimination"Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6881: [windows] support -addon in build scriptGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | | | | Merge PR #6582: Mangle auto-generated namesGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6933: Standard headers for C and Python.Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6934: Warn when using “Require” in a sectionGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | | | | | | Merge PR #6924: Clean-up remove always false useeager argument.Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6902: [compat] Remove "Discriminate Introduction"Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6903: [compat] Remove "Shrink Abstract"Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | | | | | | | | | | * | [toplevel] Respect COQ_COLORS environment variableGravatar Thomas Hebb2018-03-07
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since 3fc02bb2034a ("[pp] Move terminal-specific tagging to the toplevel."), the COQ_COLORS environment variable has been ignored, since init_terminal_output unconditionally called init_tag_map with the default colors, overwriting any custom colors that had been previously set. Fix this by creating a separate function, default_styles, to set the default colors. Also, remove the clear_styles function, as it was only called in one place and did nothing (since tag_map is empty to begin with).
| | | | | | | | | | | | | | | | | * | | | | | | | | | gitlab: install num for all jobsGravatar Gaëtan Gilbert2018-03-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously it was installed for the compilation jobs causing random failures when the other jobs got a cache without it.
| | | | | | | | | | | | | | | | | | | | | | | * | | | [checker] Printer cleanup.Gravatar Emilio Jesus Gallego Arias2018-03-07
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Makes printing rules more explicit and should close #6799.
| | | | | * | | | | | | | | | | | | | | | | | | | | Use a proper warning when a summary is captured out of module scope.Gravatar Vincent Laporte2018-03-07
| | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | * | | | | | | | | | | | | | | | | | | | | [vernac] Warn when using “Require” in a sectionGravatar Vincent Laporte2018-03-07
| | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | * | | | | | | | | | | | | | | | | | | | | [stdlib] Do not use “Require” inside sectionsGravatar Vincent Laporte2018-03-07
| |_|_|_|/ / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | * | | | | Add empty compat file for Coq 8.8Gravatar Jason Gross2018-03-07
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This closes #6598
* | | | | | | | | | | | | | | | | | | | | | | | Merge PR #6744: Add String.concatGravatar Maxime Dénès2018-03-07
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6932: [stdlib] Do not use deprecated notationsGravatar Maxime Dénès2018-03-07
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6905: Fix make ml-docGravatar Maxime Dénès2018-03-07
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`Gravatar Maxime Dénès2018-03-07
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6922: Remove outdated information regarding the FAQ.Gravatar Maxime Dénès2018-03-07
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6374: [toplevel] Modify printing goal strategy.Gravatar Maxime Dénès2018-03-07
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6790: Allow universe declarations for [with Definition].Gravatar Maxime Dénès2018-03-07
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...)Gravatar Maxime Dénès2018-03-07
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | * | | | | Add CHANGES and man entry for coqdep learning _CoqProject.Gravatar Gaëtan Gilbert2018-03-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | * | | | | Closes #6830: coqdep reads options and files from _CoqProject.Gravatar Gaëtan Gilbert2018-03-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Note that we don't look inside -arg for eg -coqlib.
| | | | | | | | | | | | | | | | | | | | | | | * | | | | | | | An experimental 'Show Extraction' command (grant feature wish #4129)Gravatar Pierre Letouzey2018-03-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Attempt to extract the current ongoing proof (request by Clément Pit-Claudel on coqdev, and also #4129). Evars are handled as axioms.
| | | | | | | | | | | | | | | | | | | | | | | * | | | | | | | Extraction: switch to EConstr.t as the central type to extract from.Gravatar Pierre Letouzey2018-03-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a bit artificial since the extraction normally operates on finished constrs (with no evars). But: - Since we use Retyping quite a lot, switching to EConstr.t allows to get rid of many `EConstr.Unsafe.to_constr (... (EConstr.of_constr ...))` - This prepares the way for a possible extraction of the content of ongoing proofs (a forthcoming `Show Extraction` command, see #4129 )
| | | | | | | | | | | | | | | | | | | | | * | | | | | | | | | romega: get rid of EConstr.UnsafeGravatar Pierre Letouzey2018-03-06
| | | | | | | | | | | | | | | | | | | | | | |/ / / / / / / / | | | | | | | | | | | | | | | | | | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We replace constr by EConstr.t everywhere, and propagate some extra sigma args
| | | | | | | | | | | | | | | | | | | | * | | | | | | | | | document -profile in dev/doc/setup.txtGravatar Enrico Tassi2018-03-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | | | | | | | | | | | | | | | | Standard headers for C and Python.Gravatar Maxime Dénès2018-03-06
| |_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | * | | | | | | | | | | | | | | | | | | | | | [stdlib] Do not use deprecated notationsGravatar Vincent Laporte2018-03-06
| |_|_|_|_|_|/ / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | * | | | | | | | | | | | Add some missing flushes in configure.Gravatar Maxime Dénès2018-03-06
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Some messages were sometimes not printed because of the missing flushes. We use a generic combinator suggested by Emilio.
| | | | | | | | | | | | | * | | | | | | | | | | | | | Hack to make bignum build on windowsGravatar Enrico Tassi2018-03-06
| | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | | | | | | | | | | | | | build: win: turn off build/installation of gnu MakeGravatar Enrico Tassi2018-03-06
| | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | * | | | | | | | | | | | | | | | Clean-up remove always false useeager argument.Gravatar Théo Zimmermann2018-03-06
| |_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | * | | | | | | | | | | | | | | | | | | | | | Remove outdated information regarding the FAQ.Gravatar Théo Zimmermann2018-03-06
| |_|_|/ / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The FAQ is not part of the Coq sources anymore.
| | | | | | | | | | | | | | | | | * | | | | | | | Rename some universe minimizing "normalize" functions to "minimize"Gravatar Gaëtan Gilbert2018-03-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | UState normalize -> minimize, Evd nf_constraints -> minimize_universes
| | | | | | | | | | | | | | | | | * | | | | | | | Deprecate UState aliases in Evd.Gravatar Gaëtan Gilbert2018-03-06
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | | | | | | Merge PR #6917: Fix failing packaging job.Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | * | | | | | | | | | | | | | | [compat] Remove "Discriminate Introduction"Gravatar Emilio Jesus Gallego Arias2018-03-06
| |_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Following up on #6791, we the option "Discriminate Introduction".
| | | | | | | | | * | | | | | | | | | | | | | | [compat] Remove "Shrink Abstract"Gravatar Emilio Jesus Gallego Arias2018-03-06
| |_|_|_|_|_|_|_|/ / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Following up on #6791, we the option "Shrink Abstract".
* | | | | | | | | | | | | | | | | | | | | | | Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ↵Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | a record.
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6795: [ssreflect] Export parsing witnesses in mli file.Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | * | | | | | | | | | | | | | | ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Gravatar Enrico Tassi2018-03-06
| | | | | | | | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #6896: [compat] Remove NOOP deprecated options.Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6824: Remove deprecated options related to typeclasses.Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 23:55:20 +0000