aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-03-02Merge PR #13891: Simplify installation instructions in README.coqbot-app[bot]
Reviewed-by: jfehrle
2021-03-02Simplify wording.Théo Zimmermann
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2021-03-02Simplify installation instructions in README.Théo Zimmermann
Now that they are well described on the website.
2021-03-02Dead code elimination: not reducible error message is never raised.Théo Zimmermann
2021-02-28Merge PR #13853: Delay the dynamic linking of native-code libraries until ↵Pierre-Marie Pédrot
native_compute is called. Ack-by: ejgallego Reviewed-by: ppedrot
2021-02-28Merge PR #13886: Correct broken link.coqbot-app[bot]
Reviewed-by: Zimmi48
2021-02-28Fix link of default_bindings.slb Prime
2021-02-27Merge PR #13876: [coqc] Don't allow to pass more than one file to coqccoqbot-app[bot]
Reviewed-by: silene Reviewed-by: gares
2021-02-27Add overlayPierre Roux
2021-02-27Add changelogPierre Roux
2021-02-27Remove decimal-only number notationsPierre Roux
This was deprecated in 8.12
2021-02-27Merge PR #13559: Signed primitive integerscoqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: silene Reviewed-by: jfehrle Ack-by: gares Ack-by: Zimmi48 Ack-by: proux01
2021-02-26[coqc] Don't allow to pass more than one file to coqcEmilio Jesus Gallego Arias
This has been in the TODO queue for a long time, and indeed I have recently seen some trouble with users passing two .v files to Coq, which it isn't a) tested, b) supported. Moreover, it doesn't even work correctly in 8.13 due to some other changes in the toplevel related to auxiliary files. (*) https://stackoverflow.com/questions/66261987/compiling-multiple-coq-files-does-not-work
2021-02-26Merge PR #13884: CI Windows: adjust branch name to Coq Platform branch renamingcoqbot-app[bot]
Reviewed-by: gares
2021-02-26Merge PR #13883: Expose Top_printers.econstr_displaycoqbot-app[bot]
Reviewed-by: ejgallego
2021-02-26CI Windows: adjust branch name to Coq Platform branch renamingMichael Soegtrop
2021-02-26Expose Top_printers.econstr_displayGaëtan Gilbert
2021-02-26Signed primitive integersAna
Signed primitive integers defined on top of the existing unsigned ones with two's complement. The module Sint63 includes the theory of signed primitive integers that differs from the unsigned case. Additions to the kernel: les (signed <=), lts (signed <), compares (signed compare), divs (signed division), rems (signed remainder), asr (arithmetic shift right) (The s suffix is not used when importing the Sint63 module.) The printing and parsing of primitive ints was updated and the int63_syntax_plugin was removed (we use Number Notation instead). A primitive int is parsed / printed as unsigned or signed depending on the scope. In the default (Set Printing All) case, it is printed in hexadecimal.
2021-02-26Merge PR #13869: Use make_case_or_project in auto_ind_declPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-02-26Merge PR #13676: Protect caml_process_pending_actions_exn with ↵Pierre-Marie Pédrot
caml_something_to_do. Reviewed-by: gasche Ack-by: ppedrot Reviewed-by: xavierleroy
2021-02-26Merge PR #13868: Make genOpcodeFiles.ml handle opcode arity.Pierre-Marie Pédrot
Reviewed-by: SkySkimmer Reviewed-by: gares Reviewed-by: ppedrot
2021-02-26Delay the dynamic linking of native-code libraries until native_compute is ↵Guillaume Melquiond
called (fix #13849). The libraries are eventually linked in native_norm and native_conv_gen, just before mk_norm_code and mk_conv_code are called. This commit also renames call_linker as execute_library to better reflect its role. It also makes link_library independent from it, since their error handling are completely opposite.
2021-02-25Merge PR #13393: [proof using] Remove duplicate code, refactor.coqbot-app[bot]
Reviewed-by: gares Ack-by: SkySkimmer
2021-02-25[proof using] Remove duplicate code, refactor.Emilio Jesus Gallego Arias
PR #13183 introduced quite a bit of duplicate code, we refactor it and expose less internals on the way. That should make the API more robust.
2021-02-25Merge PR #13202: Infrastructure for fine-grained debug flagscoqbot-app[bot]
Reviewed-by: gares Ack-by: herbelin Ack-by: Zimmi48 Ack-by: jfehrle Ack-by: SkySkimmer Ack-by: ejgallego
2021-02-25Merge PR #13863: Get rid of the compilation date from the binaries to make ↵coqbot-app[bot]
them more stable. Reviewed-by: SkySkimmer Reviewed-by: gares
2021-02-25Merge PR #13080: Ascii: add leb and ltbcoqbot-app[bot]
Reviewed-by: anton-trunov
2021-02-25Merge PR #13738: Make sure Ltac2 get cleaned too.coqbot-app[bot]
Reviewed-by: gares
2021-02-24Overlay for Set DebugGaëtan Gilbert
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-02-24Use Reductionops.clos_whd_flags in vm_compute and native_compute.Guillaume Melquiond
2021-02-23Print anomaly labels regardless of -debug, and never print user_err labelsGaëtan Gilbert
2021-02-23Normalize evars during bytecode compilation (fix #13841).Guillaume Melquiond
Otherwise, the interpreter sees already unified evars as accumulators rather than actual constants, thus preventing the computations from progressing. This was caused by 6b61b63bb8626827708024cbea1312a703a54124, which removed evar normalization. The effect went unnoticed because the computed term is still convertible to the reduced term, except that it is the lazy machinery that ends up reducing it, rather than the bytecode one. So, performances became abysmal, seemingly at random.
2021-02-23Merge PR #13880: Fix the release process checklist with respect to the ↵coqbot-app[bot]
refman update. Reviewed-by: ejgallego
2021-02-22Fix the release process checklist with respect to the refman update.Théo Zimmermann
2021-02-22Merge PR #13878: [RM] Changelog for 8.13.1coqbot-app[bot]
Reviewed-by: Zimmi48
2021-02-22Merge PR #13836: Make detyping more resistent in the debuggerPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-02-22Merge PR #13828: Fix doc comment in pp.mlicoqbot-app[bot]
Reviewed-by: ejgallego
2021-02-22mention --version to CoqIDEEnrico Tassi
2021-02-22Merge PR #13872: Make lemmas from Reals opaque whenever possible.coqbot-app[bot]
Reviewed-by: thery
2021-02-22Merge PR #13870: Add option --version to Coqide (fix #13752).coqbot-app[bot]
Reviewed-by: gares
2021-02-22changelog for 8.13.1Enrico Tassi
2021-02-20Merge PR #13874: add changelog for #13867 (Fix missing arities of VM opcodes)coqbot-app[bot]
Reviewed-by: jfehrle
2021-02-20Update doc/changelog/01-kernel/13867-changelog-for-13867.rstEnrico Tassi
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2021-02-20add changelog for 13867Enrico Tassi
2021-02-20Inline proofs of exist_exp0 and exist_cos0.Guillaume Melquiond
2021-02-19Remove some trivial definition.Guillaume Melquiond
2021-02-19Abstract the non-computational part away.Guillaume Melquiond
2021-02-19Terminate intermediate lemmas with Qed.Guillaume Melquiond
2021-02-19Make intermediate lemmas more explicit, so that they can be terminated by Qed.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 03:26:31 +0000