aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2018-06-25Reuse CI info to know which version of plugins to build on Windows.Théo Zimmermann
2018-06-25Fix for issue 7707: include Ltac2 and Equations in Windows buildMichael Soegtrop
On the way I also fixed some minor issues with calling MakeCoq_MinGW from cygwin.
2018-06-25Mini-update of version history with recent changes.Hugo Herbelin
2018-06-25Critical bugs: added #3243 and Gonthier's bug in lazy machine.Hugo Herbelin
Both reminded by Enrico.
2018-06-24Merge PR #7895: Revert "Add a note about [ci skip] in CI README."Emilio Jesus Gallego Arias
2018-06-24Merge PR #7805: Towards listing the critical bugs of the history of Coq.Théo Zimmermann
2018-06-22Merge PR #7893: Update dpdgraph branch nameThéo Zimmermann
2018-06-22Revert "Add a note about [ci skip] in CI README."Théo Zimmermann
This reverts commit 3a44a190a7f5d057b6a4bcb50124b42d83f3d03d.
2018-06-22Fix Windows install script following removal of INSTALL.ide and move of ↵Théo Zimmermann
INSTALL.doc.
2018-06-21Merge PR #7774: [build] Fix checks and notes noting 4.02.1 instead of 4.02.3Maxime Dénès
2018-06-21Update dpdgraph branch nameGaëtan Gilbert
See https://github.com/Karmaki/coq-dpdgraph/issues/50 for context
2018-06-19Merge PR #7797: Remove reference name type.Enrico Tassi
2018-06-18Overlay for reference removalMaxime Dénès
2018-06-18Update section on adding your project to CI and link to example PR.Théo Zimmermann
2018-06-18Remove reference name type.Maxime Dénès
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.
2018-06-17Merge PR #7752: [merge script] Check if the CI that was run is outdated.Maxime Dénès
2018-06-15Very first try at listing the critical bugs of the history of Coq.Hugo Herbelin
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.
2018-06-14Merge PR #7793: [ci] update docker image to include elpi 1.0.4Emilio Jesus Gallego Arias
2018-06-14Merge PR #664: Fixing #5500 (missing test in return clause of match leading ↵Matthieu Sozeau
to anomaly)
2018-06-13[ci] update docker image to include elpi 1.0.4Enrico Tassi
2018-06-13Document how to restart failed CI jobs.Théo Zimmermann
[ci skip]
2018-06-13Markdown docs: switch from absolute to relative links.Théo Zimmermann
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]
2018-06-12[api] Add compatiblity Misctypes module.Emilio Jesus Gallego Arias
To be removed in 8.10.
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
- move_location to proofs/logic. - intro_pattern_naming to Namegen.
2018-06-11Merge PR #6827: [VM] Remove projection names from structured constants.Pierre-Marie Pédrot
2018-06-11[build] Fix checks and notes noting 4.02.1 instead of 4.02.3Emilio Jesus Gallego Arias
Bumping to 4.02.3 was decided some time ago in the WG, however a couple of places escaped updating.
2018-06-11[ci] GeoCoq now depends on math-comp's ssralg.Emilio Jesus Gallego Arias
2018-06-10[VM] Remove projection names from structured constants.Maxime Dénès
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.
2018-06-09[merge script] Check if the CI that was run is outdated.Théo Zimmermann
[ci skip]
2018-06-08dev/doc/univpoly.{txt => md}, split off primitive projection infoGaëtan Gilbert
2018-06-08Merge PR #7687: [ci] [docker] Pin specific versions of OPAM CI dependencies.Gaëtan Gilbert
2018-06-06[ci] [docker] Pin specific versions of OPAM CI dependencies.Emilio Jesus Gallego Arias
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.
2018-06-06Add a note about [ci skip] in CI README.Théo Zimmermann
2018-06-06Merge PR #7717: [ci] Temporal fix for CompCertGaëtan Gilbert
2018-06-06[ci] Temporal fix for CompCertEmilio Jesus Gallego Arias
https://github.com/AbsInt/CompCert/issues/234
2018-06-05Merge PR #7099: Stronger invariants in unification signature.Matthieu Sozeau
2018-06-05Merge PR #7495: Fix restrict_universe_contextMatthieu Sozeau
2018-06-04Merge PR #7596: [ci] [windows] Use newer OCaml version.Michael Soegtrop
2018-06-04Documenting the API change.Pierre-Marie Pédrot
2018-06-04Adding an overlay for the Equations plugin.Pierre-Marie Pédrot
2018-06-02QuickChick CILeonidas Lampropoulos
2018-06-02[ci] Expose updated `OCAMLPATH` for CI users.Emilio Jesus Gallego Arias
This is needed for CI packages that use `META.coq` such as in https://github.com/coq/coq/pull/7656 .
2018-06-02[appveyor] Use OCaml version 4.06.1 in the Windows build.Emilio Jesus Gallego Arias
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.
2018-05-31[api] Move `Constrexpr` to the `interp` module.Emilio Jesus Gallego Arias
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.
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
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.
2018-05-30Merge PR #7558: [api] Make `vernac/` self-contained.Maxime Dénès
2018-05-30overlay triggering bug #7472 (that #7495) is supposed to fixEnrico Tassi
2018-05-28Merge PR #7521: Fix soundness bug with VM/native and cofixpointsPierre-Marie Pédrot
2018-05-28Unify pre_env and envMaxime Dénès
We now have only two notions of environments in the kernel: env and safe_env.
2018-05-28Merge PR #7419: Remove 100 occurrences of Evd.emptyPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-02 19:05:25 +0000