aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
* Merge PR #7906: universes_of_constr don't include universes of monomorphic ↵Gravatar Pierre-Marie Pédrot2018-06-26
|\ | | | | | | constants
* \ Merge PR #7831: Fix for issue #7707: include Ltac2 and Equations in Windows ↵Gravatar Maxime Dénès2018-06-26
|\ \ | | | | | | | | | build
* \ \ Merge PR #7783: Move INSTALL.doc to doc/README.md and improve a few things.Gravatar Maxime Dénès2018-06-26
|\ \ \
| | | * Add overlay for Equations, ElpiGravatar Gaëtan Gilbert2018-06-26
| | | |
| | * | Activate the build of Ltac2 and Equations in the Windows installer.Gravatar Théo Zimmermann2018-06-25
| | | |
| | * | Reuse CI info to know which version of plugins to build on Windows.Gravatar Théo Zimmermann2018-06-25
| | | |
| | * | Fix for issue 7707: include Ltac2 and Equations in Windows buildGravatar Michael Soegtrop2018-06-25
| |/ / |/| | | | | | | | On the way I also fixed some minor issues with calling MakeCoq_MinGW from cygwin.
* | | Merge PR #7895: Revert "Add a note about [ci skip] in CI README."Gravatar Emilio Jesus Gallego Arias2018-06-24
|\ \ \
* \ \ \ Merge PR #7805: Towards listing the critical bugs of the history of Coq.Gravatar Théo Zimmermann2018-06-24
|\ \ \ \
* \ \ \ \ Merge PR #7893: Update dpdgraph branch nameGravatar Théo Zimmermann2018-06-22
|\ \ \ \ \ | |_|_|_|/ |/| | | |
| | | * | Revert "Add a note about [ci skip] in CI README."Gravatar Théo Zimmermann2018-06-22
| |_|/ / |/| | | | | | | | | | | This reverts commit 3a44a190a7f5d057b6a4bcb50124b42d83f3d03d.
| | | * Fix Windows install script following removal of INSTALL.ide and move of ↵Gravatar Théo Zimmermann2018-06-22
| |_|/ |/| | | | | | | | INSTALL.doc.
* | | Merge PR #7774: [build] Fix checks and notes noting 4.02.1 instead of 4.02.3Gravatar Maxime Dénès2018-06-21
|\ \ \
| | * | Update dpdgraph branch nameGravatar Gaëtan Gilbert2018-06-21
| |/ / |/| | | | | | | | See https://github.com/Karmaki/coq-dpdgraph/issues/50 for context
* | | Merge PR #7797: Remove reference name type.Gravatar Enrico Tassi2018-06-19
|\ \ \
| * | | Overlay for reference removalGravatar Maxime Dénès2018-06-18
| | | |
* | | | Update section on adding your project to CI and link to example PR.Gravatar Théo Zimmermann2018-06-18
| | | |
| * | | Remove reference name type.Gravatar Maxime Dénès2018-06-18
|/ / / | | | | | | | | | | | | | | | | | | | | | reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid.
* | | Merge PR #7752: [merge script] Check if the CI that was run is outdated.Gravatar Maxime Dénès2018-06-17
|\ \ \
| | | * Very first try at listing the critical bugs of the history of Coq.Gravatar Hugo Herbelin2018-06-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | I let open several questions about fixes to the kernel which maybe were not critical. I skipped what seemed to have been bugs in beta-releases. Need double-checks, decision about the format, etc.
* | | | Merge PR #7793: [ci] update docker image to include elpi 1.0.4Gravatar Emilio Jesus Gallego Arias2018-06-14
|\ \ \ \
* \ \ \ \ Merge PR #664: Fixing #5500 (missing test in return clause of match leading ↵Gravatar Matthieu Sozeau2018-06-14
|\ \ \ \ \ | |_|_|_|/ |/| | | | | | | | | to anomaly)
| | * | | [ci] update docker image to include elpi 1.0.4Gravatar Enrico Tassi2018-06-13
| | | | |
* | | | | Document how to restart failed CI jobs.Gravatar Théo Zimmermann2018-06-13
| | | | | | | | | | | | | | | | | | | | [ci skip]
* | | | | Markdown docs: switch from absolute to relative links.Gravatar Théo Zimmermann2018-06-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We had mostly used absolute links in the past. I just discovered that GitHub recommends using relative links instead: https://help.github.com/articles/basic-writing-and-formatting-syntax/#relative-links and indeed my Emacs Markdown mode can handle relative links but doesn't interpret absolute links relatively to the root of the git repository. [ci skip]
* | | | | [api] Add compatiblity Misctypes module.Gravatar Emilio Jesus Gallego Arias2018-06-12
| | | | | | | | | | | | | | | | | | | | To be removed in 8.10.
* | | | | [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
| |/ / / |/| | | | | | | | | | | | | | | - move_location to proofs/logic. - intro_pattern_naming to Namegen.
* | | | Merge PR #6827: [VM] Remove projection names from structured constants.Gravatar Pierre-Marie Pédrot2018-06-11
|\ \ \ \
| | | | * [build] Fix checks and notes noting 4.02.1 instead of 4.02.3Gravatar Emilio Jesus Gallego Arias2018-06-11
| |_|_|/ |/| | | | | | | | | | | | | | | Bumping to 4.02.3 was decided some time ago in the WG, however a couple of places escaped updating.
* | | | [ci] GeoCoq now depends on math-comp's ssralg.Gravatar Emilio Jesus Gallego Arias2018-06-11
| | | |
| * | | [VM] Remove projection names from structured constants.Gravatar Maxime Dénès2018-06-10
|/ / / | | | | | | | | | | | | | | | | | | It was actually a hack since those names are never used to represent values, only to be passed as arguments to bytecode instructions. So instead of reusing the structured_constant type, we follow the same pattern as switch annotations.
| | * [merge script] Check if the CI that was run is outdated.Gravatar Théo Zimmermann2018-06-09
| |/ |/| | | | | [ci skip]
* | dev/doc/univpoly.{txt => md}, split off primitive projection infoGravatar Gaëtan Gilbert2018-06-08
| |
* | Merge PR #7687: [ci] [docker] Pin specific versions of OPAM CI dependencies.Gravatar Gaëtan Gilbert2018-06-08
|\ \
| * | [ci] [docker] Pin specific versions of OPAM CI dependencies.Gravatar Emilio Jesus Gallego Arias2018-06-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Packages such as `menhir` or `elpi` are fragile w.r.t. updates, so allowing a non-deterministic install in the Dockefile seems risky. We have found trouble with Menhir in the past. We thus specify a concrete version for all `CI_OPAM` packages. cc: https://github.com/AbsInt/CompCert/issues/234 We also add remove `hevea` from `apt` dependencies as it hasn't been needed since #7466 and add `texlive-science` which is needed to build the `source-doc` target due to the `textgreek` package being used.
* | | Add a note about [ci skip] in CI README.Gravatar Théo Zimmermann2018-06-06
|/ /
* | Merge PR #7717: [ci] Temporal fix for CompCertGravatar Gaëtan Gilbert2018-06-06
|\ \
| * | [ci] Temporal fix for CompCertGravatar Emilio Jesus Gallego Arias2018-06-06
| | | | | | | | | | | | https://github.com/AbsInt/CompCert/issues/234
* | | Merge PR #7099: Stronger invariants in unification signature.Gravatar Matthieu Sozeau2018-06-05
|\ \ \
* \ \ \ Merge PR #7495: Fix restrict_universe_contextGravatar Matthieu Sozeau2018-06-05
|\ \ \ \ | |_|/ / |/| | |
* | | | Merge PR #7596: [ci] [windows] Use newer OCaml version.Gravatar Michael Soegtrop2018-06-04
|\ \ \ \
| | | * | Documenting the API change.Gravatar Pierre-Marie Pédrot2018-06-04
| | | | |
| | | * | Adding an overlay for the Equations plugin.Gravatar Pierre-Marie Pédrot2018-06-04
| |_|/ / |/| | |
* | | | QuickChick CIGravatar Leonidas Lampropoulos2018-06-02
| | | |
* | | | [ci] Expose updated `OCAMLPATH` for CI users.Gravatar Emilio Jesus Gallego Arias2018-06-02
| | | | | | | | | | | | | | | | | | | | This is needed for CI packages that use `META.coq` such as in https://github.com/coq/coq/pull/7656 .
| * | | [appveyor] Use OCaml version 4.06.1 in the Windows build.Gravatar Emilio Jesus Gallego Arias2018-06-02
|/ / / | | | | | | | | | | | | | | | We bump Windows builds to 4.06.1, IMHO it makes sense to use the latest OCaml version to build on that platform due to the support status and number of fixes.
* | | [api] Move `Constrexpr` to the `interp` module.Gravatar Emilio Jesus Gallego Arias2018-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Continuing the interface cleanup we place `Constrexpr` in the internalization module, which is the one that eliminates it. This slims down `pretyping` considerably, including removing the `Univdecls` module which existed only due to bad dependency ordering in the first place. Thanks to @ Skyskimmer we also remove a duplicate `univ_decl` definition among `Misctypes` and `UState`. This is mostly a proof of concept yet as it depends on quite a few patches of the tree. For sure some tweaks will be necessary, but it should be good for review now. IMO the tree is now in a state where we can could easy eliminate more than 10 modules without any impact, IMHO this is a net saving API-wise and would help people to understand the structure of the code better.
* | | [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We remove most of what was deprecated in `Term`. Now, `intf` and `kernel` are almost deprecation-free, tho I am not very convinced about the whole `Term -> Constr` renaming but I'm afraid there is no way back. Inconsistencies with the constructor policy (see #6440) remain along the code-base and I'm afraid I don't see a plan to reconcile them. The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a good idea as someone added a `List` module inside it.
* | | Merge PR #7558: [api] Make `vernac/` self-contained.Gravatar Maxime Dénès2018-05-30
|\ \ \
| | * | overlay triggering bug #7472 (that #7495) is supposed to fixGravatar Enrico Tassi2018-05-30
| |/ / |/| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-24 03:35:19 +0000