aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-01-03[tools] Remove support for python2Emilio Jesus Gallego Arias
Closes #10491 We re-add the header in doc/tools/coqrst/notations/fontsupport.py which was removed by accident in 1a9c769ed363ee2f2784e7252af72e6c1e2fbcc6 The fontsupport script itself has been kept for reference, however it is not involved by any build target as of today.
2020-01-02Merge PR #11335: Stdlib : Arith/Wf_nat : Add statements with output in TypeHugo Herbelin
Reviewed-by: herbelin
2019-12-31Merge PR #11338: Remove uses of Global in Evd API.Gaëtan Gilbert
Reviewed-by: ejgallego Reviewed-by: herbelin
2019-12-31Merge PR #11325: [refman] Add missing s.Pierre-Marie Pédrot
Reviewed-by: jfehrle
2019-12-30Merge PR #11233: Fixes #11231: missing dependency in looking for default ↵Pierre-Marie Pédrot
clauses in pattern matching decompilation algorithm Ack-by: Zimmi48 Reviewed-by: ppedrot
2019-12-30Merge PR #11345: Remove :flag: that appears in the doc outputThéo Zimmermann
Reviewed-by: Zimmi48
2019-12-29Remove :flag: that appears in the outputJim Fehrle
2019-12-29[refman] Fix bad quoting practice leftover from Sphinx migration.Théo Zimmermann
2019-12-29Merge PR #11314: Convert productionlists in the Gallina chapter up to the ↵Théo Zimmermann
Vernacular section to prodns Reviewed-by: Zimmi48
2019-12-29Merge PR #11183: Enhance prodn in .rst doc files to support multiple ↵Théo Zimmermann
productions in a prodn Ack-by: Zimmi48 Ack-by: cpitclaudel
2019-12-29Merge PR #11334: Fixes a small bug exposing an _ANONYMOUS_REL in a ↵Pierre-Marie Pédrot
unification error message Reviewed-by: ppedrot
2019-12-29Merge PR #10977: Remove the incorrect extra space in Makefile.vofilesEnrico Tassi
Reviewed-by: gares
2019-12-28Prevent apostrophes and backticks from being stylized in latexJim Fehrle
2019-12-28Convert productionlists to prodnsJim Fehrle
2019-12-28Merge PR #11323: Fix mulc on 32-bit architecturesMichael Soegtrop
Reviewed-by: MSoegtropIMC
2019-12-28Merge PR #10747: Extend `Print Canonical Projections` with a search ↵Enrico Tassi
functionality Reviewed-by: CohenCyril Ack-by: SkySkimmer Reviewed-by: ejgallego
2019-12-28Update doc/sphinx/language/gallina-extensions.rstKazuhiko Sakaguchi
Co-Authored-By: Cyril Cohen <CohenCyril@users.noreply.github.com>
2019-12-28Extend `Print Canonical Projections` with a search functionalityKazuhiko Sakaguchi
The `Print Canonical Projections` command now can take constants and prints only the unification rules that involves or are synthesized from given constants.
2019-12-27Add critical-bugs entry, tests-suite file, and code comment.Guillaume Melquiond
2019-12-27Merge PR #11315: Ensure that a custom entry cannot be defined twice.Hugo Herbelin
Reviewed-by: herbelin Reviewed-by: maximedenes
2019-12-27docs: Update changes.rst w.r.t. ssrsetoid.v's simplificationErik Martin-Dorel
2019-12-27fix: Shorten ssrsetoid.vErik Martin-Dorel
* This patch is a quick fix that removes part of the features of coq/coq#10022, namely the ability to directly use setoid_rewrite with a (Under_rel)-tagged relation R. This just means we'll need to do an extra step [rewrite UnderE.] which was unnecessary with Coq 8.11+alpha. * This PR stays backward-compatible w.r.t. Coq 8.10 and also keeps the salient feature of coq/coq#10022 (generalize under & over to any Reflexive relation). * Related: coq-community/atbr#23
2019-12-26Merge PR #11288: [omega] Remove non-documented "omega with *"Théo Zimmermann
Reviewed-by: Zimmi48 Ack-by: maximedenes
2019-12-26Add non-utf8 timing testJason Gross
This should have been running already, but it was forgotten in #9872
2019-12-26Add rew dependent NotationsJason Gross
This way when users `Import EqNotations`, we get pretty-printing for equality `match` statements too.
2019-12-26Merge PR #11336: [ci] [gitlab] [bedrock] Build bedrock with 1 coreThéo Zimmermann
Reviewed-by: Zimmi48
2019-12-26Remove uses of Global in Evd API.Pierre-Marie Pédrot
Namely, Evd.evar_env and Evd.evar_filtered_env now take an additional environment instead of querying the imperative global one. We percolate this change as higher up as possible.
2019-12-26[omega] Remove non-documented "omega with *"Emilio Jesus Gallego Arias
This form is only used in coq-bignums and not documented. I think removal is the best choice, specially as `zify` is not part of the omega plugin anymore.
2019-12-26Deprecate the "omega with *" syntax.Pierre-Marie Pédrot
Changes to the test-suite were backported from PR #11288.
2019-12-25Show doc notations in boldfaceJim Fehrle
2019-12-24Update merging doc following the full move to teams.Théo Zimmermann
Integrate merging doc in the main contributing document.
2019-12-24Merge PR #11284: [meta] Add ltac2 information to META.Théo Zimmermann
Ack-by: Zimmi48
2019-12-24[meta] Add ltac2 information to META.Emilio Jesus Gallego Arias
Closes #11225 , we use a bit of a hack due to the way the Makefile installs this plugin.
2019-12-24[ci] [gitlab] [bedrock] Build bedrock with 1 coreEmilio Jesus Gallego Arias
Most workers these days have 1 core, and building bedrock with 2 cores in that setup seems to be too memory stressful.
2019-12-24Merge PR #11316: Windows: switch OCaml to 4.08.1Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-12-24Add statements with output in TypeOlivier Laurent
2019-12-24[recordops] do not open GlobRefEnrico Tassi
2019-12-24[Attributes] accept #[canonical] (Let|Definition)Enrico Tassi
2019-12-24[CS] Allow a variable introduced with Let to be a canonical instanceEnrico Tassi
2019-12-23Merge PR #11293: Rename files with Class in their name to make their role ↵Hugo Herbelin
clearer.
2019-12-23Fixes a small bug exposing an _ANONYMOUS_REL in a unification error message.Hugo Herbelin
Might be improvable further. In the first example, we have two environments involved and one is implicit. It does not seem excluded that a variable name of the second environment shows up which is not listed in the first environment.
2019-12-23Merge PR #11274: [library] [cleanup] Remove code duplication.Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2019-12-23Windows: switch OCaml to 4.08.1Michael Soegtrop
- remove manual flexlink circular dependency handling - use standard configure process instead of hand made windows make files - enable parallel build - remove bootstrapping step (maybe should be there for release builds)
2019-12-23Merge PR #11324: [refman] Mention Ltac2 in intro.Pierre-Marie Pédrot
Reviewed-by: jfehrle
2019-12-23Merge PR #10760: Make rapply handle all numbers of underscoresPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2019-12-22Use code owner teams for every component.Théo Zimmermann
It was decided during the Coq WG that code owner teams are more convenient, in particular because they allow adding and removing team members without going through a pull request. For each team, we should aim to have at least three code owners, even if in some cases we are going to start with less. We also stop triggering review requests for changelog entries as was also decided during the WG.
2019-12-22Apply suggestions from code reviewThéo Zimmermann
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2019-12-22Rename files with Class in their name to make their role clearer.Pierre-Marie Pédrot
We restrict to those that are actually related to typeclasses, and perform the following renamings: Classops --> Coercionops Class --> ComCoercion
2019-12-22[refman] Mention Ltac2 in intro.Théo Zimmermann
2019-12-22Use the Alloc_small macro from the OCaml runtime rather than our own.Guillaume Melquiond
We cannot use caml_alloc_small because the macros Setup_for_gc and Restore_after_gc are still relevant (and critical). This means defining the CAML_INTERNALS macro, but it is a legit use and actually documented in the OCaml manual. This will help with forward compatibility with OCaml compilers, e.g., issue #10603. Unfortunately, it also means that we can no longer use #9914 to prevent memory corruption. The old macro is still used for OCaml versions prior to 4.10, as the upstream macro might process Ctrl+C when it is called.
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-27 10:14:19 +0000