aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-12-04Merge PR #13442: Add an abstraction function in the LtacX FFI.coqbot-app[bot]
Reviewed-by: kyoDralliam
2020-12-04Delay inventing names for monomorphic universesGaëtan Gilbert
This avoids doing it repeatedly for nothing in intern/extern.
2020-12-04Merge PR #13551: Stop calling Id.Map.domain on univ binders every individual ↵coqbot-app[bot]
universe Reviewed-by: herbelin
2020-12-04[dune] [test-suite] pass BIN= as the regular makefile doesEnrico Tassi
2020-12-04[test-suite] improve ocaml_pwdEnrico Tassi
2020-12-04[win] [envars] honor file "coq_environment.txt"Enrico Tassi
On windows we provide a way to set environment variables local to a coq installation by providing a file named "coq_environment.txt" containing KEY="value" pairs. No space between KEY and = is allowed, values are in quotes according to OCaml's escaping conventions. The file is line-directed, illformed lines are skipped.
2020-12-04[doc] coq_environment.txtEnrico Tassi
2020-12-04[coq_makefile] use Envars for COQMF_WINDRIVEEnrico Tassi
2020-12-04[coq_makefile] honor environment for OCAMLFINDEnrico Tassi
2020-12-04typoYves Bertot
2020-12-04Merge PR #13497: [rm] update release notescoqbot-app[bot]
Reviewed-by: Zimmi48
2020-12-04[rm] clarify process for is_a_released_version = trueEnrico Tassi
2020-12-04[rm] update git commands to push tagsEnrico Tassi
2020-12-04Merge PR #13527: Changes for Coq 8.13coqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: jfehrle
2020-12-04Better primitive type support in custom string and numeral notations.Fabian Kunze
- float and array values are now supported for printing and parsing in custom notations (and in notations defined using the ocaml API) - the three constants bound to the primitive float, int and array type are now allowed anywhere inside a term to print, to handle them similar to `real` type constructors - Grants #13484: String notations for primitive arrays - Fixes #13517: String notation printing fails with primitive integers inside lists
2020-12-03Merge PR #13546: [coqide] fix procedure to parse argumentscoqbot-app[bot]
Reviewed-by: ejgallego
2020-12-03Merge PR #13558: [refman] Fix error names.coqbot-app[bot]
Reviewed-by: jfehrle
2020-12-03Ascii: add leb and ltbYishuai Li
2020-12-03Implement review corrections by Théo ZimmermannMatthieu Sozeau
2020-12-03Implement suggestions by Théo ZimmermannMatthieu Sozeau
2020-12-03Apply suggestions from code reviewMatthieu Sozeau
Co-authored-by: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2020-12-03Apply suggestions from code reviewEnrico Tassi
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-12-03Update doc/sphinx/changes.rstMatthieu Sozeau
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-12-03Fixes in the summary by Jim FehrleMatthieu Sozeau
Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
2020-12-03Changes without PR references fixesMatthieu Sozeau
2020-12-03Apply suggestions from @jfehrle code reviewMatthieu Sozeau
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-12-03[changelog] update markupEnrico Tassi
2020-12-03Add an anchor in syntax-extensionsMatthieu Sozeau
2020-12-03Changes for Coq 8.13Matthieu Sozeau
2020-12-03Merge PR #13548: Move *_with_full_binders variants out of the kernel.coqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: herbelin
2020-12-03[coqide] fix procedure to parse argumentsEnrico Tassi
coqide calls coqidetop -batch, if you are in -async-proof on then coqidetop spawns a worker and passes -batch to it. At some point, I could not find the commit, this made the worker die. On linux it seems it works anyway, but on windows this death is perceived by coqide which then does not start.
2020-12-03[refman] Fix error names.Théo Zimmermann
The @ syntax is not supported in the name, so we transform it manually as it would have been if no name had been provided.
2020-12-03Merge PR #13554: Split long lines in errors and warning indexcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-12-02Split long lines in errors and warning indexJim Fehrle
2020-12-02Merge PR #13275: Put all Int63 primitives in a separate fileVincent Laporte
Ack-by: SkySkimmer Ack-by: ppedrot Reviewed-by: vbgl
2020-12-02Document Number Notation for primitive integersPierre Roux
2020-12-02compute_instance_binders: use prebuilt reverse mapGaëtan Gilbert
2020-12-02Stop calling Id.Map.domain on univ binders every individual universeGaëtan Gilbert
2020-12-02Merge PR #13471: gitlab CI: remove redundant "dependencies" infocoqbot-app[bot]
Reviewed-by: Zimmi48
2020-12-02Move *_with_full_binders variants out of the kernel.Pierre-Marie Pédrot
They are not used there, and removing the redundance of the the case representation requires access to the environment, so we push their use further up.
2020-12-02Merge PR #13543: Fix a bug in funind.coqbot-app[bot]
Reviewed-by: Matafou
2020-12-02gitlab CI: remove redundant "dependencies" infoGaëtan Gilbert
When we started using "needs" for the acyclic graph scheduling we needed to duplicate dependencies and needs (I forgot if it was documented or just buggy). Nowadays gitlab doc https://docs.gitlab.com/ee/ci/yaml/#needs says >In GitLab 12.6 and later, you can’t combine the dependencies keyword with needs to control artifact downloads in jobs. dependencies is still valid in jobs that do not use needs. Some jobs in stage-1 had "dependencies: []" without a corresponding "needs", not sure why as the only job in a previous stage is docker-boot which has no artifacts to skip. We don't want "needs: []" as that would fail to wait for the docker image, so we just have nothing instead.
2020-12-02Merge PR #13472: [ci] Add job for gappacoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: ejgallego
2020-12-02Put all Int63 primitives in a separate filePierre Roux
Following a request from Pierre-Marie Pédrot in #13258
2020-12-02Make sure the msb is clear.Guillaume Melquiond
This is presumably not usable from the surface language. But an ML module could easily create a proof of false by passing a negative number to Const.mkInt.
2020-12-02Greatly simplify the conversion functions between Z.t and Uint63.t.Guillaume Melquiond
2020-12-01Fix a bug in funind.Pierre-Marie Pédrot
It was generating a completely nonsense case branch, but for some reason the proof still went trough.
2020-12-01Merge PR #13490: [ssr] Backport ssrbool from MathComp 1.12.0coqbot-app[bot]
Reviewed-by: gares
2020-12-01Make the code clearer and faster by calling mask63 explicitly at the end.Guillaume Melquiond
Before this commit, function mask63 was called implicitly at each step.
2020-12-01Avoid compiler warnings.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 03:12:20 +0000