aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2021-03-04doc: don't count a contributor twice in the changelogLi-yao Xia
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-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-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-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-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-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 #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 #13080: Ascii: add leb and ltbcoqbot-app[bot]
Reviewed-by: anton-trunov
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-02-22mention --version to CoqIDEEnrico Tassi
2021-02-22changelog for 8.13.1Enrico Tassi
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-11Merge PR #13831: Properly document the local and global locality attributes.coqbot-app[bot]
Reviewed-by: gares Reviewed-by: jfehrle Ack-by: SkySkimmer
2021-02-09Merge PR #13822: Remove deprecated command line argumentscoqbot-app[bot]
Reviewed-by: gares
2021-02-09Merge PR #13810: ide: shift+enter to find backwardscoqbot-app[bot]
Reviewed-by: herbelin
2021-02-08Properly document the local and global locality attributes.Théo Zimmermann
2021-02-05Fix hierarchy of sections in module chapter.Théo Zimmermann
2021-02-04Changelog for #13822Gaëtan Gilbert
2021-02-01Add changelog entryslrnsc
2021-01-28Merge PR #13799: Replace : term with : type in open binders.coqbot-app[bot]
Reviewed-by: jfehrle
2021-01-28Merge PR #13789: Document limitation of rewrite regarding occurrence selection.coqbot-app[bot]
Reviewed-by: jfehrle Reviewed-by: silene
2021-01-28Update doc/sphinx/proofs/writing-proofs/rewriting.rstJim Fehrle
2021-01-28Merge PR #13781: [micromega] Deprecate hopefully useless options and flagscoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: jfehrle
2021-01-28Replace : term with : type in open binders.Théo Zimmermann
And update the doc_grammar files.
2021-01-28Apply suggestions from code reviewThéo Zimmermann
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2021-01-28Merge PR #13763: Remove the SearchHead command (deprecated in 8.12)coqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2021-01-28Document how rewrite works regarding occurrence selection.Théo Zimmermann
2021-01-26Merge PR #13758: Remove the Hide Obligations flag (deprecated in 8.12)coqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2021-01-25Remove the SearchHead commandJim Fehrle
2021-01-25Remove the Hide Obligations flagJim Fehrle
2021-01-25Update doc/changelog/04-tactics/13781-deprecate_micromega_options.rstFrédéric Besson
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2021-01-25Update doc/sphinx/addendum/micromega.rstFrédéric Besson
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2021-01-24Merge PR #13762: Remove double induction tacticPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2021-01-22changelogBESSON Frederic
2021-01-22Merge PR #13754: Improve doc of occurrences and rewrite.coqbot-app[bot]
Reviewed-by: Zimmi48
2021-01-22[micromega] Deprecate hopefully useless options and flagsBESSON Frederic
The goal is to eventually only use the Simplex solver and remove all the code needed for fourier elimination.
2021-01-22Improve doc of occurrences and rewrite.Jim Fehrle
2021-01-22Merge PR #13761: Remove convert_concl_no_check (deprecated in 8.11)Pierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2021-01-21Improve wording for #13384Jim Fehrle
2021-01-21Merge PR #13764: Remove Add InjTyp and 10 other micromega commands ↵BESSON Frederic
(deprecated in 8.13) Reviewed-by: Zimmi48 Reviewed-by: fajb
2021-01-20Remove double induction tacticJim Fehrle
2021-01-20Fix: "tactic" is not a tactic, so can't begin a .. tacn::Jim Fehrle
2021-01-19Remove Add InjTyp and 10 other micromega commandsJim Fehrle
2021-01-19Remove convert_concl_no_checkJim Fehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:15:22 +0000