aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2021-03-16Adding a changelog and registering the new file in the documentation.Pierre-Marie Pédrot
2021-03-12Fixed grammar productions for PDF documentationsIsaac Oscar Gariano
This undoes changes by 48bb58156acec84991a9e570e93a4e31c0349e79 that broke the rendering of grammar productions in PDfs.
2021-03-10Merge PR #13840: [notation] option to fine tune printing of literalscoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: jfehrle
2021-03-09Add changelogKazuhiko Sakaguchi
2021-03-08Merge PR #13707: Convert 2nd part of rewriting chapter to prodncoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2021-03-06Merge PR #13586: Support nested timeoutsPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-03-06Merge PR #13882: Fix #12011 ssreflect "rewrite in" with setoidsPierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot
2021-03-06Merge PR #13236: Add a type of format strings to Ltac2.Michael Soegtrop
Reviewed-by: JasonGross Reviewed-by: MSoegtropIMC
2021-03-05Merge PR #13842: Remove decimal-only number notations (deprecated in 8.12)Pierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2021-03-04Correctly sort the glossaryJim Fehrle
2021-03-04doc: don't count a contributor twice in the changelogLi-yao Xia
2021-03-04Properly support nested timeoutsLasse Blaauwbroek
2021-03-04[doc] changelog entryEnrico Tassi
2021-03-04[doc] Set/Unset Printing Raw LiteralsEnrico Tassi
2021-03-04Fix #12011 ssreflect "rewrite in" with setoidsGaëtan Gilbert
ssreflect asks setoid rewrite to rewrite in goal "forall_special_name_ : T, _other_name_" Since this is a non dependent product, setoid rewrite converts that to "impl T _other_name_" and must be taught to restore the special name when unfolding impl.
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-27Add changelogPierre Roux
2021-02-27Remove decimal-only number notationsPierre Roux
This was deprecated in 8.12
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 05:54:29 +0000