Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR #7567: Clean-up dead file in test-suite. | 2018-05-23 | |
|\ | |||
* \ | Merge PR #7565: Document the new nested-proof error message. | 2018-05-22 | |
|\ \ | |||
* \ \ | Merge PR #7577: Fixing debugger after #6859 (loading dynlink.cma before ↵ | 2018-05-22 | |
|\ \ \ | | | | | | | | | | | | | lib.cma). | ||
| * | | | Fixing debugger after #6859 (loading dynlink.cma before lib.cma). | 2018-05-22 | |
| | | | | |||
* | | | | Merge PR #7384: Split Universes | 2018-05-22 | |
|\ \ \ \ | |/ / / |/| | | | |||
* | | | | Merge PR #7324: Infrastructure for ocamldebug on the checker | 2018-05-22 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #7526: [circle] Use Docker image from Gitlab registry. | 2018-05-22 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #7568: [ci] [gitlab] Fix printenv sorting for variables that span ↵ | 2018-05-22 | |
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | multiple lines | ||
* \ \ \ \ \ \ | Merge PR #6859: [stm] Make toplevels standalone executables. | 2018-05-22 | |
|\ \ \ \ \ \ \ | |||
| | * | | | | | | [ci] [gitlab] Fix printenv sorting for variables that span multiple lines. | 2018-05-21 | |
| |/ / / / / / |/| | | | | | | |||
| | | | | * | | Document the new nested-proof error message. | 2018-05-21 | |
| |_|_|_|/ / |/| | | | | | |||
| * | | | | | [ide] Remove special option `-ideslave` | 2018-05-21 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This has no effect anymore, verbose printing is controlled now by the regular, common `quiet` flag. | ||
| * | | | | | [stm] Make toplevels standalone executables. | 2018-05-21 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We turn coqtop "plugins" into standalone executables, which will be installed in `COQBIN` and located using the standard `PATH` mechanism. Using dynamic linking for `coqtop` customization didn't make a lot of sense, given that only one of such "plugins" could be loaded at a time. This cleans up some code and solves two problems: - `coqtop` needing to locate plugins, - dependency issues as plugins in `stm` depended on files in `toplevel`. In order to implement this, we do some minor cleanup of the toplevel API, making it functional, and implement uniform build rules. In particular: - `stm` and `toplevel` have become library-only directories, - a new directory, `topbin`, contains the new executables, - 4 new binaries have been introduced, for coqide and the stm. - we provide a common and cleaned up way to locate toplevels. | ||
| * | | | | | [ci] Add Dune to the base system. | 2018-05-21 | |
|/ / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It is needed by Elpi and pidetop, and it is anyways needed for most OCaml packages, including some Coq tools in the future. The future base Docker image will include it by default. | ||
* | | | | | Merge PR #7557: Add test cases from #7554 | 2018-05-20 | |
|\ \ \ \ \ | |||
| * | | | | | Add test cases from #7554 | 2018-05-20 | |
| | | | | | | | | | | | | | | | | | | | | | | | | Failed in v8.7.2 but were fixed by v8.8.0. | ||
* | | | | | | Merge PR #7527: [windows] Don't build menhir and int anymore in the ↵ | 2018-05-19 | |
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | packaging scripts. | ||
* \ \ \ \ \ \ | Merge PR #7550: [CI] Fix the script used by math-classes. | 2018-05-18 | |
|\ \ \ \ \ \ \ | |_|/ / / / / |/| | | | | | | |||
* | | | | | | | Merge PR #6965: [api] Move universe syntax to `Glob_term` | 2018-05-18 | |
|\ \ \ \ \ \ \ | |||
| | | | | | | * | Clean-up dead file in test-suite. | 2018-05-18 | |
| |_|_|_|_|_|/ |/| | | | | | | |||
| | * | | | | | [CI] Fix the script used by math-classes. | 2018-05-18 | |
| |/ / / / / |/| | | | | | | | | | | | | | | | | | We call configure to properly regenerate the Makefile and its dependencies. | ||
| | | | | * | Split off Universes functions for minimization. | 2018-05-17 | |
| | | | | | | | | | | | | | | | | | | | | | | | | This finishes the splitting of Universes. | ||
| | | | | * | Make Universes.refresh_constraints internal to UState | 2018-05-17 | |
| | | | | | | |||
| | | | | * | Split off Universes functions about substitutions and constraints | 2018-05-17 | |
| | | | | | | |||
| | | | | * | Remove unused argument to solve_constraints_system | 2018-05-17 | |
| | | | | | | |||
| | | | | * | Move solve_constraint_system near its only use site (comInductive) | 2018-05-17 | |
| | | | | | | |||
| | | | | * | Split off Universes functions dealing with generating new universes. | 2018-05-17 | |
| | | | | | | |||
| | | | | * | Split off Universes functions dealing with names. | 2018-05-17 | |
| | | | | | | | | | | | | | | | | | | | | | | | | This API is a bit strange, I expect it will change at some point. | ||
| | | | | * | Stop using Universes.subst(_opt)_univs_constr | 2018-05-17 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Should it be removed? The underlying `universe_subst -> constr -> constr` seems like it could be useful for plugins but where would the substitution be from? | ||
| | | | | * | Make set minimization option internal to Universes | 2018-05-17 | |
| |_|_|_|/ |/| | | | | |||
| | | * | | [circle] Use Docker image from Gitlab registry. | 2018-05-17 | |
| |_|/ / |/| | | | |||
* | | | | Merge PR #7451: Introduce an option to allow nested lemma, and turn it off ↵ | 2018-05-17 | |
|\ \ \ \ | | | | | | | | | | | | | | | | by default. | ||
* \ \ \ \ | Merge PR #7359: Reduce usage of evar_map references | 2018-05-17 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #7449: [vernac] taint two out-of-api `to_constr` use in ↵ | 2018-05-17 | |
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | `comDefinition`. | ||
* \ \ \ \ \ \ | Merge PR #6870: [ide] Don't set `quiet` on start. | 2018-05-17 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #7525: [ci] Try to build more of fiat-crypto. | 2018-05-17 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #6808: Add unit tests to test-suite | 2018-05-17 | |
|\ \ \ \ \ \ \ \ \ | |||
| | | | | | * | | | | Document nested proofs and associated option. | 2018-05-17 | |
| | | | | | | | | | | |||
| | | | | | * | | | | [STM] Nested Proofs Allowed has to be executed immediately | 2018-05-17 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | since it affects scheduling (actually the error the option lets one silence) | ||
| | | | | | * | | | | Remove deprecation warning for nested proofs. | 2018-05-17 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It is not clear yet that support for nested proofs will actually get removed in a future version. | ||
| | | | | | * | | | | Introduce an option to allow nested lemma, and turn it off by default. | 2018-05-17 | |
| |_|_|_|_|/ / / / |/| | | | | | | | | |||
* | | | | | | | | | Merge PR #7517: [sphinx] Fix indentation at the end of proof handling chapter. | 2018-05-16 | |
|\ \ \ \ \ \ \ \ \ | |||
| | * | | | | | | | | Modify make system to include Makefile.common in the test suite | 2018-05-16 | |
| | | | | | | | | | | |||
| | | * | | | | | | | [ci] Try to build more of fiat-crypto. | 2018-05-16 | |
| |_|/ / / / / / / |/| | | | | | | | | |||
* | | | | | | | | | Merge PR #7514: [ci] Don't build lite versions of CI developments. | 2018-05-16 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #7535: Typo in documentation of Derive | 2018-05-16 | |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #7493: Minor update of the documentation about the rcfile | 2018-05-16 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
| | * | | | | | | | | | | Typo in documentation of Derive | 2018-05-16 | |
| |/ / / / / / / / / / |/| | | | | | | | | | | |||
* | | | | | | | | | | | Merge PR #7079: Remove naked pointers from the VM | 2018-05-16 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7391: Add a small documentation writer's guide | 2018-05-16 | |
|\ \ \ \ \ \ \ \ \ \ \ \ |