aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-01-04Update the lower-bound of the lablgtk dependency.Théo Zimmermann
Closes #6509.
2018-01-03add optimize_heap tactic for #6488Paul Steckler
2018-01-03update PNGs; mention async error handling; change query window to query ↵Paul Steckler
pane; use color descriptions
2018-01-03Fix core hint database issue #6521Anton Trunov
2018-01-02Cleanup name-binding structure for fresh evar name generation.Pierre-Marie Pédrot
We simply use a record and pack the rel and var substitutions in it. We also properly compose variable substitutions. Fixes #6534: Fresh variable generation in case of clash is buggy.
2018-01-01Fix mli-doc issue #6531Tony Beta Lambda
2017-12-31Ignore generated test-suite/output/MExtraction.outJason Gross
2017-12-31Trim more trailing whitespace in coq-makefile timing testJason Gross
Should help with https://github.com/coq/coq/issues/5675#issuecomment-353604702 Also replace a tab with spaces
2017-12-31Add a comment about universe lifting in sections in the kernel.Pierre-Marie Pédrot
2017-12-30Expound on dependencies for github-check-prs.pyGaëtan Gilbert
2017-12-30Python script checking missing/unnecessary [needs: rebase] labelGaëtan Gilbert
2017-12-30Moving some universe substitution code out of the kernel.Pierre-Marie Pédrot
This code was not used at all inside the kernel, it was related to universe unification that happens in the upper layer. It makes more sense to put it somewhere upper.
2017-12-30Returning instance instead of substitution in universe context abstraction.Pierre-Marie Pédrot
This datatype enforces stronger invariants, e.g. that we only have in the substitution codomain a connex interval of variables from 0 to n - 1.
2017-12-30Hardening universe abstraction in Cooking.Pierre-Marie Pédrot
2017-12-30Using a dedicated type for Lib.abstr_info.Pierre-Marie Pédrot
2017-12-29Add instructions for debugging from the command line (and in Windows)Jim Fehrle
Avoid generating \r characters in generated dev/ocamldebug-coq (affects Windows)
2017-12-29[vernac] adds the “program” flag to the “atts” recordVincent Laporte
2017-12-29[vernac] Define types in orderVincent Laporte
2017-12-29Share the rel environment between Environ.env and reduction cache.Pierre-Marie Pédrot
2017-12-29Fast environment lookup for rels.Pierre-Marie Pédrot
We take advantage of the range structure to get a O(log n) retrieval of values bound to a rel in an environment.
2017-12-29Adding skewed lists.Pierre-Marie Pédrot
This is a purely functional datastructure isomorphic to usual lists, except that it features a O(log n) lookup while preserving the O(1) cons operation.
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-28[Makefile] plugins micromega and nsatz depend on unix and numVincent Laporte
2017-12-28[default.nix] depends on ocamlPackages.numVincent Laporte
2017-12-27Add TIMING_SORT_BY and --sort-by to timing scriptsJason Gross
This should help with #5675, in particular with https://github.com/coq/coq/issues/5675#issuecomment-349716292
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-21 05:44:41 +0000