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/12018-master+implb-characterization.rst | 19 | ||||
| -rw-r--r-- | doc/sphinx/using/libraries/writing.rst | 2 |
3 files changed, 25 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/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: |