diff options
Diffstat (limited to 'doc')
4 files changed, 19 insertions, 13 deletions
diff --git a/doc/changelog/08-tools/13063-fix-no-output-sync-make-file.rst b/doc/changelog/08-tools/13063-fix-no-output-sync-make-file.rst new file mode 100644 index 0000000000..75b1e26248 --- /dev/null +++ b/doc/changelog/08-tools/13063-fix-no-output-sync-make-file.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Targets such as ``print-pretty-timed`` in ``coq_makefile``-made + ``Makefile``\s no longer error in rare cases where ``--output-sync`` is not + passed to make and the timing output gets interleaved in just the wrong way + (`#13063 <https://github.com/coq/coq/pull/13063>`_, fixes `#13062 + <https://github.com/coq/coq/issues/13062>`_, by Jason Gross). diff --git a/doc/changelog/11-infrastructure-and-dependencies/13007-zarith+goodbye_num.rst b/doc/changelog/11-infrastructure-and-dependencies/13007-zarith+goodbye_num.rst new file mode 100644 index 0000000000..c142eec561 --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/13007-zarith+goodbye_num.rst @@ -0,0 +1,4 @@ +- **Removed:** + The `num` library is not linked to Coq anymore + (`#13007 <https://github.com/coq/coq/pull/13007>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 2f505e7448..e276a0edcb 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -732,12 +732,13 @@ Applying theorems does not succeed because it would require the conversion of ``id ?foo`` and :g:`O`. + .. _simple_apply_ex: .. example:: .. coqtop:: all Definition id (x : nat) := x. - Parameter H : forall y, id y = y. + Parameter H : forall x y, id x = y. Goal O = O. Fail simple apply H. @@ -907,13 +908,8 @@ Applying theorems .. tacv:: simple apply @term in @ident This behaves like :tacn:`apply … in` but it reasons modulo conversion - only on subterms that contain no variables to instantiate. For instance, - if :g:`id := fun x:nat => x` and :g:`H: forall y, id y = y -> True` and - :g:`H0 : O = O` then :g:`simple apply H in H0` does not succeed because it - would require the conversion of :g:`id ?x` and :g:`O` where :g:`?x` is - an existential variable to instantiate. - Tactic :n:`simple apply @term in @ident` does not - either traverse tuples as :n:`apply @term in @ident` does. + only on subterms that contain no variables to instantiate and does not + traverse tuples. See :ref:`the corresponding example <simple_apply_ex>`. .. tacv:: {? simple} apply {+, @term {? with @bindings_list}} in @ident {? as @simple_intropattern} {? simple} eapply {+, @term {? with @bindings_list}} in @ident {? as @simple_intropattern} diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 3fef3bcbd1..56464851ba 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -1424,11 +1424,11 @@ def setup(app): app.connect('doctree-resolved', CoqtopBlocksTransform.merge_consecutive_coqtop_blocks) # Add extra styles - app.add_stylesheet("ansi.css") - app.add_stylesheet("coqdoc.css") - app.add_javascript("notations.js") - app.add_stylesheet("notations.css") - app.add_stylesheet("pre-text.css") + app.add_css_file("ansi.css") + app.add_css_file("coqdoc.css") + app.add_js_file("notations.js") + app.add_css_file("notations.css") + app.add_css_file("pre-text.css") # Tell Sphinx about extra settings app.add_config_value("report_undocumented_coq_objects", None, 'env') |