diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/08-tools/12211-time-ocaml.rst | 5 | ||||
| -rw-r--r-- | doc/changelog/10-standard-library/12008-ollibs-bool.rst | 5 | ||||
| -rw-r--r-- | doc/changelog/10-standard-library/12018-master+implb-characterization.rst | 19 | ||||
| -rw-r--r-- | doc/sphinx/using/libraries/writing.rst | 2 | ||||
| -rw-r--r-- | doc/stdlib/Library.tex | 1 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 1 |
6 files changed, 32 insertions, 1 deletions
diff --git a/doc/changelog/08-tools/12211-time-ocaml.rst b/doc/changelog/08-tools/12211-time-ocaml.rst new file mode 100644 index 0000000000..7ff68cc495 --- /dev/null +++ b/doc/changelog/08-tools/12211-time-ocaml.rst @@ -0,0 +1,5 @@ +- **Changed:** + When passing ``TIMED=1`` to ``make`` with either Coq's own makefile + or a ``coq_makefile``\-made makefile, timing information is now + printed for OCaml files as well (`#12211 + <https://github.com/coq/coq/pull/12211>`_, by Jason Gross). diff --git a/doc/changelog/10-standard-library/12008-ollibs-bool.rst b/doc/changelog/10-standard-library/12008-ollibs-bool.rst new file mode 100644 index 0000000000..7c10d261a7 --- /dev/null +++ b/doc/changelog/10-standard-library/12008-ollibs-bool.rst @@ -0,0 +1,5 @@ +- **Added:** + Order relations ``ltb`` and ``compareb`` added in ``Bool.Bool``. + Order properties for ``bool`` added in ``Bool.BoolOrder`` as well as two modules ``Bool_as_OT`` and ``Bool_as_DT`` in ``Structures.OrdersEx`` + (`#12008 <https://github.com/coq/coq/pull/12008>`_, + by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/12018-master+implb-characterization.rst b/doc/changelog/10-standard-library/12018-master+implb-characterization.rst new file mode 100644 index 0000000000..4b0abdfa3b --- /dev/null +++ b/doc/changelog/10-standard-library/12018-master+implb-characterization.rst @@ -0,0 +1,19 @@ +- **Added:** + Added lemmas + :g:`orb_negb_l`, + :g:`andb_negb_l`, + :g:`implb_true_iff`, + :g:`implb_false_iff`, + :g:`implb_true_r`, + :g:`implb_false_r`, + :g:`implb_true_l`, + :g:`implb_false_l`, + :g:`implb_same`, + :g:`implb_contrapositive`, + :g:`implb_negb`, + :g:`implb_curry`, + :g:`implb_andb_distrib_r`, + :g:`implb_orb_distrib_r`, + :g:`implb_orb_distrib_l` in library :g:`Bool` + (`#12018 <https://github.com/coq/coq/pull/12018>`_,` + by Hugo Herbelin).` diff --git a/doc/sphinx/using/libraries/writing.rst b/doc/sphinx/using/libraries/writing.rst index 801d492acb..325ea2af60 100644 --- a/doc/sphinx/using/libraries/writing.rst +++ b/doc/sphinx/using/libraries/writing.rst @@ -62,7 +62,7 @@ deprecated compatibility alias using :cmd:`Notation (abbreviation)` Definition bar x := S x. #[deprecated(since="1.2", note="Use bar instead.")] - Notation foo := bar. + Notation foo := bar (only parsing). Then, the following code still works, but emits a warning: diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex index 44a0b1d361..1a9d4d738f 100644 --- a/doc/stdlib/Library.tex +++ b/doc/stdlib/Library.tex @@ -5,6 +5,7 @@ \usepackage[T1]{fontenc} \usepackage{fullpage} \usepackage{amsfonts} +\usepackage{amssymb} \usepackage{url} \usepackage[color]{../../coqdoc} diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index b2c9c936c9..4a62888552 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -99,6 +99,7 @@ through the <tt>Require Import</tt> command.</p> <dd> theories/Bool/Bool.v theories/Bool/BoolEq.v + theories/Bool/BoolOrder.v theories/Bool/DecBool.v theories/Bool/IfProp.v theories/Bool/Sumbool.v |