aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-03-08Relax conversion of constructors according to the pCuIC modelMatthieu Sozeau
- Nothing to check in conversion as they have a common supertype by typing. - In inference, enforce that one is lower than the other.
2018-03-08Merge PR #6743: Add notation {x & P} for sigTMaxime Dénès
2018-03-08Merge PR #6927: Add some missing flushes in configure.Maxime Dénès
2018-03-08Merge PR #6909: Deprecate Focus and UnfocusMaxime Dénès
2018-03-08Merge PR #6899: [compat] Remove "Standard Proposition Elimination"Maxime Dénès
2018-03-08Merge PR #6881: [windows] support -addon in build scriptMaxime Dénès
2018-03-08Merge PR #6582: Mangle auto-generated namesMaxime Dénès
2018-03-08Merge PR #6933: Standard headers for C and Python.Maxime Dénès
2018-03-08Merge PR #6934: Warn when using “Require” in a sectionMaxime Dénès
2018-03-08Merge PR #6924: Clean-up remove always false useeager argument.Maxime Dénès
2018-03-08Merge PR #6902: [compat] Remove "Discriminate Introduction"Maxime Dénès
2018-03-08Merge PR #6903: [compat] Remove "Shrink Abstract"Maxime Dénès
2018-03-08Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Maxime Dénès
2018-03-07[toplevel] Respect COQ_COLORS environment variableThomas Hebb
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).
2018-03-07gitlab: install num for all jobsGaëtan Gilbert
Previously it was installed for the compilation jobs causing random failures when the other jobs got a cache without it.
2018-03-07[checker] Printer cleanup.Emilio Jesus Gallego Arias
Makes printing rules more explicit and should close #6799.
2018-03-07Use a proper warning when a summary is captured out of module scope.Vincent Laporte
2018-03-07[vernac] Warn when using “Require” in a sectionVincent Laporte
2018-03-07[stdlib] Do not use “Require” inside sectionsVincent Laporte
2018-03-07Add empty compat file for Coq 8.8Jason Gross
This closes #6598
2018-03-07Merge PR #6744: Add String.concatMaxime Dénès
2018-03-07Merge PR #6932: [stdlib] Do not use deprecated notationsMaxime Dénès
2018-03-07Merge PR #6905: Fix make ml-docMaxime Dénès
2018-03-07Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`Maxime Dénès
2018-03-07Merge PR #6922: Remove outdated information regarding the FAQ.Maxime Dénès
2018-03-07Merge PR #6374: [toplevel] Modify printing goal strategy.Maxime Dénès
2018-03-07Merge PR #6790: Allow universe declarations for [with Definition].Maxime Dénès
2018-03-07Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...)Maxime Dénès
2018-03-06Add CHANGES and man entry for coqdep learning _CoqProject.Gaëtan Gilbert
2018-03-06Closes #6830: coqdep reads options and files from _CoqProject.Gaëtan Gilbert
Note that we don't look inside -arg for eg -coqlib.
2018-03-06An experimental 'Show Extraction' command (grant feature wish #4129)Pierre Letouzey
Attempt to extract the current ongoing proof (request by Clément Pit-Claudel on coqdev, and also #4129). Evars are handled as axioms.
2018-03-06Extraction: switch to EConstr.t as the central type to extract from.Pierre Letouzey
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 )
2018-03-06romega: get rid of EConstr.UnsafePierre Letouzey
We replace constr by EConstr.t everywhere, and propagate some extra sigma args
2018-03-06document -profile in dev/doc/setup.txtEnrico Tassi
2018-03-06Standard headers for C and Python.Maxime Dénès
2018-03-06[stdlib] Do not use deprecated notationsVincent Laporte
2018-03-06Add some missing flushes in configure.Maxime Dénès
Some messages were sometimes not printed because of the missing flushes. We use a generic combinator suggested by Emilio.
2018-03-06Hack to make bignum build on windowsEnrico Tassi
2018-03-06build: win: turn off build/installation of gnu MakeEnrico Tassi
2018-03-06Clean-up remove always false useeager argument.Théo Zimmermann
2018-03-06Remove outdated information regarding the FAQ.Théo Zimmermann
The FAQ is not part of the Coq sources anymore.
2018-03-06Rename some universe minimizing "normalize" functions to "minimize"Gaëtan Gilbert
UState normalize -> minimize, Evd nf_constraints -> minimize_universes
2018-03-06Deprecate UState aliases in Evd.Gaëtan Gilbert
2018-03-06Merge PR #6917: Fix failing packaging job.Maxime Dénès
2018-03-06[compat] Remove "Discriminate Introduction"Emilio Jesus Gallego Arias
Following up on #6791, we the option "Discriminate Introduction".
2018-03-06[compat] Remove "Shrink Abstract"Emilio Jesus Gallego Arias
Following up on #6791, we the option "Shrink Abstract".
2018-03-06Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ↵Maxime Dénès
a record.
2018-03-06Merge PR #6795: [ssreflect] Export parsing witnesses in mli file.Maxime Dénès
2018-03-06ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Enrico Tassi
2018-03-06Merge PR #6896: [compat] Remove NOOP deprecated options.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-28 08:11:35 +0000