aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-01-08Merge PR #6526: Fixing various typos in the Credits chapter.Maxime Dénès
2018-01-08github-check-prs.py: print PR URLs when needed.Gaëtan Gilbert
2018-01-08github-check-prs.py: Strip spaces from token from command lineGaëtan Gilbert
2018-01-08github-check-prs.py: command line option to get token from a fileGaëtan Gilbert
2018-01-08Merge PR #6510: Document between and exists_between types.Maxime Dénès
2018-01-08Document between and exists_between types.Ismail
2018-01-08Merge PR #6518: Fix build of micromega & nsatz with OCaml 4.06Maxime Dénès
2018-01-08Merge PR #6501: Document use of ocamldebug from the command line in ↵Maxime Dénès
Cygwin/Windows
2018-01-07Mention -B argument of make to rerun testsJasper Hugunin
2018-01-06First stab at documenting the test suite.Jasper Hugunin
2018-01-06Remove dir-locals and ship suggested helper hooks instead.Gaëtan Gilbert
.dir-locals led to issues with unsafe local variable warnings. With this method the user is opting in to running this code so there are no warnings.
2018-01-05[PR template] Remove the relative link.Théo Zimmermann
Was actually pointing to https://github.com/CHANGES.
2018-01-05Documentation and CHANGES for bracket with goal selector.Théo Zimmermann
2018-01-05Brackets support single numbered goal selectors.Théo Zimmermann
This allows to focus on a sub-goal other than the first one without resorting to the `Focus` command.
2018-01-04Normalize MacOS installer name.Théo Zimmermann
2018-01-04Normalize Windows installer names.Théo Zimmermann
2018-01-04Use a more efficient substitution composition in evar hypothesis naming.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-28 07:59:54 +0000