aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* [vernac] vernac_expr no longer recursiveGravatar Vincent Laporte2018-01-08
|
* [vernac] adds the “program” flag to the “atts” recordGravatar Vincent Laporte2017-12-29
|
* [vernac] Define types in orderGravatar Vincent Laporte2017-12-29
|
* Merge PR #6493: [API] remove large file containing duplicate interfacesGravatar Maxime Dénès2017-12-29
|\
* \ Merge PR #975: Create checklist for pull requests.Gravatar Maxime Dénès2017-12-29
|\ \
* \ \ Merge PR #6492: Remove query-in-IDE warning.Gravatar Maxime Dénès2017-12-29
|\ \ \
* \ \ \ Merge PR #6405: Remove the local polymorphic flag hack.Gravatar Maxime Dénès2017-12-29
|\ \ \ \
* \ \ \ \ Merge PR #6433: [flags] Move global time flag into an attribute.Gravatar Maxime Dénès2017-12-29
|\ \ \ \ \
| | | | | * overlay for #6493Gravatar Enrico Tassi2017-12-27
| | | | | |
| | | | | * [API] remove large file containing duplicate interfacesGravatar Enrico Tassi2017-12-27
| |_|_|_|/ |/| | | | | | | | | | | | | | | | | | | ... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client.
| | | * | Remove query-in-IDE warning.Gravatar Maxime Dénès2017-12-27
| |_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | I don't understand what is wrong with putting a query in a script running in the IDE. It is typically needed when giving demos, and that sounds like a ligitimate use case. By the way, we do it ourselves every year during the demo at CoqPL...
* | | | Merge PR #6102: Fix #5998: AppVeyor package building is currently failingGravatar Maxime Dénès2017-12-27
|\ \ \ \
| | | * | Add equations overlay.Gravatar Maxime Dénès2017-12-27
| | | | |
| | | * | Remove the local polymorphic flag hack.Gravatar Maxime Dénès2017-12-27
| |_|/ / |/| | | | | | | | | | | | | | | | | | | Some code in typeclasses was even breaking the invariant that use_polymorphic_flag should not be called twice, but that code was morally dead it seems, so we remove it.
| * | | Re-enable package building and artefact storage.Gravatar Maxime Dénès2017-12-27
| | | |
| * | | Fix #5998: AppVeyor package building is currently failingGravatar Maxime Dénès2017-12-27
| | | |
* | | | Merge PR #6507: [ide] [doc] Document tweak to Query call.Gravatar Maxime Dénès2017-12-27
|\ \ \ \
* \ \ \ \ Merge PR #6504: Fix overlay selection for Circle CI.Gravatar Maxime Dénès2017-12-27
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6040: Making coq_makefile usage consistent with what it claims + ↵Gravatar Maxime Dénès2017-12-27
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | possibly fixing printing errors (was: Removing failure of coq_makefile on no arguments)
* \ \ \ \ \ \ Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.Gravatar Maxime Dénès2017-12-27
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6444: [lib] Split auxiliary libraries into Coq-specific and general.Gravatar Maxime Dénès2017-12-27
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6443: [vernac] Cleanup of do_definition.Gravatar Maxime Dénès2017-12-27
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6495: Remove syntax for classification in TACTIC EXTEND.Gravatar Maxime Dénès2017-12-27
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6494: Remove legacy Value.normalize function.Gravatar Maxime Dénès2017-12-27
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6289: Remove unused boolean from cl_context field of ↵Gravatar Maxime Dénès2017-12-27
|\ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Typeclasses.typeclass
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6473: Fix warning about shadowing a global name.Gravatar Maxime Dénès2017-12-27
|\ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | * | | | [ide] [doc] Document tweak to Query call.Gravatar Emilio Jesus Gallego Arias2017-12-26
| |_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | |
| | | | | | | | | * | | | Fix overlay selection for Circle CI.Gravatar Gaëtan Gilbert2017-12-26
| | | | | | | | | | | | |
| | | | | | | | | * | | | Delete old overlays (leaving example)Gravatar Gaëtan Gilbert2017-12-26
| |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | |
| | | | | | | | | | | * Create pull request template.Gravatar Théo Zimmermann2017-12-24
| |_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | |
| | | | | | | * | | | [api] Also deprecate constructors of Decl_kinds.Gravatar Emilio Jesus Gallego Arias2017-12-23
| |_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Unfortunately OCaml doesn't deprecate the constructors of a type when the type alias is deprecated. In this case it means that we don't get rid of the kernel dependency unless we deprecate the constructors too.
| | | | | | | | | * [flags] Move global time flag into an attribute.Gravatar Emilio Jesus Gallego Arias2017-12-23
| |_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | One less global flag.
| | | | | | * | | [lib] Split auxiliary libraries into Coq-specific and general.Gravatar Emilio Jesus Gallego Arias2017-12-23
| |_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Up to this point the `lib` directory contained two different library archives, `clib.cma` and `lib.cma`, which a rough splitting between Coq-specific libraries and general-purpose ones. We know split the directory in two, as to make the distinction clear: - `clib`: contains libraries that are not Coq specific and implement common data structures and programming patterns. These libraries could be eventually replace with external dependencies and the rest of the code base wouldn't notice much. - `lib`: contains Coq-specific common libraries in widespread use along the codebase, but that are not considered part of other components. Examples are printing, error handling, or flags. In some cases we have coupling due to utility files depending on Coq specific flags, however this commit doesn't modify any files, but only moves them around, further cleanup is welcome, as indeed a few files in `lib` should likely be placed in `clib`. Also note that `Deque` is not used ATM.
| | | | | | * | Registering a printing handler in coq_makefile.Gravatar Hugo Herbelin2017-12-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows to fix the non-printing of error messages produced when parsing arguments.
| | | | | | * | Forbidding -o and -f in input file of coq_makefile.Gravatar Hugo Herbelin2017-12-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This was apparently either silently doing nothing or failing.
| | | | | | * | Removing failure of coq_makefile on no arguments.Gravatar Hugo Herbelin2017-12-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Nevertheless making option -o of coq_makefile recommended as discussed in PR#6040. This is one way to resolve the inconsistency with the usage which says that all arguments are optional.
* | | | | | | | Merge PR #6465: Gitlab touchupGravatar Maxime Dénès2017-12-22
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6469: No universe constraints in Let definitionsGravatar Maxime Dénès2017-12-22
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6318: Separate vernac controls and regular commands.Gravatar Maxime Dénès2017-12-22
|\ \ \ \ \ \ \ \ \ \
| | | | | | | * | | | Remove syntax for classification in TACTIC EXTEND.Gravatar Maxime Dénès2017-12-22
| |_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | It was left ignored after 8089dc960c9e8caf778907fd87be48d77b066433.
| | | | | | * | | | Remove legacy Value.normalize function.Gravatar Maxime Dénès2017-12-22
| |_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | It was the identity.
* | | | | | | | | Merge PR #6484: Update README and CONTRIBUTING to mention the wiki and FAQ.Gravatar Maxime Dénès2017-12-22
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6485: Fix badges.Gravatar Maxime Dénès2017-12-22
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6445: [stm] [ide protocol] Allow to include several commands on query.Gravatar Maxime Dénès2017-12-22
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6222: Share computation of unifiable evarsGravatar Maxime Dénès2017-12-22
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | * | | Merge code paths in interp_definition and cleanup a bit.Gravatar Gaëtan Gilbert2017-12-21
| | | | | | | | | | | | |
| | | * | | | | | | | | | Fix badges.Gravatar Théo Zimmermann2017-12-21
| |_|/ / / / / / / / / / |/| | | | | | | | | | |
| | | * | | | | | | | | Update README and CONTRIBUTING to mention the wiki and FAQ.Gravatar Théo Zimmermann2017-12-21
| |_|/ / / / / / / / / |/| | | | | | | | | |
* | | | | | | | | | | Merge PR #6474: Fix CI with parallel make (messed up dependencies)Gravatar Maxime Dénès2017-12-21
|\ \ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | | Fix CI with parallel make (messed up dependencies)Gravatar Gaëtan Gilbert2017-12-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When invoking through Makefile we always rebuild dependencies. To skip dependencies, invoke ci-wrapper directly. We make Circle CI do this. In order to properly support invoking ci-wrapper directly we replace "make" in ci-common by a bash function which adds -j to the make invocation outside submakes. We also set TIMED in the ci-wrapper.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 03:39:28 +0000