aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-01-16merge-pr.sh: use git diff --quietGaëtan Gilbert
2018-01-16Source basic overlay before user overlays.Gaëtan Gilbert
2018-01-16Cleanup shell expansions and quoting.Gaëtan Gilbert
2018-01-16Simplify logic and streamline lint-repository.shGaëtan Gilbert
We inline should-check-whitespace.sh in check-eof-newline.sh simplifying the find invocation.
2018-01-08Cleanup conditional in lint-repository.shGaëtan Gilbert
2017-12-29Merge PR #6493: [API] remove large file containing duplicate interfacesMaxime Dénès
2017-12-29Merge PR #975: Create checklist for pull requests.Maxime Dénès
2017-12-29Merge PR #6492: Remove query-in-IDE warning.Maxime Dénès
2017-12-29Merge PR #6405: Remove the local polymorphic flag hack.Maxime Dénès
2017-12-29Merge PR #6433: [flags] Move global time flag into an attribute.Maxime Dénès
2017-12-27overlay for #6493Enrico Tassi
2017-12-27[API] remove large file containing duplicate interfacesEnrico Tassi
... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client.
2017-12-27Remove query-in-IDE warning.Maxime Dénès
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...
2017-12-27Merge PR #6102: Fix #5998: AppVeyor package building is currently failingMaxime Dénès
2017-12-27Add equations overlay.Maxime Dénès
2017-12-27Remove the local polymorphic flag hack.Maxime Dénès
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.
2017-12-27Re-enable package building and artefact storage.Maxime Dénès
2017-12-27Fix #5998: AppVeyor package building is currently failingMaxime Dénès
2017-12-27Merge PR #6507: [ide] [doc] Document tweak to Query call.Maxime Dénès
2017-12-27Merge PR #6504: Fix overlay selection for Circle CI.Maxime Dénès
2017-12-27Merge PR #6040: Making coq_makefile usage consistent with what it claims + ↵Maxime Dénès
possibly fixing printing errors (was: Removing failure of coq_makefile on no arguments)
2017-12-27Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.Maxime Dénès
2017-12-27Merge PR #6444: [lib] Split auxiliary libraries into Coq-specific and general.Maxime Dénès
2017-12-27Merge PR #6443: [vernac] Cleanup of do_definition.Maxime Dénès
2017-12-27Merge PR #6495: Remove syntax for classification in TACTIC EXTEND.Maxime Dénès
2017-12-27Merge PR #6494: Remove legacy Value.normalize function.Maxime Dénès
2017-12-27Merge PR #6289: Remove unused boolean from cl_context field of ↵Maxime Dénès
Typeclasses.typeclass
2017-12-27Merge PR #6473: Fix warning about shadowing a global name.Maxime Dénès
2017-12-26[ide] [doc] Document tweak to Query call.Emilio Jesus Gallego Arias
2017-12-26Fix overlay selection for Circle CI.Gaëtan Gilbert
2017-12-26Delete old overlays (leaving example)Gaëtan Gilbert
2017-12-24Create pull request template.Théo Zimmermann
2017-12-23[api] Also deprecate constructors of Decl_kinds.Emilio Jesus Gallego Arias
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.
2017-12-23[flags] Move global time flag into an attribute.Emilio Jesus Gallego Arias
One less global flag.
2017-12-23[lib] Split auxiliary libraries into Coq-specific and general.Emilio Jesus Gallego Arias
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.
2017-12-23Registering a printing handler in coq_makefile.Hugo Herbelin
This allows to fix the non-printing of error messages produced when parsing arguments.
2017-12-23Forbidding -o and -f in input file of coq_makefile.Hugo Herbelin
This was apparently either silently doing nothing or failing.
2017-12-23Removing failure of coq_makefile on no arguments.Hugo Herbelin
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.
2017-12-22Merge PR #6465: Gitlab touchupMaxime Dénès
2017-12-22Merge PR #6469: No universe constraints in Let definitionsMaxime Dénès
2017-12-22Merge PR #6318: Separate vernac controls and regular commands.Maxime Dénès
2017-12-22Remove syntax for classification in TACTIC EXTEND.Maxime Dénès
It was left ignored after 8089dc960c9e8caf778907fd87be48d77b066433.
2017-12-22Remove legacy Value.normalize function.Maxime Dénès
It was the identity.
2017-12-22Merge PR #6484: Update README and CONTRIBUTING to mention the wiki and FAQ.Maxime Dénès
2017-12-22Merge PR #6485: Fix badges.Maxime Dénès
2017-12-22Merge PR #6445: [stm] [ide protocol] Allow to include several commands on query.Maxime Dénès
2017-12-22Merge PR #6222: Share computation of unifiable evarsMaxime Dénès
2017-12-21Merge code paths in interp_definition and cleanup a bit.Gaëtan Gilbert
2017-12-21Fix badges.Théo Zimmermann
2017-12-21Update README and CONTRIBUTING to mention the wiki and FAQ.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 19:04:57 +0000