| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-04-09 | Merge script: adds a way for confirmation to expect a newline. | Théo Zimmermann | |
| This fulfils Gaetan's wish. | |||
| 2018-04-09 | Add sanity check in merge script: local branch is up-to-date. | Théo Zimmermann | |
| In case the local branch is ahead of upstream, we only print a warning because it could be that we are merging several PRs in a row. | |||
| 2018-04-08 | Document requirement to have git >= 2.7 to use the merge script. | Théo Zimmermann | |
| As reported in https://github.com/coq/coq/issues/7097#issuecomment-378632415 | |||
| 2018-04-08 | Merge script does not warn when the remote is set to HTTPS. | Théo Zimmermann | |
| This should solve Emilio's problem. | |||
| 2018-04-08 | Merge script: use fetch URL for the remote. | Théo Zimmermann | |
| In case the push URL has been overriden to make it fetch-only. | |||
| 2018-04-08 | Merge PR #6809: Improve shell scripts | Michael Soegtrop | |
| 2018-04-06 | Merge PR #6960: [api] Move some types to their proper module. | Pierre-Marie Pédrot | |
| 2018-04-06 | Merge PR #7178: Fixes issue #7172 (don't include MinGW make in install) | Enrico Tassi | |
| 2018-04-05 | Improve shell scripts | zapashcanon | |
| 2018-04-05 | Fixes issue #7172 (don't include MinGW make in install) | Michael Soegtrop | |
| 2018-04-05 | Add note for homebrew users. | Théo Zimmermann | |
| 2018-04-05 | Some advice about merge script dependencies. | Théo Zimmermann | |
| Including: how to create a GPG key. | |||
| 2018-04-05 | Improve the MERGING doc. | Théo Zimmermann | |
| In particular, describes what to do with overlays. | |||
| 2018-04-03 | merge-pr.sh: cache github API calls | Gaëtan Gilbert | |
| 2018-04-02 | [api] Move some types to their proper module. | Emilio Jesus Gallego Arias | |
| We solve some modularity and type duplication problems by moving types to a better place. In particular: - We move tactics types from `Misctypes` to `Tactics` as this is their proper module an single user [with LTAC]. - We deprecate aliases in `Tacexpr` to such tactic types. cc: #6512 | |||
| 2018-03-31 | Merge PR #6950: pre-commit, linter: verify user overlay extensions (must be sh) | Emilio Jesus Gallego Arias | |
| 2018-03-31 | Linter: verify overlay extensions. | Gaëtan Gilbert | |
| 2018-03-31 | pre-commit: verify user overlay extensions (must be .sh). | Gaëtan Gilbert | |
| This has come up a couple times. | |||
| 2018-03-29 | Remove outdated patch from ci-sf | Jasper Hugunin | |
| 2018-03-26 | Merge PR #6739: Tentative fix for #6520: camlcity.org unresponsive makes ↵ | Maxime Dénès | |
| AppVeyor fail. | |||
| 2018-03-26 | Merge PR #6970: [vernac] Move `Quit` and `Drop` to the toplevel layer. | Enrico Tassi | |
| 2018-03-23 | Merge PR #7029: improve merge-pr script | Maxime Dénès | |
| 2018-03-23 | improve merge-pr script | Enrico Tassi | |
| The script now performs many more checks and reports errors in a more intelligible way. | |||
| 2018-03-23 | More precise wording about the merge process. | Maxime Dénès | |
| In particular, don't use the GitHub interface. Also, not all reviews are mandatory in some corner cases. | |||
| 2018-03-21 | Refine a bit the decentralized merging process. | Maxime Dénès | |
| We make GitHub assign only principal maintainers as reviewers. This reduces the level of noise (PRs with 10 code owners), and makes it easy for the assignee to check if all reviews have been completed (all reviewers in the list have to approve the PR, which was not the case before if two reviewers were assigned for the same component). This change means that when a principal maintainer submits a patch touching the component they own, they should ask a review from the secondary maintainer. | |||
| 2018-03-19 | Describe new merging process. | Maxime Dénès | |
| 2018-03-15 | [win] update bignums to tag V8.8+beta1 | Enrico Tassi | |
| 2018-03-11 | [vernac] Move `Quit` and `Drop` to the toplevel layer. | Emilio Jesus Gallego Arias | |
| This is a first step towards moving REPL-specific commands out of the core layers. In particular, we remove `Quit` and `Drop` from the core vernacular to specific toplevel-level parsing rules. | |||
| 2018-03-10 | [ssreflect] Fix module scoping problems due to packing and mli files. | Emilio Jesus Gallego Arias | |
| Unfortunately, mli-only files cannot be included in packs, so we have the weird situation that the scope for `Tacexpr` is wrong. So we cannot address the module as `Ltac_plugin.Tacexpr` but it lives in the global namespace instead. This creates problem when using other modular build/packing strategies [such as #6857] This could be indeed considered a bug in the OCaml compiler. In order to remedy this situation we face two choices: - leave the module out of the pack (!) - create an implementation for the module I chose the second solution as it seems to me like the most sensible choice. cc: #6512. | |||
| 2018-03-09 | [located] Push inner locations in `reference` to a CAst.t node. | Emilio Jesus Gallego Arias | |
| The `reference` type contains some ad-hoc locations in its constructors, but there is no reason not to handle them with the standard attribute container provided by `CAst.t`. An orthogonal topic to this commit is whether the `reference` type should contain a location or not at all. It seems that many places would become a bit clearer by splitting `reference` into non-located `reference` and `lreference`, however some other places become messier so we maintain the current status-quo for now. | |||
| 2018-03-09 | [located] More work towards using CAst.t | Emilio Jesus Gallego Arias | |
| We continue with the work of #402 and #6745 and update most of the remaining parts of the AST: - module declarations - intro patterns - top-level sentences Now, parsed documents should be full annotated by `CAst` nodes. | |||
| 2018-03-09 | Merge PR #6775: Allow using cumulativity without forcing strict constraints. | Maxime Dénès | |
| 2018-03-09 | Overlay for Elpi. | Gaëtan Gilbert | |
| 2018-03-09 | Add an overlay for Equations and Ltac2. | Pierre-Marie Pédrot | |
| 2018-03-08 | Merge PR #6817: [configure]: support for profiles | Maxime Dénès | |
| 2018-03-08 | Merge PR #6881: [windows] support -addon in build script | Maxime Dénès | |
| 2018-03-06 | document -profile in dev/doc/setup.txt | Enrico Tassi | |
| 2018-03-06 | Standard headers for C and Python. | Maxime Dénès | |
| 2018-03-06 | Hack to make bignum build on windows | Enrico Tassi | |
| 2018-03-06 | build: win: turn off build/installation of gnu Make | Enrico Tassi | |
| 2018-03-05 | Merge PR #6855: Update headers following #6543. | Maxime Dénès | |
| 2018-03-04 | Merge PR #935: Handling evars in the VM | Maxime Dénès | |
| 2018-03-04 | Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`. | Maxime Dénès | |
| 2018-03-04 | Merge PR #6876: Unify Const_sorts and Const_type, and remove Vsort | Maxime Dénès | |
| 2018-03-04 | Merge PR #6873: [toplevel] Update state when `Drop` exception is thrown [#6872] | Maxime Dénès | |
| 2018-03-04 | Merge PR #6676: [proofview] goals come with a state | Maxime Dénès | |
| 2018-03-03 | Handling evars in the VM. | Pierre-Marie Pédrot | |
| We simply treat them as as an application of an atom to its instance, and in the decompilation phase we reconstruct the instance from the stack. This grants wish BZ#5659. | |||
| 2018-03-02 | [VM] Unify Const_sorts and Const_type, and remove Vsort. | Maxime Dénès | |
| This simplifies the representation of values, and brings it closer to the ones of the native compiler. | |||
| 2018-03-02 | installer: win: put addons in a separate package | Enrico Tassi | |
| 2018-03-02 | build: win: detect 404 as HTML files | Enrico Tassi | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |