aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-03-04Cleanup internal hint locality handlingGaëtan Gilbert
By separating the libobject for create db and other hints we can unify handling of local/superglobal.
2021-03-03Merge PR #12567: [build] Split stdlib to it's own package.coqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross Ack-by: gares Ack-by: LasseBlaauwbroek Ack-by: silene Ack-by: vbgl
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
We introduce a new package structure for Coq: - `coq-core`: Coq's OCaml tools code and plugins - `coq-stdlib`: Coq's stdlib [.vo files] - `coq`: meta-package that pulls `coq-{core,stdlib}` This has several advantages, in particular it allows to install Coq without the stdlib which is useful in several scenarios, it also open the door towards a versioning of the stdlib at the package level. The main user-visible change is that Coq's ML development files now live in `$lib/coq-core`, for compatibility in the regular build we install a symlink and support both setups for a while. Note that plugin developers and even `coq_makefile` should actually rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust. There is a transient state where we actually look for both `$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support the non-ocamlfind plus custom variables. This will be much improved once #13617 is merged (which requires this PR first), then, we will introduce a `coq.boot` library so finally `coqdep`, `coqchk`, etc... can share the same path setup code. IMHO the plan should work fine.
2021-03-02Merge PR #13889: Dead code elimination: not reducible error message is never ↵coqbot-app[bot]
raised. Reviewed-by: jfehrle
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-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-23Print anomaly labels regardless of -debug, and never print user_err labelsGaëtan Gilbert
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
2021-02-19Make most of DRealAbstr opaque.Guillaume Melquiond
The function returned by DRealAbstr starts by a call to the axiom sig_forall_dec, so it is not computable anyway.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 15:39:34 +0000