diff options
78 files changed, 813 insertions, 284 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 8880ec1d21..1a1d31bdd7 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -212,7 +212,10 @@ before_script: dependencies: - not-a-real-job script: - - cd _install_ci + # exit 0: workaround for https://gitlab.com/gitlab-org/gitlab/issues/202505 + # the validate:quick job is sometimes started before build:quick, without artifacts + # we ignore these spurious errors so if the job fails it's a real error + - cd _install_ci || exit 0 - find lib/coq/ -name '*.vo' -fprint0 vofiles - xargs -0 --arg-file=vofiles bin/coqchk -o -m -coqlib lib/coq/ > ../coqchk.log 2>&1 || touch coqchk.failed - tail -n 1000 ../coqchk.log # the log is too big for gitlab so pipe to a file and display the tail @@ -713,7 +716,11 @@ library:ci-fiat-crypto: - plugin:ci-rewriter library:ci-flocq: - extends: .ci-template + extends: .ci-template-flambda + artifacts: + name: "$CI_JOB_NAME" + paths: + - _build_ci library:ci-corn: extends: .ci-template-flambda @@ -769,6 +776,13 @@ library:ci-verdi-raft: library:ci-vst: extends: .ci-template-flambda + stage: stage-3 + needs: + - build:edge+flambda + - library:ci-flocq + dependencies: + - build:edge+flambda + - library:ci-flocq # Plugins are by definition the projects that depend on Coq's ML API @@ -9,7 +9,9 @@ ## If you're mentioned here and want to update your information, ## either amend this file and commit it, or contact the coqdev list +Guillaume Allais <guillaume.allais@ens-lyon.org> gallais <guillaume.allais@ens-lyon.org> Abhishek Anand <abhishek.anand.iitg@gmail.com> Abhishek Anand (@brixpro-home) <abhishek.anand.iitg@gmail.com> +Abhishek Anand <abhishek.anand.iitg@gmail.com> Abhishek Anand (optiplex7010@home) <abhishek.anand.iitg@gmail.com> Léo Andrès <leo@ndrs.fr> zapashcanon <leo@ndrs.fr> Jim Apple <github.public@jbapple.com> jbapple <github.public@jbapple.com> Bruno Barras <bruno.barras@inria.fr> barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -21,13 +23,17 @@ Yves Bertot <yves.bertot@inria.fr> Yves Bertot <Yves.Bertot@inri Yves Bertot <yves.bertot@inria.fr> Yves Bertot <bertot@nardis.inria.fr> Frédéric Besson <frederic.besson@inria.fr> fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> Siddharth Bhat <siddu.druid@gmail.com> Siddharth <siddu.druid@gmail.com> +Lasse Blaauwbroek <lasse@blaauwbroek.eu> Lasse Blaauwbroek <lasse@lasse-work.localdomain> Simon Boulier <simon.boulier@ens-rennes.fr> SimonBoulier <simon.boulier@ens-rennes.fr> +Simon Boulier <simon.boulier@ens-rennes.fr> SimonBoulier <SimonBoulier@users.noreply.github.com> Pierre Boutillier <pierre.boutillier@ens-lyon.org> pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> Pierre Boutillier <pierre.boutillier@ens-lyon.org> Pierre <pierre.boutillier@ens-lyon.org> Pierre Boutillier <pierre.boutillier@ens-lyon.org> Pierre Boutillier <pierre.boutillier@pps.univ-paris-diderot.fr> +Michele Caci <michele.caci@gmail.com> mcaci <michele.caci@gmail.com> Arthur Charguéraud <arthur@chargueraud.org> charguer <arthur@chargueraud.org> Xavier Clerc <xavier.clerc@inria.fr> xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7> Xavier Clerc <xavier.clerc@inria.fr> xclerc <xavier.clerc@inria.fr> +Cyril Cohen <cohen@crans.org> Cyril Cohen <CohenCyril@users.noreply.github.com> Pierre Corbineau <Pierre.Corbineau@NOSPAM@imag.fr> corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> Judicaël Courant <courant@gforge> courant <courant@85f007b7-540e-0410-9357-904b9bb8a0f7> Pierre Courtieu <Pierre.Courtieu@cnam.fr> courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -39,8 +45,10 @@ Maxime Dénès <mail@maximedenes.fr> Maxime Dénès <maxime.dene Olivier Desmettre <desmettr@gforge> desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> Damien Doligez <doligez@gforge> doligez <doligez@85f007b7-540e-0410-9357-904b9bb8a0f7> İsmail Dönmez <ismail-s@users.noreply.github.com> Ismail <ismail-s@users.noreply.github.com> +formalize.eth <formalize@protonmail.com> ilya <ilya@localhost.localdomain> Andres Erbsen <andreser@mit.edu> Andres Erbsen <andres@kevix.co> Jim Fehrle <jfehrle@sbcglobal.net> Jim <jfehrle@sbcglobal.net> +Jim Fehrle <jfehrle@sbcglobal.net> Jim Fehrle <jim.fehrle@gmail.com> Jean-Christophe Filliâtre <Jean-Christophe.Filliatre@lri.fr> filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> Jean-Christophe Filliâtre <Jean-Christophe.Filliatre@lri.fr> Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr> Julien Forest <julien.forest@ensiie.fr> jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -63,6 +71,7 @@ Jason Gross <jgross@mit.edu> Jason Gross <jasongross9@gmai Vincent Gross <vgross@gforge> vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7> Huang Guan-Shieng <huang@gforge> huang <huang@85f007b7-540e-0410-9357-904b9bb8a0f7> Hugo Herbelin <Hugo.Herbelin@inria.fr> herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> +Hugo Herbelin <Hugo.Herbelin@inria.fr> Hugo Herbelin <herbelin@users.noreply.github.com> Jasper Hugunin <jasperh@cs.washington.edu> Jasper Hugunin <jasper@hashplex.com> Tom Hutchinson <thutchin@gforge> thutchin <thutchin@85f007b7-540e-0410-9357-904b9bb8a0f7> Cezary Kaliszyk <cek@gforge> cek <cek@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -74,13 +83,18 @@ Matej Košík <matej.kosik@inria.fr> Matej Kosik <matej.kosik@in Matej Košík <matej.kosik@inria.fr> Matej Košík <mail@matej-kosik.net> Ambroise Lafont <chaster_killer@hotmail.fr> amblaf <you@example.com> Ambroise Lafont <chaster_killer@hotmail.fr> Ambroise <chaster_killer@hotmail.fr> -Vincent Laporte <Vincent.Laporte@fondation-inria.fr> Vincent Laporte <Vincent.Laporte@gmail.com> +Vincent Laporte <Vincent.Laporte@inria.fr> Vincent Laporte <Vincent.Laporte@gmail.com> +Vincent Laporte <Vincent.Laporte@inria.fr> Vincent Laporte <Vincent.Laporte@fondation-inria.fr> Marc Lasson <marc.lasson@gmail.com> mlasson <marc.lasson@gmail.com> William Lawvere <mundungus.corleone@gmail.com> william-lawvere <mundungus.corleone@gmail.com> +Larry Darryl Lee Jr. <llee454@gmail.com> llee454@gmail.com <llee454@gmail.com> +Xavier Leroy <xavier.leroy@college-de-france.fr> Xavier Leroy <xavier.leroy@inria.fr> Pierre Letouzey <pierre.letouzey@inria.fr> letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> Pierre Letouzey <pierre.letouzey@inria.fr> letouzey <pierre.letouzey@inria.fr> Xia Li-yao <lysxia@gmail.com> Lysxia <lysxia@gmail.com> +Yishuai Li <yishuai@cis.upenn.edu> Yishuai Li <yishuai@upenn.edu> Assia Mahboubi <assia.mahboubi@inria.fr> amahboub <amahboub@85f007b7-540e-0410-9357-904b9bb8a0f7> +Kenji Maillard <kenji.maillard@inria.fr> Kenji Maillard <kenji@maillard.blue> Evgeny Makarov <emakarov@gforge> emakarov <emakarov@85f007b7-540e-0410-9357-904b9bb8a0f7> Gregory Malecha <gmalecha@eecs.harvard.edu> Gregory Malecha <gmalecha@cs.harvard.edu> Gregory Malecha <gmalecha@eecs.harvard.edu> Gregory Malecha <gmalecha@gmail.com> @@ -103,9 +117,11 @@ Christine Paulin <cpaulin@gforge> mohring <mohring@85f007b7-540 Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> Frederic Peschanski <frederic.peschanski@lip6.fr> fredokun <frederic.peschanski@lip6.fr> Clément Pit-Claudel <clement.pitclaudel@live.com> Clément Pit--Claudel <clement.pitclaudel@live.com> +Clément Pit-Claudel <clement.pitclaudel@live.com> Clément Pit-Claudel <cpitclaudel@users.noreply.github.com> Loïc Pottier <pottier@gforge> pottier <pottier@85f007b7-540e-0410-9357-904b9bb8a0f7> Matthias Puech <puech@gforge> puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> Lars Rasmusson <lars.rasmusson@sics.se> larsr <Lars.Rasmusson@sics.se> +Lars Rasmusson <lars.rasmusson@sics.se> larsr <Lars.Rasmusson@gmail.com> Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr> ddr <ddr@85f007b7-540e-0410-9357-904b9bb8a0f7> Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr> Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr> Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr> Daniel De Rauglaudre <ddr@gforge> @@ -116,6 +132,7 @@ Pierre Roux <pierre@roux01.fr> Pierre Roux <pierre.roux@oner Matthew Ryan <mr_1993@hotmail.co.uk> mrmr1993 <mr_1993@hotmail.co.uk> Claudio Sacerdoti Coen <sacerdot@gforge> sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> Kazuhiko Sakaguchi <pi8027@gmail.com> Kazuhiko Sakaguchi <sakaguchi@coins.tsukuba.ac.jp> +Kazuhiko Sakaguchi <pi8027@gmail.com> Kazuhiko Sakaguchi <sakaguchi@peano-system.jp> Vincent Siles <vsiles@gforge> vsiles <vsiles@85f007b7-540e-0410-9357-904b9bb8a0f7> Michael Soegtrop <michael.soegtrop@intel.com> Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Elie Soubiran <soubiran@gforge> soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -138,8 +155,9 @@ Benjamin Werner <werner@gforge> werner <werner@85f007b7-540e- Wang Zhuyang <hawnzug@gmail.com> hawnzug <hawnzug@gmail.com> Beta Ziliani <beta@mpi-sws.org> Beta Ziliani <bziliani@famaf.unc.edu.ar> Beta Ziliani <beta@mpi-sws.org> beta <beta@mpi-sws.org> -Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> Theo Zimmermann <theo.zimmermann@ens.fr> -Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> Théo Zimmermann <theo.zimmi@gmail.com> +Théo Zimmermann <theo.zimmermann@inria.fr> Theo Zimmermann <theo.zimmermann@ens.fr> +Théo Zimmermann <theo.zimmermann@inria.fr> Théo Zimmermann <theo.zimmi@gmail.com> +Théo Zimmermann <theo.zimmermann@inria.fr> Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> # Anonymous accounts diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index c38f9ec7d6..3582d18cf6 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -570,9 +570,10 @@ We have a linter that checks a few different things: [Style guide](#style-guide) for additional style recommendations. - **Code is properly formatted**: for some parts of the codebase, formatting will be enforced using the - [`ocamlformat`](https://github.com/ocaml-ppx/ocamlformat) tool. You - can integrate the formatter in your editor of choice (see docs) or - use `dune build @fmt --auto-promote` to fix this kind of errors. + [`ocamlformat`](https://github.com/ocaml-ppx/ocamlformat) tool. + Formatting issues will also be fixed automatically by the pre-commit + hook mentioned above (you may also use `dune build @fmt + --auto-promote` to fix this kind of errors). You may run the linter yourself with `dev/lint-repository.sh`. diff --git a/Makefile.build b/Makefile.build index 5b26f11b12..8a8500ba1a 100644 --- a/Makefile.build +++ b/Makefile.build @@ -201,12 +201,12 @@ DEPENDENCIES := \ # Default timing command # Use /usr/bin/env time on linux, gtime on Mac OS -TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)" +TIMEFMT?="$@ (real: %e, user: %U, sys: %S, mem: %M ko)" ifneq (,$(TIMED)) -ifeq (0,$(shell /usr/bin/env time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) +ifeq (0,$(shell /usr/bin/env time -f "" true >/dev/null 2>/dev/null; echo $$?)) STDTIME?=/usr/bin/env time -f $(TIMEFMT) else -ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) +ifeq (0,$(shell gtime -f "" true >/dev/null 2>/dev/null; echo $$?)) STDTIME?=gtime -f $(TIMEFMT) else STDTIME?=time diff --git a/Makefile.ci b/Makefile.ci index d4383fd409..1a5e8166a2 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -76,6 +76,8 @@ ci-quickchick: ci-ext-lib ci-simple-io ci-metacoq: ci-equations +ci-vst: ci-flocq + # Generic rule, we use make to ease CI integration $(CI_TARGETS): ci-%: +./dev/ci/ci-wrapper.sh $* diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh index e9f8324f28..7a9531216e 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")" git_download Flocq -( cd "${CI_BUILD_DIR}/Flocq" && autoconf && ./configure && ./remake "-j${NJOBS}" ) +( cd "${CI_BUILD_DIR}/Flocq" && autoconf && ./configure && ./remake "-j${NJOBS}" && ./remake install ) diff --git a/doc/changelog/04-tactics/11883-fix-autounfold.rst b/doc/changelog/04-tactics/11883-fix-autounfold.rst new file mode 100644 index 0000000000..83ff177380 --- /dev/null +++ b/doc/changelog/04-tactics/11883-fix-autounfold.rst @@ -0,0 +1,13 @@ +- **Fixed:** + The behavior of :tacn:`autounfold` no longer depends on the names of terms and modules + (`#11883 <https://github.com/coq/coq/pull/11883>`_, + fixes `#7812 <https://github.com/coq/coq/issues/7812>`_, + by Attila Gáspár). +- **Changed:** + `at` clauses can no longer be used with :tacn:`autounfold`. Since they had no effect, it is safe to remove them + (`#11883 <https://github.com/coq/coq/pull/11883>`_, + by Attila Gáspár). +- **Changed:** + :tacn:`autounfold` no longer fails when the :cmd:`Opaque` command is used on constants in the hint databases + (`#11883 <https://github.com/coq/coq/pull/11883>`_, + by Attila Gáspár). diff --git a/doc/changelog/04-tactics/11976-deprecate-omega.rst b/doc/changelog/04-tactics/11976-deprecate-omega.rst new file mode 100644 index 0000000000..59c9612d17 --- /dev/null +++ b/doc/changelog/04-tactics/11976-deprecate-omega.rst @@ -0,0 +1,5 @@ +- **Deprecated:** + The :tacn:`omega` tactic is deprecated; + use :tacn:`lia` from the :ref:`Micromega <micromega>` plugin instead + (`#11976 <https://github.com/coq/coq/pull/11976>`_, + by Vincent Laporte). diff --git a/doc/changelog/04-tactics/12116-master+fix12045-missing-reduction-in-using-ind-scheme.rst b/doc/changelog/04-tactics/12116-master+fix12045-missing-reduction-in-using-ind-scheme.rst new file mode 100644 index 0000000000..7af2b4d97b --- /dev/null +++ b/doc/changelog/04-tactics/12116-master+fix12045-missing-reduction-in-using-ind-scheme.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Anomaly with induction schemes whose conclusion is not normalized + (`#12116 <https://github.com/coq/coq/pull/12116>`_, + by Hugo Herbelin; fixes + `#12045 <https://github.com/coq/coq/pull/12045>`_) diff --git a/doc/changelog/08-tools/12026-master+coqdoc-self-linked-defs-wish7093.rst b/doc/changelog/08-tools/12026-master+coqdoc-self-linked-defs-wish7093.rst new file mode 100644 index 0000000000..5c4ef82b8b --- /dev/null +++ b/doc/changelog/08-tools/12026-master+coqdoc-self-linked-defs-wish7093.rst @@ -0,0 +1,4 @@ +- **Added:** + Definitions in coqdoc link to themselves, giving access in html to their own url + (`#12026 <https://github.com/coq/coq/pull/12026>`_, + by Hugo Herbelin; granting `#7093 <https://github.com/coq/coq/pull/7093>`_). diff --git a/doc/changelog/08-tools/12033-master+coqdoc-fix7697-passing-binders-location.rst b/doc/changelog/08-tools/12033-master+coqdoc-fix7697-passing-binders-location.rst new file mode 100644 index 0000000000..af0d28305a --- /dev/null +++ b/doc/changelog/08-tools/12033-master+coqdoc-fix7697-passing-binders-location.rst @@ -0,0 +1,5 @@ +- **Added:** + Add hyperlinks on bound variables for coqdoc + (`#12033 <https://github.com/coq/coq/pull/12033>`_, + by Hugo Herbelin; it incidentally fixes + `#7697 <https://github.com/coq/coq/pull/7697>`_). diff --git a/doc/changelog/08-tools/12091-master+coqdoc-css-target.rst b/doc/changelog/08-tools/12091-master+coqdoc-css-target.rst new file mode 100644 index 0000000000..f6af5d40e8 --- /dev/null +++ b/doc/changelog/08-tools/12091-master+coqdoc-css-target.rst @@ -0,0 +1,4 @@ +- **Added:** + ``Coqdoc``: Highlighting of the exact position of the target of links + (`#12091 <https://github.com/coq/coq/pull/12091>`_, + by Hugo Herbelin). diff --git a/doc/changelog/08-tools/12126-adjust-timed-name.rst b/doc/changelog/08-tools/12126-adjust-timed-name.rst new file mode 100644 index 0000000000..c305b384d9 --- /dev/null +++ b/doc/changelog/08-tools/12126-adjust-timed-name.rst @@ -0,0 +1,8 @@ +- **Changed:** + The output of ``make TIMED=1`` (and therefore the timing targets + such as ``print-pretty-timed`` and ``print-pretty-timed-diff``) now + displays the full name of the output file being built, rather than + the stem of the rule (which was usually the filename without the + extension, but in general could be anything for user-defined rules + involving ``%``) (`#12126 + <https://github.com/coq/coq/pull/12126>`_, by Jason Gross). diff --git a/doc/changelog/09-coqide/12106-master+coqide-style-apply-all-windows.rst b/doc/changelog/09-coqide/12106-master+coqide-style-apply-all-windows.rst new file mode 100644 index 0000000000..a17e9956b9 --- /dev/null +++ b/doc/changelog/09-coqide/12106-master+coqide-style-apply-all-windows.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Highlighting style and language settings consistently apply to all three buffers of CoqIDE + (`#12106 <https://github.com/coq/coq/pull/12106>`_, + by Hugo Herbelin; fixes + `#11506 <https://github.com/coq/coq/pull/11506>`_). diff --git a/doc/changelog/10-standard-library/12014-ollibs-vector.rst b/doc/changelog/10-standard-library/12014-ollibs-vector.rst new file mode 100644 index 0000000000..87625dd23b --- /dev/null +++ b/doc/changelog/10-standard-library/12014-ollibs-vector.rst @@ -0,0 +1,10 @@ +- **Added:** + Properties of some operations on vectors: + + - ``nth_order``: ``nth_order_hd``, ``nth_order_tl``, ``nth_order_ext`` + - ``replace``: ``nth_order_replace_eq``, ``nth_order_replace_neq``, ``replace_id``, ``replace_replace_eq``, ``replace_replace_neq`` + - ``map``: ``map_id``, ``map_map``, ``map_ext_in``, ``map_ext`` + - ``Forall`` and ``Forall2``: ``Forall_impl``, ``Forall_forall``, ``Forall_nth_order``, ``Forall2_nth_order`` + + (`#12014 <https://github.com/coq/coq/pull/12014>`_, + by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/12044-issue-12015.rst b/doc/changelog/10-standard-library/12044-issue-12015.rst new file mode 100644 index 0000000000..166fc80fb0 --- /dev/null +++ b/doc/changelog/10-standard-library/12044-issue-12015.rst @@ -0,0 +1,10 @@ +- **Fixed:** + Rewrote ``Structures.OrderedTypeEx.String_as_OT.compare`` + to avoid huge proof terms + (Fixes `#12015 <https://github.com/coq/coq/issues/12015>`_, + `#12044 <https://github.com/coq/coq/pull/12044>`_, + by formalize.eth (formalize@protonmail.com)). +- **Added:** + Added ``Structures.OrderedTypeEx.Ascii_as_OT`` + (`#12044 <https://github.com/coq/coq/pull/12044>`_, + by formalize.eth (formalize@protonmail.com)). diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index f706633da9..77bf58aac6 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -1,4 +1,4 @@ -.. _ micromega: +.. _micromega: Micromega: tactics for solving arithmetic goals over ordered rings ================================================================== diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index daca43e65e..082ea4691b 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -7,20 +7,18 @@ Omega: a solver for quantifier-free problems in Presburger Arithmetic .. warning:: - The :tacn:`omega` tactic is about to be deprecated in favor of the - :tacn:`lia` tactic. The goal is to consolidate the arithmetic - solving capabilities of Coq into a single engine; moreover, - :tacn:`lia` is in general more powerful than :tacn:`omega` (it is a - complete Presburger arithmetic solver while :tacn:`omega` was known - to be incomplete). - - Work is in progress to make sure that there are no regressions - (including no performance regression) when switching from - :tacn:`omega` to :tacn:`lia` in existing projects. However, we - already recommend using :tacn:`lia` in new or refactored proof - scripts. We also ask that you report (in our `bug tracker - <https://github.com/coq/coq/issues>`_) any issue you encounter, - especially if the issue was not present in :tacn:`omega`. + The :tacn:`omega` tactic is deprecated in favor of the :tacn:`lia` + tactic. The goal is to consolidate the arithmetic solving + capabilities of Coq into a single engine; moreover, :tacn:`lia` is + in general more powerful than :tacn:`omega` (it is a complete + Presburger arithmetic solver while :tacn:`omega` was known to be + incomplete). + + It is recommended to switch from :tacn:`omega` to :tacn:`lia` in existing + projects. We also ask that you report (in our `bug tracker + <https://github.com/coq/coq/issues>`_) any issue you encounter, especially + if the issue was not present in :tacn:`omega`. If no new issues are + reported, :tacn:`omega` will be removed soon. Note that replacing :tacn:`omega` with :tacn:`lia` can break non-robust proof scripts which rely on incompleteness bugs of @@ -31,6 +29,10 @@ Description of ``omega`` .. tacn:: omega + .. deprecated:: 8.12 + + Use :tacn:`lia` instead. + :tacn:`omega` is a tactic for solving goals in Presburger arithmetic, i.e. for proving formulas made of equations and inequalities over the type ``nat`` of natural numbers or the type ``Z`` of binary-encoded integers. @@ -118,7 +120,7 @@ loaded by .. example:: - .. coqtop:: all + .. coqtop:: all warn Require Import Omega. diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index b1f392c337..a69521c278 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -1,3 +1,5 @@ +.. |GtkSourceView| replace:: :smallcaps:`GtkSourceView` + .. _coqintegrateddevelopmentenvironment: |Coq| Integrated Development Environment @@ -158,7 +160,18 @@ presented as a notebook. The first section is for selecting the text font used for scripts, goal and message windows. -The second and third sections are for controlling colors and style. +The second and third sections are for controlling colors and style of +the three main buffers. A predefined |Coq| highlighting style as well +as standard |GtkSourceView| styles are available. Other styles can be +added e.g. in ``$HOME/.local/share/gtksourceview-3.0/styles/`` (see +the general documentation about |GtkSourceView| for the various +possibilities). Note that the style of the rest of graphical part of +Coqide is not under the control of |GtkSourceView| but of GTK+ and +governed by files such as ``settings.ini`` and ``gtk.css`` in +``$XDG_CONFIG_HOME/gtk-3.0`` or files in +``$HOME/.themes/NameOfTheme/gtk-3.0``, as well as the environment +variable ``GTK_THEME`` (search on internet for the various +possibilities). The fourth section is for customizing the editor. It includes in particular the ability to activate an Emacs mode named diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 921c7bbbf7..bc77e2e58c 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -245,9 +245,9 @@ file timing data: COQDEP Fast.v COQDEP Slow.v COQC Slow.v - Slow (user: 0.34 mem: 395448 ko) + Slow.vo (user: 0.34 mem: 395448 ko) COQC Fast.v - Fast (user: 0.01 mem: 45184 ko) + Fast.vo (user: 0.01 mem: 45184 ko) + ``pretty-timed`` this target stores the output of ``make TIMED=1`` into @@ -280,15 +280,15 @@ file timing data: COQDEP Fast.v COQDEP Slow.v COQC Slow.v - Slow (user: 0.36 mem: 393912 ko) + Slow.vo (user: 0.36 mem: 393912 ko) COQC Fast.v - Fast (user: 0.05 mem: 45992 ko) + Fast.vo (user: 0.05 mem: 45992 ko) Time | File Name -------------------- 0m00.41s | Total -------------------- - 0m00.36s | Slow - 0m00.05s | Fast + 0m00.36s | Slow.vo + 0m00.05s | Fast.vo + ``print-pretty-timed-diff`` @@ -338,8 +338,8 @@ file timing data: -------------------------------------------------------- 0m00.39s | Total | 0m00.35s || +0m00.03s | +11.42% -------------------------------------------------------- - 0m00.37s | Slow | 0m00.01s || +0m00.36s | +3600.00% - 0m00.02s | Fast | 0m00.34s || -0m00.32s | -94.11% + 0m00.37s | Slow.vo | 0m00.01s || +0m00.36s | +3600.00% + 0m00.02s | Fast.vo | 0m00.34s || -0m00.32s | -94.11% The following targets and ``Makefile`` variables allow collection of per- diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index 0ace9ef5b9..b63ae32311 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -353,7 +353,7 @@ the optional tactic of the ``Hint Rewrite`` command. .. coqtop:: in reset - Require Import Omega. + Require Import Lia. .. coqtop:: in @@ -367,7 +367,7 @@ the optional tactic of the ``Hint Rewrite`` command. .. coqtop:: in - Hint Rewrite g0 g1 g2 using omega : base1. + Hint Rewrite g0 g1 g2 using lia : base1. .. coqtop:: in diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 62708b01ed..1772362351 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1715,6 +1715,7 @@ performance issue. .. coqtop:: reset in + Set Warnings "-omega-is-deprecated". Require Import Coq.omega.Omega. Ltac mytauto := tauto. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 90a991794f..b5d1e8bffd 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -2607,7 +2607,7 @@ After the :token:`i_pattern`, a list of binders is allowed. .. coqtop:: reset none From Coq Require Import ssreflect. - From Coq Require Import Omega. + From Coq Require Import ZArith Lia. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -2615,7 +2615,7 @@ After the :token:`i_pattern`, a list of binders is allowed. .. coqtop:: all Lemma test : True. - have H x (y : nat) : 2 * x + y = x + x + y by omega. + have H x (y : nat) : 2 * x + y = x + x + y by lia. A proof term provided after ``:=`` can mention these bound variables (that are automatically introduced with the given names). @@ -2625,7 +2625,7 @@ with parentheses even if no type is specified: .. coqtop:: all restart - have (x) : 2 * x = x + x by omega. + have (x) : 2 * x = x + x by lia. The :token:`i_item` and :token:`s_item` can be used to interpret the asserted hypothesis with views (see section :ref:`views_and_reflection_ssr`) or simplify the resulting @@ -2668,9 +2668,9 @@ context entry name. Arguments Sub {_} _ _. Lemma test n m (H : m + 1 < n) : True. - have @i : 'I_n by apply: (Sub m); omega. + have @i : 'I_n by apply: (Sub m); lia. -Note that the subterm produced by :tacn:`omega` is in general huge and +Note that the subterm produced by :tacn:`lia` is in general huge and uninteresting, and hence one may want to hide it. For this purpose the ``[: name ]`` intro pattern and the tactic ``abstract`` (see :ref:`abstract_ssr`) are provided. @@ -2680,7 +2680,7 @@ For this purpose the ``[: name ]`` intro pattern and the tactic .. coqtop:: all abort Lemma test n m (H : m + 1 < n) : True. - have [:pm] @i : 'I_n by apply: (Sub m); abstract: pm; omega. + have [:pm] @i : 'I_n by apply: (Sub m); abstract: pm; lia. The type of ``pm`` can be cleaned up by its annotation ``(*1*)`` by just simplifying it. The annotations are there for technical reasons only. @@ -2694,7 +2694,7 @@ with have and an explicit term, they must be used as follows: Lemma test n m (H : m + 1 < n) : True. have [:pm] @i : 'I_n := Sub m pm. - by omega. + by lia. In this case the abstract constant ``pm`` is assigned by using it in the term that follows ``:=`` and its corresponding goal is left to be @@ -2712,7 +2712,7 @@ makes use of it). .. coqtop:: all abort Lemma test n m (H : m + 1 < n) : True. - have [:pm] @i k : 'I_(n+k) by apply: (Sub m); abstract: pm k; omega. + have [:pm] @i k : 'I_(n+k) by apply: (Sub m); abstract: pm k; lia. Last, notice that the use of intro patterns for abstract constants is orthogonal to the transparent flag ``@`` for have. @@ -2963,7 +2963,7 @@ illustrated in the following example. .. coqtop:: reset none - From Coq Require Import ssreflect Omega. + From Coq Require Import ssreflect Lia. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index 67d0b37e81..65c88ed8d5 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -44,6 +44,7 @@ theories/micromega/Refl.v theories/micromega/RingMicromega.v theories/micromega/Tauto.v theories/micromega/VarMap.v +theories/micromega/ZArith_hints.v theories/micromega/ZCoeff.v theories/micromega/ZMicromega.v theories/micromega/ZifyInst.v diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index b448d0f9d3..57243207f0 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -188,20 +188,19 @@ class CoqObject(ObjectDescription): def _add_index_entry(self, name, target): """Add `name` (pointing to `target`) to the main index.""" assert isinstance(name, str) - if not name.startswith("_"): - # remove trailing . , found in commands, but not ... (ellipsis) - trim = name.endswith(".") and not name.endswith("...") - index_text = name[:-1] if trim else name - if self.index_suffix: - index_text += " " + self.index_suffix - self.indexnode['entries'].append(('single', index_text, target, '', None)) + # remove trailing . , found in commands, but not ... (ellipsis) + trim = name.endswith(".") and not name.endswith("...") + index_text = name[:-1] if trim else name + if self.index_suffix: + index_text += " " + self.index_suffix + self.indexnode['entries'].append(('single', index_text, target, '', None)) aliases = None # additional indexed names for a command or other object def add_target_and_index(self, name, _, signode): """Attach a link target to `signode` and an index entry for `name`. This is only called (from ``ObjectDescription.run``) if ``:noindex:`` isn't specified.""" - if name: + if name and not (isinstance(name, str) and name.startswith('_')): target = self._add_target(signode, name) self._add_index_entry(name, target) if self.aliases is not None: diff --git a/ide/coqide.ml b/ide/coqide.ml index 3b36875e3a..54ef8c7a8a 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1293,12 +1293,18 @@ let build_ui () = (* Initializing hooks *) let refresh_style style = let style = style_manager#style_scheme style in - let iter_session v = v.script#source_buffer#set_style_scheme style in + let iter_session v = + v.script#source_buffer#set_style_scheme style; + v.proof#source_buffer#set_style_scheme style; + v.messages#default_route#source_buffer#set_style_scheme style in List.iter iter_session notebook#pages in let refresh_language lang = let lang = lang_manager#language lang in - let iter_session v = v.script#source_buffer#set_language lang in + let iter_session v = + v.script#source_buffer#set_language lang; + v.proof#source_buffer#set_language lang; + v.messages#default_route#source_buffer#set_language lang in List.iter iter_session notebook#pages in let refresh_toolbar b = diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index b99e5f8069..9d97b01a7a 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -28,6 +28,7 @@ end class type message_view = object inherit GObj.widget + method source_buffer : GSourceView3.source_buffer method connect : message_view_signals method clear : unit method add : Pp.t -> unit @@ -44,7 +45,9 @@ class type message_view = let message_view () : message_view = let buffer = GSourceView3.source_buffer ~highlight_matching_brackets:true - ~tag_table:Tags.Message.table () + ~tag_table:Tags.Message.table + ?language:(lang_manager#language source_language#get) + ?style_scheme:(style_manager#style_scheme source_style#get) () in let mark = buffer#create_mark ~left_gravity:false buffer#start_iter in let box = GPack.vbox () in @@ -88,6 +91,8 @@ let message_view () : message_view = val push = new GUtil.signal () + method source_buffer = buffer + method connect = new message_view_signals_impl box#as_widget push diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli index 21c11b2754..054dd0e571 100644 --- a/ide/wg_MessageView.mli +++ b/ide/wg_MessageView.mli @@ -18,6 +18,7 @@ end class type message_view = object inherit GObj.widget + method source_buffer : GSourceView3.source_buffer method connect : message_view_signals method clear : unit method add : Pp.t -> unit diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 3e03ef11f7..b8ed3436ce 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -15,6 +15,7 @@ open Ideutils class type proof_view = object inherit GObj.widget + method source_buffer : GSourceView3.source_buffer method buffer : GText.buffer method refresh : force:bool -> unit method clear : unit -> unit @@ -195,7 +196,9 @@ let display mode (view : #GText.view_skel) goals hints evars = let proof_view () = let buffer = GSourceView3.source_buffer ~highlight_matching_brackets:true - ~tag_table:Tags.Proof.table () + ~tag_table:Tags.Proof.table + ?language:(lang_manager#language source_language#get) + ?style_scheme:(style_manager#style_scheme source_style#get) () in let text_buffer = new GText.buffer buffer#as_buffer in let view = GSourceView3.source_view @@ -217,6 +220,8 @@ let proof_view () = val mutable evars = None val mutable last_width = -1 + method source_buffer = buffer + method buffer = text_buffer method clear () = buffer#set_text "" diff --git a/ide/wg_ProofView.mli b/ide/wg_ProofView.mli index db6fb9e9cd..8217f72066 100644 --- a/ide/wg_ProofView.mli +++ b/ide/wg_ProofView.mli @@ -11,6 +11,7 @@ class type proof_view = object inherit GObj.widget + method source_buffer : GSourceView3.source_buffer method buffer : GText.buffer method refresh : force:bool -> unit method clear : unit -> unit diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 45255609e0..b72802d911 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -53,6 +53,12 @@ type var_internalization_type = | Method | Variable +type var_unique_id = string + +let var_uid = + let count = ref 0 in + fun id -> incr count; Id.to_string id ^ ":" ^ string_of_int !count + type var_internalization_data = (* type of the "free" variable, for coqdoc, e.g. while typing the constructor of JMeq, "JMeq" behaves as a variable of type Inductive *) @@ -60,7 +66,9 @@ type var_internalization_data = (* signature of impargs of the variable *) Impargs.implicit_status list * (* subscopes of the args of the variable *) - scope_name option list + scope_name option list * + (* unique ID for coqdoc links *) + var_unique_id type internalization_env = (var_internalization_data) Id.Map.t @@ -177,15 +185,18 @@ let parsing_explicit = ref false let empty_internalization_env = Id.Map.empty -let compute_internalization_data env sigma ty typ impl = +let compute_internalization_data env sigma id ty typ impl = let impl = compute_implicits_with_manual env sigma typ (is_implicit_args()) impl in - (ty, impl, compute_arguments_scope sigma typ) + (ty, impl, compute_arguments_scope sigma typ, var_uid id) let compute_internalization_env env sigma ?(impls=empty_internalization_env) ty = List.fold_left3 - (fun map id typ impl -> Id.Map.add id (compute_internalization_data env sigma ty typ impl) map) + (fun map id typ impl -> Id.Map.add id (compute_internalization_data env sigma id ty typ impl) map) impls +let extend_internalization_data (r, impls, scopes, uid) impl scope = + (r, impls@[impl], scopes@[scope], uid) + (**********************************************************************) (* Contracting "{ _ }" in notations *) @@ -341,7 +352,7 @@ let impls_binder_list = let impls_type_list n ?(args = []) = let rec aux acc n c = match DAst.get c with | GProd (na,bk,_,c) -> aux (build_impls n bk na acc) (n+1) c - | _ -> (Variable,List.rev acc,[]) + | _ -> List.rev acc in aux args n let impls_term_list n ?(args = []) = @@ -351,7 +362,7 @@ let impls_term_list n ?(args = []) = let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in let n,acc' = List.fold_left (fun (n,acc) (na, bk, _, _) -> (n+1,build_impls n bk na acc)) (n,acc) args.(nb) in aux acc' n bds.(nb) - |_ -> (Variable,List.rev acc,[]) + |_ -> List.rev acc in aux args n (* Check if in binder "(x1 x2 .. xn : t)", none of x1 .. xn-1 occurs in t *) @@ -431,8 +442,9 @@ let push_name_env ntnvars implargs env = if Id.Map.is_empty ntnvars && Id.equal id ldots_var then error_ldots_var ?loc; set_var_scope ?loc id false (env.tmp_scope,env.scopes) ntnvars; - Dumpglob.dump_binding ?loc id; - pure_push_name_env (id,implargs) env + let uid = var_uid id in + Dumpglob.dump_binding ?loc uid; + pure_push_name_env (id,(Variable,implargs,[],uid)) env let remember_binders_impargs env bl = List.map_filter (fun (na,_,_,_) -> @@ -463,7 +475,7 @@ let intern_generalized_binder intern_type ntnvars let ty' = intern_type {env with ids = ids; unb = true} ty in let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty' in let env' = List.fold_left - (fun env {loc;v=x} -> push_name_env ntnvars (Variable,[],[])(*?*) env (make ?loc @@ Name x)) + (fun env {loc;v=x} -> push_name_env ntnvars [](*?*) env (make ?loc @@ Name x)) env fvs in let b' = check_implicit_meaningful ?loc b' env in let bl = List.map @@ -530,7 +542,7 @@ let intern_cases_pattern_as_binder ?loc ntnvars env p = user_err ?loc (str "Unsupported nested \"as\" clause."); il,disjpat in - let env = List.fold_right (fun {loc;v=id} env -> push_name_env ntnvars (Variable,[],[]) env (make ?loc @@ Name id)) il env in + let env = List.fold_right (fun {loc;v=id} env -> push_name_env ntnvars [] env (make ?loc @@ Name id)) il env in let na = alias_of_pat (List.hd disjpat) in let ienv = Name.fold_right Id.Set.remove na env.ids in let id = Namegen.next_name_away_with_default "pat" na ienv in @@ -586,7 +598,7 @@ let intern_generalization intern env ntnvars loc bk ak c = GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None), acc)) in List.fold_right (fun ({loc;v=id} as lid) (env, acc) -> - let env' = push_name_env ntnvars (Variable,[],[]) env CAst.(make @@ Name id) in + let env' = push_name_env ntnvars [] env CAst.(make @@ Name id) in (env', abs lid acc)) fvs (env,c) in c' @@ -677,7 +689,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam if onlyident then (* Do not try to interpret a variable as a constructor *) let na = out_patvar pat in - let env = push_name_env ntnvars (Variable,[],[]) env (make ?loc:pat.loc na) in + let env = push_name_env ntnvars [] env (make ?loc:pat.loc na) in (renaming,env), None, na else (* Interpret as a pattern *) @@ -1004,9 +1016,9 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us = else (* Is [id] registered with implicit arguments *) try - let ty,impls,argsc = Id.Map.find id env.impls in + let ty,impls,argsc,uid = Id.Map.find id env.impls in let tys = string_of_ty ty in - Dumpglob.dump_reference ?loc "<>" (Id.to_string id) tys; + Dumpglob.dump_reference ?loc "<>" uid tys; gvar (loc,id) us, make_implicits_list impls, argsc with Not_found -> (* Is [id] bound in current term or is an ltac var bound to constr *) @@ -2084,7 +2096,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = List.rev_append match_td matchs) tms ([],Id.Set.empty,Id.Map.empty,[]) in let env' = Id.Set.fold - (fun var bli -> push_name_env ntnvars (Variable,[],[]) bli (CAst.make @@ Name var)) + (fun var bli -> push_name_env ntnvars [] bli (CAst.make @@ Name var)) (Id.Set.union ex_ids as_in_vars) (restart_lambda_binders env) in @@ -2122,17 +2134,17 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (* "in" is None so no match to add *) let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in let p' = Option.map (fun u -> - let env'' = push_name_env ntnvars (Variable,[],[]) env' + let env'' = push_name_env ntnvars [] env' (CAst.make na') in intern_type (slide_binders env'') u) po in DAst.make ?loc @@ GLetTuple (List.map (fun { CAst.v } -> v) nal, (na', p'), b', - intern (List.fold_left (push_name_env ntnvars (Variable,[],[])) env nal) c) + intern (List.fold_left (push_name_env ntnvars []) env nal) c) | CIf (c, (na,po), b1, b2) -> let env' = reset_tmp_scope env in let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,na,None) in (* no "in" no match to ad too *) let p' = Option.map (fun p -> - let env'' = push_name_env ntnvars (Variable,[],[]) env + let env'' = push_name_env ntnvars [] env (CAst.make na') in intern_type (slide_binders env'') p) po in DAst.make ?loc @@ diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 9f06f16258..2eb96aad56 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -43,26 +43,28 @@ type var_internalization_type = | Method | Variable -type var_internalization_data = - var_internalization_type * - (* type of the "free" variable, for coqdoc, e.g. while typing the - constructor of JMeq, "JMeq" behaves as a variable of type Inductive *) - - Impargs.implicit_status list * (* signature of impargs of the variable *) - Notation_term.scope_name option list (* subscopes of the args of the variable *) +(** This collects relevant information for interning local variables: + - their coqdoc kind (a recursive call in a inductive, fixpoint of class; or a bound variable) + e.g. while typing the constructor of JMeq, "JMeq" behaves as a variable of type Inductive + - their implicit arguments + - their argument scopes *) +type var_internalization_data (** A map of free variables to their implicit arguments and scopes *) type internalization_env = var_internalization_data Id.Map.t val empty_internalization_env : internalization_env -val compute_internalization_data : env -> evar_map -> var_internalization_type -> +val compute_internalization_data : env -> evar_map -> Id.t -> var_internalization_type -> types -> Impargs.manual_implicits -> var_internalization_data val compute_internalization_env : env -> evar_map -> ?impls:internalization_env -> var_internalization_type -> Id.t list -> types list -> Impargs.manual_implicits list -> internalization_env +val extend_internalization_data : + var_internalization_data -> Impargs.implicit_status -> scope_name option -> var_internalization_data + type ltac_sign = { ltac_vars : Id.Set.t; (** Variables of Ltac which may be bound to a term *) diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index e659a5ac5c..57ec708b07 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -246,8 +246,6 @@ let add_glob_kn ?loc kn = let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in add_glob_gen ?loc sp lib_dp "syndef" -let dump_binding ?loc id = () - let dump_def ?loc ty secpath id = Option.iter (fun loc -> if !glob_output = Feedback then Feedback.feedback (Feedback.GlobDef (loc, id, secpath, ty)) @@ -275,3 +273,6 @@ let dump_notation (loc,(df,_)) sc sec = Option.iter (fun loc -> let location = (Loc.make_loc (i, i+1)) in dump_def ~loc:location "not" (Names.DirPath.to_string (Lib.current_dirpath sec)) (cook_notation df sc) ) loc + +let dump_binding ?loc uid = + dump_def ?loc "binder" "<>" uid diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 5409b20472..14e5a81308 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -36,7 +36,7 @@ val dump_secvar : ?loc:Loc.t -> Names.Id.t -> unit val dump_libref : ?loc:Loc.t -> Names.DirPath.t -> string -> unit val dump_notation_location : (int * int) list -> Constrexpr.notation -> (Notation.notation_location * Notation_term.scope_name option) -> unit -val dump_binding : ?loc:Loc.t -> Names.Id.Set.elt -> unit +val dump_binding : ?loc:Loc.t -> string -> unit val dump_notation : (Constrexpr.notation * Notation.notation_location) Loc.located -> Notation_term.scope_name option -> bool -> unit diff --git a/library/goptions.ml b/library/goptions.ml index 1418407533..666ba8ee2e 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -24,6 +24,10 @@ type option_value = | StringValue of string | StringOptValue of string option +type table_value = + | StringRefValue of string + | QualidRefValue of qualid + (** Summary of an option status *) type option_state = { opt_depr : bool; @@ -35,8 +39,13 @@ type option_state = { let nickname table = String.concat " " table +let error_no_table_of_this_type ~kind key = + user_err ~hdr:"Goptions" + (str ("There is no " ^ kind ^ "-valued table with this name: \"" ^ nickname key ^ "\".")) + let error_undeclared_key key = - user_err ~hdr:"Goptions" (str (nickname key) ++ str ": no table or option of this type") + user_err ~hdr:"Goptions" + (str ("There is no flag, option or table with this name: \"" ^ nickname key ^ "\".")) (****************************************************************************) (* 1- Tables *) @@ -184,6 +193,23 @@ end module MakeRefTable = functor (A : RefConvertArg) -> MakeTable (RefConvert(A)) +type iter_table_aux = { aux : 'a. 'a table_of_A -> Environ.env -> 'a -> unit } + +let iter_table f key lv = + let aux = function + | StringRefValue s -> + begin + try f.aux (get_string_table key) (Global.env()) s + with Not_found -> error_no_table_of_this_type ~kind:"string" key + end + | QualidRefValue locqid -> + begin + try f.aux (get_ref_table key) (Global.env()) locqid + with Not_found -> error_no_table_of_this_type ~kind:"qualid" key + end + in + List.iter aux lv + (****************************************************************************) (* 2- Flags. *) @@ -387,9 +413,10 @@ let declare_interpreted_string_option_and_ref ~depr ~key ~(value:'a) from_string (* Setting values of options *) let warn_unknown_option = - CWarnings.create ~name:"unknown-option" ~category:"option" - (fun key -> strbrk "There is no option " ++ - str (nickname key) ++ str ".") + CWarnings.create + ~name:"unknown-option" ~category:"option" + (fun key -> strbrk "There is no flag or option with this name: \"" ++ + str (nickname key) ++ str "\".") let set_option_value ?(locality = OptDefault) check_and_cast key v = let opt = try Some (get_option key) with Not_found -> None in diff --git a/library/goptions.mli b/library/goptions.mli index 336cae420c..150954cbac 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -187,6 +187,10 @@ type option_value = | StringValue of string | StringOptValue of string option +type table_value = + | StringRefValue of string + | QualidRefValue of qualid + val set_option_value : ?locality:option_locality -> ('a -> option_value -> option_value) -> option_name -> 'a -> unit (** [set_option_value ?locality f name v] sets [name] to the result of @@ -204,4 +208,7 @@ type option_state = { val get_tables : unit -> option_state OptionMap.t val print_tables : unit -> Pp.t +type iter_table_aux = { aux : 'a. 'a table_of_A -> Environ.env -> 'a -> unit } +val iter_table : iter_table_aux -> option_name -> table_value list -> unit + val error_undeclared_key : option_name -> 'a diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index eec78391af..55e659d487 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -46,7 +46,7 @@ let build_newrecursive lnameargsardef = Constrintern.interp_context_evars ~program_mode:false env evd binders in let impl = - Constrintern.compute_internalization_data env0 evd + Constrintern.compute_internalization_data env0 evd recname Constrintern.Recursive arity impls' in let open Context.Named.Declaration in diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 2eef459217..79d6c05e1d 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1899,8 +1899,15 @@ let destructure_goal = let destructure_goal = destructure_goal +let warn_omega_is_deprecated = + let name = "omega-is-deprecated" in + let category = "deprecated" in + CWarnings.create ~name ~category (fun () -> + Pp.str "omega is deprecated since 8.12; use “lia” instead.") + let omega_solver = Proofview.tclUNIT () >>= fun () -> (* delay for [check_required_library] *) + warn_omega_is_deprecated (); Coqlib.check_required_library ["Coq";"omega";"Omega"]; reset_all (); destructure_goal diff --git a/tactics/eauto.ml b/tactics/eauto.ml index a89e5ef19a..28b5ed5811 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -430,29 +430,39 @@ let make_dimension n = function | None -> (true,make_depth n) | Some d -> (false,d) +let autounfolds ids csts gl cls = + let hyps = Tacmach.New.pf_ids_of_hyps gl in + let env = Tacmach.New.pf_env gl in + let ids = List.filter (fun id -> List.mem id hyps && Tacred.is_evaluable env (EvalVarRef id)) ids in + let csts = List.filter (fun cst -> Tacred.is_evaluable env (EvalConstRef cst)) csts in + let flags = + List.fold_left (fun flags cst -> CClosure.RedFlags.(red_add flags (fCONST cst))) + (List.fold_left (fun flags id -> CClosure.RedFlags.(red_add flags (fVAR id))) + CClosure.betaiotazeta ids) csts + in reduct_option ~check:false (Reductionops.clos_norm_flags flags, DEFAULTcast) cls + let cons a l = a :: l -let autounfolds db occs cls gl = - let unfolds = List.concat (List.map (fun dbname -> - let db = try searchtable_map dbname - with Not_found -> user_err ~hdr:"autounfold" (str "Unknown database " ++ str dbname) - in - let (ids, csts) = Hint_db.unfolds db in - let hyps = pf_ids_of_hyps gl in - let ids = Id.Set.filter (fun id -> List.mem id hyps) ids in - Cset.fold (fun cst -> cons (AllOccurrences, EvalConstRef cst)) csts - (Id.Set.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db) - in Proofview.V82.of_tactic (unfold_option unfolds cls) gl +exception UnknownDatabase of string let autounfold db cls = - Proofview.V82.tactic begin fun gl -> - let cls = concrete_clause_of (fun () -> pf_ids_of_hyps gl) cls in - let tac = autounfolds db in - tclMAP (function - | OnHyp (id,occs,where) -> tac occs (Some (id,where)) - | OnConcl occs -> tac occs None) - cls gl - end + if not (Locusops.clause_with_generic_occurrences cls) then + user_err ~hdr:"autounfold" (str "\"at\" clause not supported"); + match List.fold_left (fun (ids, csts) dbname -> + let db = try searchtable_map dbname + with Not_found -> raise (UnknownDatabase dbname) + in + let (db_ids, db_csts) = Hint_db.unfolds db in + (Id.Set.fold cons db_ids ids, Cset.fold cons db_csts csts)) ([], []) db + with + | (ids, csts) -> Proofview.Goal.enter begin fun gl -> + let cls = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cls in + let tac = autounfolds ids csts gl in + Tacticals.New.tclMAP (function + | OnHyp (id, _, where) -> tac (Some (id, where)) + | OnConcl _ -> tac None) cls + end + | exception UnknownDatabase dbname -> Tacticals.New.tclZEROMSG (str "Unknown database " ++ str dbname) let autounfold_tac db cls = Proofview.tclUNIT () >>= fun () -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c79aca3d3c..8c4400a80f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4499,7 +4499,7 @@ let check_expected_type env sigma (elimc,bl) elimt = if n == 0 then error "Scheme cannot be applied."; let sigma,cl = make_evar_clause env sigma ~len:(n - 1) elimt in let sigma = solve_evar_clause env sigma true cl bl in - let (_,u,_) = destProd sigma cl.cl_concl in + let (_,u,_) = destProd sigma (whd_all env sigma cl.cl_concl) in fun t -> match Evarconv.unify_leq_delay env sigma t u with | _sigma -> true | exception Evarconv.UnableToUnify _ -> false diff --git a/test-suite/bugs/closed/bug_12045.v b/test-suite/bugs/closed/bug_12045.v new file mode 100644 index 0000000000..4e416778a9 --- /dev/null +++ b/test-suite/bugs/closed/bug_12045.v @@ -0,0 +1,19 @@ +(* Check enough reduction happens in the conclusion of an induction scheme *) + +Lemma foo : + forall (P : nat -> Prop), + (forall n, P (S n)) -> + forall n, + (fun e => + IsSucc e -> + P e) n. +Proof. +Admitted. + +Theorem bar : forall n, + IsSucc n -> + True. +Proof. + intros. + Fail induction n using foo. (* was an anomaly *) +Admitted. diff --git a/test-suite/bugs/closed/bug_1912.v b/test-suite/bugs/closed/bug_1912.v index 987a541778..0228abbb9b 100644 --- a/test-suite/bugs/closed/bug_1912.v +++ b/test-suite/bugs/closed/bug_1912.v @@ -1,4 +1,4 @@ -Require Import ZArith. +Require Import Omega. Goal forall x, Z.succ (Z.pred x) = x. intros x. diff --git a/test-suite/bugs/closed/bug_7812.v b/test-suite/bugs/closed/bug_7812.v new file mode 100644 index 0000000000..a714eea81d --- /dev/null +++ b/test-suite/bugs/closed/bug_7812.v @@ -0,0 +1,30 @@ +Module Foo. + Definition binary A := A -> A -> Prop. + + Definition inter A (R1 R2 : binary A): binary A := + fun (x y:A) => R1 x y /\ R2 x y. +End Foo. + +Module Simple_sparse_proof. + Parameter node : Type. + Parameter graph : Type. + Parameter has_edge : graph -> node -> node -> Prop. + Implicit Types x y z : node. + Implicit Types G : graph. + + Parameter mem : forall A, A -> list A -> Prop. + Hypothesis mem_nil : forall x, mem node x nil = False. + + Definition notin (l: list node): node -> node -> Prop := + fun x y => ~ mem node x l /\ ~ mem node y l. + + Definition edge_notin G l : node -> node -> Prop := + Foo.inter node (has_edge G) (notin l). + + Hint Unfold Foo.inter notin edge_notin : rel_crush. + + Lemma edge_notin_nil G : forall x y, edge_notin G nil x y <-> has_edge G x y. + Proof. + intros. autounfold with rel_crush. rewrite !mem_nil. tauto. + Qed. +End Simple_sparse_proof. diff --git a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired index 7900c034da..ebe44f3548 100644 --- a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired +++ b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired @@ -1,15 +1,5 @@ -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' COQDEP VFILES -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' COQC Slow.v -Slow (real: 0.04, user: 0.02, sys: 0.01, mem: 45512 ko) +Slow.vo (real: 0.04, user: 0.02, sys: 0.01, mem: 45512 ko) COQC Fast.v -Fast (real: 0.41, user: 0.37, sys: 0.04, mem: 395200 ko) -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' +Fast.vo (real: 0.41, user: 0.37, sys: 0.04, mem: 395200 ko) diff --git a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired index 7ab0bc75d9..bf17a3e95c 100644 --- a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired +++ b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired @@ -1,15 +1,5 @@ -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' COQDEP VFILES -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' COQC Slow.v -Slow (real: 0.40, user: 0.35, sys: 0.04, mem: 394968 ko) +Slow.vo (real: 0.40, user: 0.35, sys: 0.04, mem: 394968 ko) COQC Fast.v -Fast (real: 0.04, user: 0.03, sys: 0.00, mem: 46564 ko) -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' +Fast.vo (real: 0.04, user: 0.03, sys: 0.00, mem: 46564 ko) diff --git a/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired index 72c520218c..c8f35dc1e4 100644 --- a/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired +++ b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired @@ -2,5 +2,5 @@ After | File Name | Before || Change | % Change -------------------------------------------------------- 0m00.34s | Total | 0m00.49s || -0m00.14s | -30.61% -------------------------------------------------------- -0m00.32s | Fast | 0m00.02s || +0m00.30s | +1500.00% -0m00.02s | Slow | 0m00.47s || -0m00.44s | -95.74%
\ No newline at end of file +0m00.32s | Fast.vo | 0m00.02s || +0m00.30s | +1500.00% +0m00.02s | Slow.vo | 0m00.47s || -0m00.44s | -95.74%
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index 4ee4aae36c..f556638640 100755 --- a/test-suite/coq-makefile/timing/run.sh +++ b/test-suite/coq-makefile/timing/run.sh @@ -63,7 +63,7 @@ TO_SED_IN_PER_LINE=( for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do for ext in "" .desired; do - grep -v 'warning: undefined variable' < ${file}${ext} | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_FILE[@]}" > ${file}${ext}.processed + sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_FILE[@]}" ${file}${ext} > ${file}${ext}.processed done echo "cat $file" cat "$file" diff --git a/test-suite/coqdoc/binder.html.out b/test-suite/coqdoc/binder.html.out new file mode 100644 index 0000000000..af8eb46845 --- /dev/null +++ b/test-suite/coqdoc/binder.html.out @@ -0,0 +1,41 @@ +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" +"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> +<html xmlns="http://www.w3.org/1999/xhtml"> +<head> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> +<link href="coqdoc.css" rel="stylesheet" type="text/css" /> +<title>Coqdoc.binder</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library Coqdoc.binder</h1> + +<div class="code"> +</div> + +<div class="doc"> +Link binders +</div> +<div class="code"> + +<br/> +<span class="id" title="keyword">Definition</span> <a id="foo" class="idref" href="#foo"><span class="id" title="definition">foo</span></a> <a id="alpha:1" class="idref" href="#alpha:1"><span class="id" title="binder">alpha</span></a> <a id="beta:2" class="idref" href="#beta:2"><span class="id" title="binder">beta</span></a> := <a class="idref" href="Coqdoc.binder.html#alpha:1"><span class="id" title="variable">alpha</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="Coqdoc.binder.html#beta:2"><span class="id" title="variable">beta</span></a>.<br/> +</div> +</div> + +<div id="footer"> +<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> +</div> + +</div> + +</body> +</html>
\ No newline at end of file diff --git a/test-suite/coqdoc/binder.tex.out b/test-suite/coqdoc/binder.tex.out new file mode 100644 index 0000000000..2b5648aee6 --- /dev/null +++ b/test-suite/coqdoc/binder.tex.out @@ -0,0 +1,28 @@ +\documentclass[12pt]{report} +\usepackage[utf8x]{inputenc} + +%Warning: tipa declares many non-standard macros used by utf8x to +%interpret utf8 characters but extra packages might have to be added +%such as "textgreek" for Greek letters not already in tipa +%or "stmaryrd" for mathematical symbols. +%Utf8 codes missing a LaTeX interpretation can be defined by using +%\DeclareUnicodeCharacter{code}{interpretation}. +%Use coqdoc's option -p to add new packages or declarations. +\usepackage{tipa} + +\usepackage[T1]{fontenc} +\usepackage{fullpage} +\usepackage{coqdoc} +\usepackage{amsmath,amssymb} +\usepackage{url} +\begin{document} +\coqlibrary{Coqdoc.binder}{Library }{Coqdoc.binder} + +\begin{coqdoccode} +\end{coqdoccode} +Link binders \begin{coqdoccode} +\coqdocemptyline +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.binder.foo}{foo}{\coqdocdefinition{foo}} \coqdef{Coqdoc.binder.alpha:1}{alpha}{\coqdocbinder{alpha}} \coqdef{Coqdoc.binder.beta:2}{beta}{\coqdocbinder{beta}} := \coqref{Coqdoc.binder.alpha:1}{\coqdocvariable{alpha}} \coqexternalref{::nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}} \coqref{Coqdoc.binder.beta:2}{\coqdocvariable{beta}}.\coqdoceol +\end{coqdoccode} +\end{document} diff --git a/test-suite/coqdoc/binder.v b/test-suite/coqdoc/binder.v new file mode 100644 index 0000000000..283ef64ac5 --- /dev/null +++ b/test-suite/coqdoc/binder.v @@ -0,0 +1,3 @@ +(** Link binders *) + +Definition foo alpha beta := alpha + beta. diff --git a/test-suite/coqdoc/bug11194.html.out b/test-suite/coqdoc/bug11194.html.out index 304d041033..6fc6533e59 100644 --- a/test-suite/coqdoc/bug11194.html.out +++ b/test-suite/coqdoc/bug11194.html.out @@ -19,11 +19,11 @@ <h1 class="libtitle">Library Coqdoc.bug11194</h1> <div class="code"> -<span class="id" title="keyword">Record</span> <a name="a_struct"><span class="id" title="record">a_struct</span></a> := { <a name="anum"><span class="id" title="projection">anum</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> }.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="keyword">Structure</span> <a name="a_struct_0"><span class="id" title="definition">a_struct_0</span></a> := {| <a class="idref" href="Coqdoc.bug11194.html#Build_a_struct"><span class="id" title="constructor">anum</span></a> <a class="idref" href="Coqdoc.bug11194.html#Build_a_struct"><span class="id" title="constructor">:=</span></a> <a class="idref" href="Coqdoc.bug11194.html#Build_a_struct"><span class="id" title="constructor">0</span></a>|}.<br/> -<span class="id" title="keyword">Definition</span> <a name="rename_a_s_0"><span class="id" title="definition">rename_a_s_0</span></a> := <a class="idref" href="Coqdoc.bug11194.html#a_struct_0"><span class="id" title="definition">a_struct_0</span></a>.<br/> -<span class="id" title="keyword">Coercion</span> <a name="some_nat"><span class="id" title="definition">some_nat</span></a> := (@<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>).<br/> -<span class="id" title="keyword">Definition</span> <a name="rename_some_nat"><span class="id" title="definition">rename_some_nat</span></a> := <a class="idref" href="Coqdoc.bug11194.html#some_nat"><span class="id" title="definition">some_nat</span></a>.<br/> +<span class="id" title="keyword">Record</span> <a id="a_struct" class="idref" href="#a_struct"><span class="id" title="record">a_struct</span></a> := { <a id="anum" class="idref" href="#anum"><span class="id" title="projection">anum</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> }.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="keyword">Structure</span> <a id="a_struct_0" class="idref" href="#a_struct_0"><span class="id" title="definition">a_struct_0</span></a> := {| <a class="idref" href="Coqdoc.bug11194.html#Build_a_struct"><span class="id" title="constructor">anum</span></a> <a class="idref" href="Coqdoc.bug11194.html#Build_a_struct"><span class="id" title="constructor">:=</span></a> <a class="idref" href="Coqdoc.bug11194.html#Build_a_struct"><span class="id" title="constructor">0</span></a>|}.<br/> +<span class="id" title="keyword">Definition</span> <a id="rename_a_s_0" class="idref" href="#rename_a_s_0"><span class="id" title="definition">rename_a_s_0</span></a> := <a class="idref" href="Coqdoc.bug11194.html#a_struct_0"><span class="id" title="definition">a_struct_0</span></a>.<br/> +<span class="id" title="keyword">Coercion</span> <a id="some_nat" class="idref" href="#some_nat"><span class="id" title="definition">some_nat</span></a> := (@<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>).<br/> +<span class="id" title="keyword">Definition</span> <a id="rename_some_nat" class="idref" href="#rename_some_nat"><span class="id" title="definition">rename_some_nat</span></a> := <a class="idref" href="Coqdoc.bug11194.html#some_nat"><span class="id" title="definition">some_nat</span></a>.<br/> </div> </div> diff --git a/test-suite/coqdoc/bug11353.html.out b/test-suite/coqdoc/bug11353.html.out index 0b4b4b6e37..f9d6a79906 100644 --- a/test-suite/coqdoc/bug11353.html.out +++ b/test-suite/coqdoc/bug11353.html.out @@ -19,13 +19,13 @@ <h1 class="libtitle">Library Coqdoc.bug11353</h1> <div class="code"> -<span class="id" title="keyword">Definition</span> <a name="a"><span class="id" title="definition">a</span></a> := 0. #[ <span class="id" title="var">universes</span>( <span class="id" title="var">template</span>) ]<br/> -<span class="id" title="keyword">Inductive</span> <a name="mysum"><span class="id" title="inductive">mysum</span></a> (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> :=<br/> - | <a name="myinl"><span class="id" title="constructor">myinl</span></a> : <a class="idref" href="Coqdoc.bug11353.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="Coqdoc.bug11353.html#mysum"><span class="id" title="inductive">mysum</span></a> <a class="idref" href="Coqdoc.bug11353.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.bug11353.html#B"><span class="id" title="variable">B</span></a><br/> - | <a name="myinr"><span class="id" title="constructor">myinr</span></a> : <a class="idref" href="Coqdoc.bug11353.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="Coqdoc.bug11353.html#mysum"><span class="id" title="inductive">mysum</span></a> <a class="idref" href="Coqdoc.bug11353.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.bug11353.html#B"><span class="id" title="variable">B</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a id="a" class="idref" href="#a"><span class="id" title="definition">a</span></a> := 0. #[ <span class="id" title="var">universes</span>( <span class="id" title="var">template</span>) ]<br/> +<span class="id" title="keyword">Inductive</span> <a id="mysum" class="idref" href="#mysum"><span class="id" title="inductive">mysum</span></a> (<a id="A:1" class="idref" href="#A:1"><span class="id" title="binder">A</span></a> <a id="B:2" class="idref" href="#B:2"><span class="id" title="binder">B</span></a>:<span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> :=<br/> + | <a id="myinl" class="idref" href="#myinl"><span class="id" title="constructor">myinl</span></a> : <a class="idref" href="Coqdoc.bug11353.html#A:1"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Coqdoc.bug11353.html#mysum:3"><span class="id" title="inductive">mysum</span></a> <a class="idref" href="Coqdoc.bug11353.html#A:1"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.bug11353.html#B:2"><span class="id" title="variable">B</span></a><br/> + | <a id="myinr" class="idref" href="#myinr"><span class="id" title="constructor">myinr</span></a> : <a class="idref" href="Coqdoc.bug11353.html#B:2"><span class="id" title="variable">B</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Coqdoc.bug11353.html#mysum:3"><span class="id" title="inductive">mysum</span></a> <a class="idref" href="Coqdoc.bug11353.html#A:1"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.bug11353.html#B:2"><span class="id" title="variable">B</span></a>.<br/> <br/> -#[<span class="id" title="var">local</span>]<span class="id" title="keyword">Definition</span> <a name="b"><span class="id" title="definition">b</span></a> := 1.<br/> +#[<span class="id" title="var">local</span>]<span class="id" title="keyword">Definition</span> <a id="b" class="idref" href="#b"><span class="id" title="definition">b</span></a> := 1.<br/> </div> </div> diff --git a/test-suite/coqdoc/bug11353.tex.out b/test-suite/coqdoc/bug11353.tex.out index a6478682d8..12ea109d0e 100644 --- a/test-suite/coqdoc/bug11353.tex.out +++ b/test-suite/coqdoc/bug11353.tex.out @@ -22,11 +22,11 @@ \coqdocnoindent \coqdockw{Definition} \coqdef{Coqdoc.bug11353.a}{a}{\coqdocdefinition{a}} := 0. \#[ \coqdocvar{universes}( \coqdocvar{template}) ]\coqdoceol \coqdocnoindent -\coqdockw{Inductive} \coqdef{Coqdoc.bug11353.mysum}{mysum}{\coqdocinductive{mysum}} (\coqdocvar{A} \coqdocvar{B}:\coqdockw{Type}) : \coqdockw{Type} :=\coqdoceol +\coqdockw{Inductive} \coqdef{Coqdoc.bug11353.mysum}{mysum}{\coqdocinductive{mysum}} (\coqdef{Coqdoc.bug11353.A:1}{A}{\coqdocbinder{A}} \coqdef{Coqdoc.bug11353.B:2}{B}{\coqdocbinder{B}}:\coqdockw{Type}) : \coqdockw{Type} :=\coqdoceol \coqdocindent{1.00em} -\ensuremath{|} \coqdef{Coqdoc.bug11353.myinl}{myinl}{\coqdocconstructor{myinl}} : \coqdocvariable{A} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum}{\coqdocinductive{mysum}} \coqdocvariable{A} \coqdocvariable{B}\coqdoceol +\ensuremath{|} \coqdef{Coqdoc.bug11353.myinl}{myinl}{\coqdocconstructor{myinl}} : \coqref{Coqdoc.bug11353.A:1}{\coqdocvariable{A}} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum:3}{\coqdocinductive{mysum}} \coqref{Coqdoc.bug11353.A:1}{\coqdocvariable{A}} \coqref{Coqdoc.bug11353.B:2}{\coqdocvariable{B}}\coqdoceol \coqdocindent{1.00em} -\ensuremath{|} \coqdef{Coqdoc.bug11353.myinr}{myinr}{\coqdocconstructor{myinr}} : \coqdocvariable{B} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum}{\coqdocinductive{mysum}} \coqdocvariable{A} \coqdocvariable{B}.\coqdoceol +\ensuremath{|} \coqdef{Coqdoc.bug11353.myinr}{myinr}{\coqdocconstructor{myinr}} : \coqref{Coqdoc.bug11353.B:2}{\coqdocvariable{B}} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum:3}{\coqdocinductive{mysum}} \coqref{Coqdoc.bug11353.A:1}{\coqdocvariable{A}} \coqref{Coqdoc.bug11353.B:2}{\coqdocvariable{B}}.\coqdoceol \coqdocemptyline \coqdocnoindent \#[\coqdocvar{local}]\coqdockw{Definition} \coqdef{Coqdoc.bug11353.b}{b}{\coqdocdefinition{b}} := 1.\coqdoceol diff --git a/test-suite/coqdoc/bug5648.html.out b/test-suite/coqdoc/bug5648.html.out index 5c5a2dc299..e1d1c1313e 100644 --- a/test-suite/coqdoc/bug5648.html.out +++ b/test-suite/coqdoc/bug5648.html.out @@ -19,18 +19,18 @@ <h1 class="libtitle">Library Coqdoc.bug5648</h1> <div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="a"><span class="id" title="lemma">a</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a id="a" class="idref" href="#a"><span class="id" title="lemma">a</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a>.<br/> <span class="id" title="keyword">Proof</span>.<br/> <span class="id" title="tactic">auto</span>.<br/> <span class="id" title="keyword">Qed</span>.<br/> <br/> -<span class="id" title="keyword">Variant</span> <a name="t"><span class="id" title="inductive">t</span></a> :=<br/> -| <a name="A"><span class="id" title="constructor">A</span></a> | <a name="Add"><span class="id" title="constructor">Add</span></a> | <a name="G"><span class="id" title="constructor">G</span></a> | <a name="Goal"><span class="id" title="constructor">Goal</span></a> | <a name="L"><span class="id" title="constructor">L</span></a> | <a name="Lemma"><span class="id" title="constructor">Lemma</span></a> | <a name="P"><span class="id" title="constructor">P</span></a> | <a name="Proof"><span class="id" title="constructor">Proof</span></a> .<br/> +<span class="id" title="keyword">Variant</span> <a id="t" class="idref" href="#t"><span class="id" title="inductive">t</span></a> :=<br/> +| <a id="A" class="idref" href="#A"><span class="id" title="constructor">A</span></a> | <a id="Add" class="idref" href="#Add"><span class="id" title="constructor">Add</span></a> | <a id="G" class="idref" href="#G"><span class="id" title="constructor">G</span></a> | <a id="Goal" class="idref" href="#Goal"><span class="id" title="constructor">Goal</span></a> | <a id="L" class="idref" href="#L"><span class="id" title="constructor">L</span></a> | <a id="Lemma" class="idref" href="#Lemma"><span class="id" title="constructor">Lemma</span></a> | <a id="P" class="idref" href="#P"><span class="id" title="constructor">P</span></a> | <a id="Proof" class="idref" href="#Proof"><span class="id" title="constructor">Proof</span></a> .<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="d"><span class="id" title="definition">d</span></a> <span class="id" title="var">x</span> :=<br/> - <span class="id" title="keyword">match</span> <a class="idref" href="Coqdoc.bug5648.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="keyword">with</span><br/> +<span class="id" title="keyword">Definition</span> <a id="d" class="idref" href="#d"><span class="id" title="definition">d</span></a> <a id="x:3" class="idref" href="#x:3"><span class="id" title="binder">x</span></a> :=<br/> + <span class="id" title="keyword">match</span> <a class="idref" href="Coqdoc.bug5648.html#x:3"><span class="id" title="variable">x</span></a> <span class="id" title="keyword">with</span><br/> | <a class="idref" href="Coqdoc.bug5648.html#A"><span class="id" title="constructor">A</span></a> ⇒ 0<br/> | <a class="idref" href="Coqdoc.bug5648.html#Add"><span class="id" title="constructor">Add</span></a> ⇒ 1<br/> | <a class="idref" href="Coqdoc.bug5648.html#G"><span class="id" title="constructor">G</span></a> ⇒ 2<br/> diff --git a/test-suite/coqdoc/bug5648.tex.out b/test-suite/coqdoc/bug5648.tex.out index 82f7da2309..c221d7ca8a 100644 --- a/test-suite/coqdoc/bug5648.tex.out +++ b/test-suite/coqdoc/bug5648.tex.out @@ -34,9 +34,9 @@ \ensuremath{|} \coqdef{Coqdoc.bug5648.A}{A}{\coqdocconstructor{A}} \ensuremath{|} \coqdef{Coqdoc.bug5648.Add}{Add}{\coqdocconstructor{Add}} \ensuremath{|} \coqdef{Coqdoc.bug5648.G}{G}{\coqdocconstructor{G}} \ensuremath{|} \coqdef{Coqdoc.bug5648.Goal}{Goal}{\coqdocconstructor{Goal}} \ensuremath{|} \coqdef{Coqdoc.bug5648.L}{L}{\coqdocconstructor{L}} \ensuremath{|} \coqdef{Coqdoc.bug5648.Lemma}{Lemma}{\coqdocconstructor{Lemma}} \ensuremath{|} \coqdef{Coqdoc.bug5648.P}{P}{\coqdocconstructor{P}} \ensuremath{|} \coqdef{Coqdoc.bug5648.Proof}{Proof}{\coqdocconstructor{Proof}} .\coqdoceol \coqdocemptyline \coqdocnoindent -\coqdockw{Definition} \coqdef{Coqdoc.bug5648.d}{d}{\coqdocdefinition{d}} \coqdocvar{x} :=\coqdoceol +\coqdockw{Definition} \coqdef{Coqdoc.bug5648.d}{d}{\coqdocdefinition{d}} \coqdef{Coqdoc.bug5648.x:3}{x}{\coqdocbinder{x}} :=\coqdoceol \coqdocindent{1.00em} -\coqdockw{match} \coqdocvariable{x} \coqdockw{with}\coqdoceol +\coqdockw{match} \coqref{Coqdoc.bug5648.x:3}{\coqdocvariable{x}} \coqdockw{with}\coqdoceol \coqdocindent{1.00em} \ensuremath{|} \coqref{Coqdoc.bug5648.A}{\coqdocconstructor{A}} \ensuremath{\Rightarrow} 0\coqdoceol \coqdocindent{1.00em} diff --git a/test-suite/coqdoc/bug5700.html.out b/test-suite/coqdoc/bug5700.html.out index b96fc6281d..286e8bba4d 100644 --- a/test-suite/coqdoc/bug5700.html.out +++ b/test-suite/coqdoc/bug5700.html.out @@ -26,7 +26,7 @@ </div> <div class="code"> -<span class="id" title="keyword">Definition</span> <a name="const1"><span class="id" title="definition">const1</span></a> := 1.<br/> +<span class="id" title="keyword">Definition</span> <a id="const1" class="idref" href="#const1"><span class="id" title="definition">const1</span></a> := 1.<br/> <br/> </div> @@ -36,7 +36,7 @@ </div> <div class="code"> -<span class="id" title="keyword">Definition</span> <a name="const2"><span class="id" title="definition">const2</span></a> := 2.<br/> +<span class="id" title="keyword">Definition</span> <a id="const2" class="idref" href="#const2"><span class="id" title="definition">const2</span></a> := 2.<br/> </div> </div> diff --git a/test-suite/coqdoc/links.html.out b/test-suite/coqdoc/links.html.out index d2d4d5d764..12d284dc54 100644 --- a/test-suite/coqdoc/links.html.out +++ b/test-suite/coqdoc/links.html.out @@ -51,93 +51,93 @@ Various checks for coqdoc <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Strings.String.html#"><span class="id" title="library">String</span></a>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="g"><span class="id" title="definition">g</span></a> := "dfjkh""sdfhj forall <> * ~"%<span class="id" title="var">string</span>.<br/> +<span class="id" title="keyword">Definition</span> <a id="g" class="idref" href="#g"><span class="id" title="definition">g</span></a> := "dfjkh""sdfhj forall <> * ~"%<span class="id" title="var">string</span>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="a"><span class="id" title="definition">a</span></a> (<span class="id" title="var">b</span>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) := <a class="idref" href="Coqdoc.links.html#b"><span class="id" title="variable">b</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a id="a" class="idref" href="#a"><span class="id" title="definition">a</span></a> (<a id="b:1" class="idref" href="#b:1"><span class="id" title="binder">b</span></a>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) := <a class="idref" href="Coqdoc.links.html#b:1"><span class="id" title="variable">b</span></a>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="f"><span class="id" title="definition">f</span></a> := <span class="id" title="keyword">∀</span> <span class="id" title="var">C</span>:<span class="id" title="keyword">Prop</span>, <a class="idref" href="Coqdoc.links.html#C"><span class="id" title="variable">C</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a id="f" class="idref" href="#f"><span class="id" title="definition">f</span></a> := <span class="id" title="keyword">∀</span> <a id="C:2" class="idref" href="#C:2"><span class="id" title="binder">C</span></a>:<span class="id" title="keyword">Prop</span>, <a class="idref" href="Coqdoc.links.html#C:2"><span class="id" title="variable">C</span></a>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">"</span></a>n ++ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>).<br/> +<span class="id" title="keyword">Notation</span> <a id="f03f7a04ef75ff3ac66ca5c23554e52e" class="idref" href="#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">"</span></a>n ++ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>).<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">"</span></a>n ++ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#mult"><span class="id" title="abbreviation">mult</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>). +<span class="id" title="keyword">Notation</span> <a id="f03f7a04ef75ff3ac66ca5c23554e52e" class="idref" href="#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">"</span></a>n ++ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#mult"><span class="id" title="abbreviation">mult</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>). <br/> -<span class="id" title="keyword">Notation</span> <a name="f07b3676d96b68749d342542fd80e2b0"><span class="id" title="notation">"</span></a>n ** m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60).<br/> +<span class="id" title="keyword">Notation</span> <a id="f07b3676d96b68749d342542fd80e2b0" class="idref" href="#f07b3676d96b68749d342542fd80e2b0"><span class="id" title="notation">"</span></a>n ** m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60).<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="a647c51c9816a1b44fcfa5312db8344a"><span class="id" title="notation">"</span></a>n ▵ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60).<br/> +<span class="id" title="keyword">Notation</span> <a id="a647c51c9816a1b44fcfa5312db8344a" class="idref" href="#a647c51c9816a1b44fcfa5312db8344a"><span class="id" title="notation">"</span></a>n ▵ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60).<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">"</span></a>n '_' ++ 'x' m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 3).<br/> +<span class="id" title="keyword">Notation</span> <a id="3dd9eae9daa65efe5444f5fc3529a2e7" class="idref" href="#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">"</span></a>n '_' ++ 'x' m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 3).<br/> <br/> -<span class="id" title="keyword">Inductive</span> <a name="eq"><span class="id" title="inductive">eq</span></a> (<span class="id" title="var">A</span>:<span class="id" title="keyword">Type</span>) (<span class="id" title="var">x</span>:<a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a>) : <span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> := <a name="eq_refl"><span class="id" title="constructor">eq_refl</span></a> : <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></span></a><a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a><br/> +<span class="id" title="keyword">Inductive</span> <a id="eq" class="idref" href="#eq"><span class="id" title="inductive">eq</span></a> (<a id="A:3" class="idref" href="#A:3"><span class="id" title="binder">A</span></a>:<span class="id" title="keyword">Type</span>) (<a id="x:4" class="idref" href="#x:4"><span class="id" title="binder">x</span></a>:<a class="idref" href="Coqdoc.links.html#A:3"><span class="id" title="variable">A</span></a>) : <span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> := <a id="eq_refl" class="idref" href="#eq_refl"><span class="id" title="constructor">eq_refl</span></a> : <a class="idref" href="Coqdoc.links.html#x:4"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> <a class="idref" href="Coqdoc.links.html#x:4"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></span></a><a class="idref" href="Coqdoc.links.html#A:3"><span class="id" title="variable">A</span></a><br/> <br/> -<span class="id" title="keyword">where</span> <a name="b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">"</span></a>x = y :> A" := (@<a class="idref" href="Coqdoc.links.html#eq"><span class="id" title="inductive">eq</span></a> <span class="id" title="var">A</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) : <span class="id" title="var">type_scope</span>.<br/> +<span class="id" title="keyword">where</span> <a id="b8b2ebc8e1a8b9aa935c0702efb5dccf" class="idref" href="#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">"</span></a>x = y :> A" := (@<a class="idref" href="Coqdoc.links.html#eq:6"><span class="id" title="inductive">eq</span></a> <span class="id" title="var">A</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) : <span class="id" title="var">type_scope</span>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="eq0"><span class="id" title="definition">eq0</span></a> := 0 <a class="idref" href="Coqdoc.links.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="Coqdoc.links.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a id="eq0" class="idref" href="#eq0"><span class="id" title="definition">eq0</span></a> := 0 <a class="idref" href="Coqdoc.links.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="Coqdoc.links.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">"</span></a>( x # y ; .. ; z )" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#pair"><span class="id" title="constructor">pair</span></a> .. (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#pair"><span class="id" title="constructor">pair</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) .. <span class="id" title="var">z</span>).<br/> +<span class="id" title="keyword">Notation</span> <a id="2c0c193cd2aedf7ecdb713db64dbfce6" class="idref" href="#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">"</span></a>( x # y ; .. ; z )" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#pair"><span class="id" title="constructor">pair</span></a> .. (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#pair"><span class="id" title="constructor">pair</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) .. <span class="id" title="var">z</span>).<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="9f5a1d89cbd4d38f5e289576db7123d1"><span class="id" title="definition">b_α</span></a> := <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Coqdoc.links.html#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">(</span></a>0<a class="idref" href="Coqdoc.links.html#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">#</span></a>0<a class="idref" href="Coqdoc.links.html#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">;</span></a>0<a class="idref" href="Coqdoc.links.html#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a>0 <a class="idref" href="Coqdoc.links.html#f07b3676d96b68749d342542fd80e2b0"><span class="id" title="notation">**</span></a> 0<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">))</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a id="9f5a1d89cbd4d38f5e289576db7123d1" class="idref" href="#9f5a1d89cbd4d38f5e289576db7123d1"><span class="id" title="definition">b_α</span></a> := <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Coqdoc.links.html#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">(</span></a>0<a class="idref" href="Coqdoc.links.html#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">#</span></a>0<a class="idref" href="Coqdoc.links.html#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">;</span></a>0<a class="idref" href="Coqdoc.links.html#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a>0 <a class="idref" href="Coqdoc.links.html#f07b3676d96b68749d342542fd80e2b0"><span class="id" title="notation">**</span></a> 0<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">))</span></a>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="h"><span class="id" title="abbreviation">h</span></a> := <a class="idref" href="Coqdoc.links.html#a"><span class="id" title="definition">a</span></a>.<br/> +<span class="id" title="keyword">Notation</span> <a id="h" class="idref" href="#h"><span class="id" title="abbreviation">h</span></a> := <a class="idref" href="Coqdoc.links.html#a"><span class="id" title="definition">a</span></a>.<br/> <br/> - <span class="id" title="keyword">Section</span> <a name="test"><span class="id" title="section">test</span></a>.<br/> + <span class="id" title="keyword">Section</span> <a id="test" class="idref" href="#test"><span class="id" title="section">test</span></a>.<br/> <br/> - <span class="id" title="keyword">Variables</span> <a name="test.b'"><span class="id" title="variable">b'</span></a> <a name="test.b2"><span class="id" title="variable">b2</span></a>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> + <span class="id" title="keyword">Variables</span> <a id="test.b'" class="idref" href="#test.b'"><span class="id" title="variable">b'</span></a> <a id="test.b2" class="idref" href="#test.b2"><span class="id" title="variable">b2</span></a>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> <br/> - <span class="id" title="keyword">Notation</span> <a name="2158f15740ce05a939b657be222c26d6"><span class="id" title="notation">"</span></a>n + m" := (<span class="id" title="var">n</span> <a class="idref" href="Coqdoc.links.html#a647c51c9816a1b44fcfa5312db8344a"><span class="id" title="notation">▵</span></a> <span class="id" title="var">m</span>) : <span class="id" title="var">my_scope</span>.<br/> + <span class="id" title="keyword">Notation</span> <a id="2158f15740ce05a939b657be222c26d6" class="idref" href="#2158f15740ce05a939b657be222c26d6"><span class="id" title="notation">"</span></a>n + m" := (<span class="id" title="var">n</span> <a class="idref" href="Coqdoc.links.html#a647c51c9816a1b44fcfa5312db8344a"><span class="id" title="notation">▵</span></a> <span class="id" title="var">m</span>) : <span class="id" title="var">my_scope</span>.<br/> <br/> <span class="id" title="keyword">Delimit</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">my_scope</span> <span class="id" title="keyword">with</span> <span class="id" title="var">my</span>.<br/> <br/> - <span class="id" title="keyword">Notation</span> <a name="l"><span class="id" title="abbreviation">l</span></a> := 0.<br/> + <span class="id" title="keyword">Notation</span> <a id="l" class="idref" href="#l"><span class="id" title="abbreviation">l</span></a> := 0.<br/> <br/> - <span class="id" title="keyword">Definition</span> <a name="ab410a966ac148e9b78c65c6cdf301fd"><span class="id" title="definition">α</span></a> := (0 <a class="idref" href="Coqdoc.links.html#2158f15740ce05a939b657be222c26d6"><span class="id" title="notation">+</span></a> <a class="idref" href="Coqdoc.links.html#l"><span class="id" title="abbreviation">l</span></a>)%<span class="id" title="var">my</span>.<br/> + <span class="id" title="keyword">Definition</span> <a id="ab410a966ac148e9b78c65c6cdf301fd" class="idref" href="#ab410a966ac148e9b78c65c6cdf301fd"><span class="id" title="definition">α</span></a> := (0 <a class="idref" href="Coqdoc.links.html#2158f15740ce05a939b657be222c26d6"><span class="id" title="notation">+</span></a> <a class="idref" href="Coqdoc.links.html#l"><span class="id" title="abbreviation">l</span></a>)%<span class="id" title="var">my</span>.<br/> <br/> - <span class="id" title="keyword">Definition</span> <a name="a'"><span class="id" title="definition">a'</span></a> <span class="id" title="var">b</span> := <a class="idref" href="Coqdoc.links.html#test.b'"><span class="id" title="variable">b'</span></a><a class="idref" href="Coqdoc.links.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a>0<a class="idref" href="Coqdoc.links.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a><a class="idref" href="Coqdoc.links.html#test.b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">_</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">++</span></a><a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">x</span></a> <a class="idref" href="Coqdoc.links.html#b"><span class="id" title="variable">b</span></a>.<br/> + <span class="id" title="keyword">Definition</span> <a id="a'" class="idref" href="#a'"><span class="id" title="definition">a'</span></a> <a id="b:9" class="idref" href="#b:9"><span class="id" title="binder">b</span></a> := <a class="idref" href="Coqdoc.links.html#test.b'"><span class="id" title="variable">b'</span></a><a class="idref" href="Coqdoc.links.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a>0<a class="idref" href="Coqdoc.links.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a><a class="idref" href="Coqdoc.links.html#test.b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">_</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">++</span></a><a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">x</span></a> <a class="idref" href="Coqdoc.links.html#b:9"><span class="id" title="variable">b</span></a>.<br/> <br/> - <span class="id" title="keyword">Definition</span> <a name="c"><span class="id" title="definition">c</span></a> := <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">}+{</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">}</span></a>.<br/> + <span class="id" title="keyword">Definition</span> <a id="c" class="idref" href="#c"><span class="id" title="definition">c</span></a> := <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">}+{</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">}</span></a>.<br/> <br/> - <span class="id" title="keyword">Definition</span> <a name="d"><span class="id" title="definition">d</span></a> := (1<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a>2)%<span class="id" title="var">nat</span>.<br/> + <span class="id" title="keyword">Definition</span> <a id="d" class="idref" href="#d"><span class="id" title="definition">d</span></a> := (1<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a>2)%<span class="id" title="var">nat</span>.<br/> <br/> - <span class="id" title="keyword">Lemma</span> <a name="e"><span class="id" title="lemma">e</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e03f39daf98516fa530d3f6f5a1b4d92"><span class="id" title="notation">+</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> + <span class="id" title="keyword">Lemma</span> <a id="e" class="idref" href="#e"><span class="id" title="lemma">e</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e03f39daf98516fa530d3f6f5a1b4d92"><span class="id" title="notation">+</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> <span class="id" title="var">Admitted</span>.<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="Coqdoc.links.html#test"><span class="id" title="section">test</span></a>.<br/> <br/> - <span class="id" title="keyword">Section</span> <a name="test2"><span class="id" title="section">test2</span></a>.<br/> + <span class="id" title="keyword">Section</span> <a id="test2" class="idref" href="#test2"><span class="id" title="section">test2</span></a>.<br/> <br/> - <span class="id" title="keyword">Variables</span> <a name="test2.b'"><span class="id" title="variable">b'</span></a>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> + <span class="id" title="keyword">Variables</span> <a id="test2.b'" class="idref" href="#test2.b'"><span class="id" title="variable">b'</span></a>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> <br/> - <span class="id" title="keyword">Section</span> <a name="test2.test"><span class="id" title="section">test</span></a>.<br/> + <span class="id" title="keyword">Section</span> <a id="test2.test" class="idref" href="#test2.test"><span class="id" title="section">test</span></a>.<br/> <br/> - <span class="id" title="keyword">Variables</span> <a name="test2.test.b2"><span class="id" title="variable">b2</span></a>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> + <span class="id" title="keyword">Variables</span> <a id="test2.test.b2" class="idref" href="#test2.test.b2"><span class="id" title="variable">b2</span></a>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> <br/> - <span class="id" title="keyword">Definition</span> <a name="a''"><span class="id" title="definition">a''</span></a> <span class="id" title="var">b</span> := <a class="idref" href="Coqdoc.links.html#test2.b'"><span class="id" title="variable">b'</span></a> <a class="idref" href="Coqdoc.links.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#O"><span class="id" title="constructor">O</span></a> <a class="idref" href="Coqdoc.links.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a> <a class="idref" href="Coqdoc.links.html#test2.test.b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">_</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">++</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">x</span></a> <a class="idref" href="Coqdoc.links.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="Coqdoc.links.html#h"><span class="id" title="abbreviation">h</span></a> 0.<br/> + <span class="id" title="keyword">Definition</span> <a id="a''" class="idref" href="#a''"><span class="id" title="definition">a''</span></a> <a id="b:12" class="idref" href="#b:12"><span class="id" title="binder">b</span></a> := <a class="idref" href="Coqdoc.links.html#test2.b'"><span class="id" title="variable">b'</span></a> <a class="idref" href="Coqdoc.links.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#O"><span class="id" title="constructor">O</span></a> <a class="idref" href="Coqdoc.links.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a> <a class="idref" href="Coqdoc.links.html#test2.test.b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">_</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">++</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">x</span></a> <a class="idref" href="Coqdoc.links.html#b:12"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="Coqdoc.links.html#h"><span class="id" title="abbreviation">h</span></a> 0.<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="Coqdoc.links.html#test2.test"><span class="id" title="section">test</span></a>.<br/> diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out index 24f96ff1e6..2304f5ecc1 100644 --- a/test-suite/coqdoc/links.tex.out +++ b/test-suite/coqdoc/links.tex.out @@ -45,10 +45,10 @@ Various checks for coqdoc \coqdockw{Definition} \coqdef{Coqdoc.links.g}{g}{\coqdocdefinition{g}} := "dfjkh""sdfhj forall <> * \~{}"\%\coqdocvar{string}.\coqdoceol \coqdocemptyline \coqdocnoindent -\coqdockw{Definition} \coqdef{Coqdoc.links.a}{a}{\coqdocdefinition{a}} (\coqdocvar{b}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}) := \coqdocvariable{b}.\coqdoceol +\coqdockw{Definition} \coqdef{Coqdoc.links.a}{a}{\coqdocdefinition{a}} (\coqdef{Coqdoc.links.b:1}{b}{\coqdocbinder{b}}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}) := \coqref{Coqdoc.links.b:1}{\coqdocvariable{b}}.\coqdoceol \coqdocemptyline \coqdocnoindent -\coqdockw{Definition} \coqdef{Coqdoc.links.f}{f}{\coqdocdefinition{f}} := \coqdockw{\ensuremath{\forall}} \coqdocvar{C}:\coqdockw{Prop}, \coqdocvariable{C}.\coqdoceol +\coqdockw{Definition} \coqdef{Coqdoc.links.f}{f}{\coqdocdefinition{f}} := \coqdockw{\ensuremath{\forall}} \coqdef{Coqdoc.links.C:2}{C}{\coqdocbinder{C}}:\coqdockw{Prop}, \coqref{Coqdoc.links.C:2}{\coqdocvariable{C}}.\coqdoceol \coqdocemptyline \coqdocnoindent \coqdockw{Notation} \coqdef{Coqdoc.links.:::x '++' x}{"}{"}n ++ m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}).\coqdoceol @@ -65,11 +65,11 @@ Various checks for coqdoc \coqdockw{Notation} \coqdef{Coqdoc.links.:::x ''' ''' '++' 'x' x}{"}{"}n '\_' ++ 'x' m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 3).\coqdoceol \coqdocemptyline \coqdocnoindent -\coqdockw{Inductive} \coqdef{Coqdoc.links.eq}{eq}{\coqdocinductive{eq}} (\coqdocvar{A}:\coqdockw{Type}) (\coqdocvar{x}:\coqdocvariable{A}) : \coqdocvar{A} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqdockw{Prop} := \coqdef{Coqdoc.links.eq refl}{eq\_refl}{\coqdocconstructor{eq\_refl}} : \coqdocvariable{x} \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{=}} \coqdocvariable{x} \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{:>}}\coqdocvariable{A}\coqdoceol +\coqdockw{Inductive} \coqdef{Coqdoc.links.eq}{eq}{\coqdocinductive{eq}} (\coqdef{Coqdoc.links.A:3}{A}{\coqdocbinder{A}}:\coqdockw{Type}) (\coqdef{Coqdoc.links.x:4}{x}{\coqdocbinder{x}}:\coqref{Coqdoc.links.A:3}{\coqdocvariable{A}}) : \coqdocvar{A} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqdockw{Prop} := \coqdef{Coqdoc.links.eq refl}{eq\_refl}{\coqdocconstructor{eq\_refl}} : \coqref{Coqdoc.links.x:4}{\coqdocvariable{x}} \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{=}} \coqref{Coqdoc.links.x:4}{\coqdocvariable{x}} \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{:>}}\coqref{Coqdoc.links.A:3}{\coqdocvariable{A}}\coqdoceol \coqdocnoindent \coqdoceol \coqdocnoindent -\coqdockw{where} \coqdef{Coqdoc.links.::type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqref{Coqdoc.links.eq}{\coqdocinductive{eq}} \coqdocvar{A} \coqdocvar{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol +\coqdockw{where} \coqdef{Coqdoc.links.::type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqref{Coqdoc.links.eq:6}{\coqdocinductive{eq}} \coqdocvar{A} \coqdocvar{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol \coqdocemptyline \coqdocnoindent \coqdockw{Definition} \coqdef{Coqdoc.links.eq0}{eq0}{\coqdocdefinition{eq0}} := 0 \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{=}} 0 \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{:>}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol @@ -102,7 +102,7 @@ Various checks for coqdoc \coqdockw{Definition} \coqdef{Coqdoc.links.xCExB1}{α}{\coqdocdefinition{α}} := (0 \coqref{Coqdoc.links.test.::my scope:x '+' x}{\coqdocnotation{+}} \coqref{Coqdoc.links.l}{\coqdocabbreviation{l}})\%\coqdocvar{my}.\coqdoceol \coqdocemptyline \coqdocindent{2.00em} -\coqdockw{Definition} \coqdef{Coqdoc.links.a'}{a'}{\coqdocdefinition{a'}} \coqdocvar{b} := \coqdocvariable{b'}\coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}}0\coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}}\coqdocvariable{b2} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{++}}\coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqdocvariable{b}.\coqdoceol +\coqdockw{Definition} \coqdef{Coqdoc.links.a'}{a'}{\coqdocdefinition{a'}} \coqdef{Coqdoc.links.b:9}{b}{\coqdocbinder{b}} := \coqref{Coqdoc.links.test.b'}{\coqdocvariable{b'}}\coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}}0\coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}}\coqref{Coqdoc.links.test.b2}{\coqdocvariable{b2}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{++}}\coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqref{Coqdoc.links.b:9}{\coqdocvariable{b}}.\coqdoceol \coqdocemptyline \coqdocindent{2.00em} \coqdockw{Definition} \coqdef{Coqdoc.links.c}{c}{\coqdocdefinition{c}} := \coqexternalref{::type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\{}}\coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}\coqexternalref{::type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\}+\{}}\coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}\coqexternalref{::type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\}}}.\coqdoceol @@ -131,7 +131,7 @@ Various checks for coqdoc \coqdockw{Variables} \coqdef{Coqdoc.links.test2.test.b2}{b2}{\coqdocvariable{b2}}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol \coqdocemptyline \coqdocindent{3.00em} -\coqdockw{Definition} \coqdef{Coqdoc.links.a''}{a'{}'}{\coqdocdefinition{a'{}'}} \coqdocvar{b} := \coqdocvariable{b'} \coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}} \coqexternalref{O}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{O}} \coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}} \coqdocvariable{b2} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{++}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqdocvariable{b} \coqexternalref{::nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}} \coqref{Coqdoc.links.h}{\coqdocabbreviation{h}} 0.\coqdoceol +\coqdockw{Definition} \coqdef{Coqdoc.links.a''}{a'{}'}{\coqdocdefinition{a'{}'}} \coqdef{Coqdoc.links.b:12}{b}{\coqdocbinder{b}} := \coqref{Coqdoc.links.test2.b'}{\coqdocvariable{b'}} \coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}} \coqexternalref{O}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{O}} \coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}} \coqref{Coqdoc.links.test2.test.b2}{\coqdocvariable{b2}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{++}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqref{Coqdoc.links.b:12}{\coqdocvariable{b}} \coqexternalref{::nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}} \coqref{Coqdoc.links.h}{\coqdocabbreviation{h}} 0.\coqdoceol \coqdocemptyline \coqdocindent{2.00em} \coqdockw{End} \coqref{Coqdoc.links.test2.test}{\coqdocsection{test}}.\coqdoceol diff --git a/test-suite/output/undeclared_key.out b/test-suite/output/undeclared_key.out new file mode 100644 index 0000000000..ed768751fc --- /dev/null +++ b/test-suite/output/undeclared_key.out @@ -0,0 +1,13 @@ +The command has indeed failed with message: +There is no flag, option or table with this name: "Search Blacklists". +The command has indeed failed with message: +There is no qualid-valued table with this name: "Search Blacklist". +File "stdin", line 3, characters 0-22: +Warning: There is no flag or option with this name: "Search Blacklists". +[unknown-option,option] +The command has indeed failed with message: +There is no string-valued table with this name: "Search Blacklists". +The command has indeed failed with message: +There is no qualid-valued table with this name: "Search Blacklist". +The command has indeed failed with message: +There is no qualid-valued table with this name: "Search Blacklist". diff --git a/test-suite/output/undeclared_key.v b/test-suite/output/undeclared_key.v new file mode 100644 index 0000000000..4134bc8bfa --- /dev/null +++ b/test-suite/output/undeclared_key.v @@ -0,0 +1,6 @@ +Fail Test Search Blacklists. +Fail Test Search Blacklist for foo. +Set Search Blacklists. +Fail Remove Search Blacklists "bar" foo. +Fail Remove Search Blacklist "bar" foo. +Fail Add Search Blacklist "bar" foo. diff --git a/theories/Logic/WKL.v b/theories/Logic/WKL.v index 478bc434ad..d9eea2f89d 100644 --- a/theories/Logic/WKL.v +++ b/theories/Logic/WKL.v @@ -25,7 +25,7 @@ Require Import WeakFan List. Import ListNotations. -Require Import Omega. +Require Import Arith. (** [is_path_from P n l] means that there exists a path of length [n] from [l] on which [P] does not hold *) diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v index 466e2bf994..443931e5bb 100644 --- a/theories/Vectors/VectorSpec.v +++ b/theories/Vectors/VectorSpec.v @@ -15,7 +15,7 @@ *) Require Fin. -Require Import VectorDef. +Require Import VectorDef PeanoNat Eqdep_dec. Import VectorNotations. Definition cons_inj {A} {a1 a2} {n} {v1 v2 : t A n} @@ -32,6 +32,8 @@ Defined. (** Lemmas are done for functions that use [Fin.t] but thanks to [Peano_dec.le_unique], all is true for the one that use [lt] *) +(** ** Properties of [nth] and [nth_order] *) + Lemma eq_nth_iff A n (v1 v2: t A n): (forall p1 p2, p1 = p2 -> v1 [@ p1 ] = v2 [@ p2 ]) <-> v1 = v2. Proof. @@ -44,12 +46,35 @@ split. - intros; now f_equal. Qed. +Lemma nth_order_hd A: forall n (v : t A (S n)) (H : 0 < S n), + nth_order v H = hd v. +Proof. intros; now rewrite (eta v). Qed. + +Lemma nth_order_tl A: forall n k (v : t A (S n)) (H : k < n) (HS : S k < S n), + nth_order (tl v) H = nth_order v HS. +Proof. +induction n; intros. +- inversion H. +- rewrite (eta v). + unfold nth_order; simpl. + now rewrite (Fin.of_nat_ext H (Lt.lt_S_n _ _ HS)). +Qed. + Lemma nth_order_last A: forall n (v: t A (S n)) (H: n < S n), nth_order v H = last v. Proof. unfold nth_order; refine (@rectS _ _ _ _); now simpl. Qed. +Lemma nth_order_ext A: forall n k (v : t A n) (H1 H2 : k < n), + nth_order v H1 = nth_order v H2. +Proof. +intros; unfold nth_order. +now rewrite (Fin.of_nat_ext H1 H2). +Qed. + +(** ** Properties of [shiftin] and [shiftrepeat] *) + Lemma shiftin_nth A a n (v: t A n) k1 k2 (eq: k1 = k2): nth (shiftin a v) (Fin.L_R 1 k1) = nth v k2. Proof. @@ -82,11 +107,99 @@ Proof. refine (@rectS _ _ _ _); now simpl. Qed. +(** ** Properties of [replace] *) + +Lemma nth_order_replace_eq A: forall n k (v : t A n) a (H1 : k < n) (H2 : k < n), + nth_order (replace v (Fin.of_nat_lt H2) a) H1 = a. +Proof. +intros n k; revert n; induction k; intros; + (destruct n; [ inversion H1 | subst ]). +- now rewrite nth_order_hd, (eta v). +- rewrite <- (nth_order_tl _ _ _ _ (proj2 (Nat.succ_lt_mono _ _) H1)), (eta v). + apply IHk. +Qed. + +Lemma nth_order_replace_neq A: forall n k1 k2, k1 <> k2 -> + forall (v : t A n) a (H1 : k1 < n) (H2 : k2 < n), + nth_order (replace v (Fin.of_nat_lt H2) a) H1 = nth_order v H1. +Proof. +intros n k1; revert n; induction k1; intros; + (destruct n ; [ inversion H1 | subst ]). +- rewrite 2 nth_order_hd. + destruct k2; intuition. + now rewrite 2 (eta v). +- rewrite <- 2 (nth_order_tl _ _ _ _ (proj2 (Nat.succ_lt_mono _ _) H1)), (eta v). + destruct k2; auto. + apply IHk1. + intros Hk; apply H; now subst. +Qed. + +Lemma replace_id A: forall n p (v : t A n), + replace v p (nth v p) = v. +Proof. +induction p; intros; rewrite 2 (eta v); simpl; auto. +now rewrite IHp. +Qed. + +Lemma replace_replace_eq A: forall n p (v : t A n) a b, + replace (replace v p a) p b = replace v p b. +Proof. +intros. +induction p; rewrite 2 (eta v); simpl; auto. +now rewrite IHp. +Qed. + +Lemma replace_replace_neq A: forall n p1 p2 (v : t A n) a b, p1 <> p2 -> + replace (replace v p1 a) p2 b = replace (replace v p2 b) p1 a. +Proof. +apply (Fin.rect2 (fun n p1 p2 => forall v a b, + p1 <> p2 -> replace (replace v p1 a) p2 b = replace (replace v p2 b) p1 a)). +- intros n v a b Hneq. + now contradiction Hneq. +- intros n p2 v; revert n v p2. + refine (@rectS _ _ _ _); auto. +- intros n p1 v; revert n v p1. + refine (@rectS _ _ _ _); auto. +- intros n p1 p2 IH v; revert n v p1 p2 IH. + refine (@rectS _ _ _ _); simpl; do 6 intro; [ | do 3 intro ]; intro Hneq; + f_equal; apply IH; intros Heq; apply Hneq; now subst. +Qed. + +(** ** Properties of [const] *) + Lemma const_nth A (a: A) n (p: Fin.t n): (const a n)[@ p] = a. Proof. now induction p. Qed. +(** ** Properties of [map] *) + +Lemma map_id A: forall n (v : t A n), + map (fun x => x) v = v. +Proof. +induction v; simpl; [ | rewrite IHv ]; auto. +Qed. + +Lemma map_map A B C: forall (f:A->B) (g:B->C) n (v : t A n), + map g (map f v) = map (fun x => g (f x)) v. +Proof. +induction v; simpl; [ | rewrite IHv ]; auto. +Qed. + +Lemma map_ext_in A B: forall (f g:A->B) n (v : t A n), + (forall a, In a v -> f a = g a) -> map f v = map g v. +Proof. +induction v; simpl; auto. +intros; rewrite H by constructor; rewrite IHv; intuition. +apply H; now constructor. +Qed. + +Lemma map_ext A B: forall (f g:A->B), (forall a, f a = g a) -> + forall n (v : t A n), map f v = map g v. +Proof. +intros; apply map_ext_in; auto. +Qed. + Lemma nth_map {A B} (f: A -> B) {n} v (p1 p2: Fin.t n) (eq: p1 = p2): (map f v) [@ p1] = f (v [@ p2]). Proof. @@ -105,6 +218,8 @@ refine (@rect2 _ _ _ _ _); simpl. now simpl. Qed. +(** ** Properties of [fold_left] *) + Lemma fold_left_right_assoc_eq {A B} {f: A -> B -> A} (assoc: forall a b c, f (f a b) c = f (f a c) b) {n} (v: t B n): forall a, fold_left f a v = fold_right (fun x y => f y x) v a. @@ -118,6 +233,8 @@ assert (forall n h (v: t B n) a, fold_left f (f a h) v = f (fold_left f a v) h). + simpl. intros; now rewrite<- (IHv). Qed. +(** ** Properties of [to_list] *) + Lemma to_list_of_list_opp {A} (l: list A): to_list (of_list l) = l. Proof. induction l. @@ -125,6 +242,8 @@ induction l. - unfold to_list; simpl. now f_equal. Qed. +(** ** Properties of [take] *) + Lemma take_O : forall {A} {n} le (v:t A n), take 0 le v = []. Proof. reflexivity. @@ -153,10 +272,14 @@ Proof. - destruct v. inversion le. simpl. apply f_equal. apply IHp. Qed. +(** ** Properties of [uncons] and [splitat] *) + Lemma uncons_cons {A} : forall {n : nat} (a : A) (v : t A n), uncons (a::v) = (a,v). Proof. reflexivity. Qed. +(* [append] *) + Lemma append_comm_cons {A} : forall {n m : nat} (v : t A n) (w : t A m) (a : A), a :: (v ++ w) = (a :: v) ++ w. Proof. reflexivity. Qed. @@ -187,3 +310,80 @@ Proof with auto. f_equal... apply IHv... Qed. + +(** ** Properties of [Forall] and [Forall2] *) + +Lemma Forall_impl A: forall (P Q : A -> Prop), (forall a, P a -> Q a) -> + forall n (v : t A n), Forall P v -> Forall Q v. +Proof. +induction v; intros HP; constructor; inversion HP as [| ? ? ? ? ? Heq1 [Heq2 He]]; + apply (inj_pair2_eq_dec _ Nat.eq_dec) in He; subst; intuition. +Qed. + +Lemma Forall_forall A: forall P n (v : t A n), + Forall P v <-> forall a, In a v -> P a. +Proof. +intros P n v; split. +- intros HP a Hin. + revert HP; induction Hin; intros HP; + inversion HP as [| ? ? ? ? ? Heq1 [Heq2 He]]; subst; auto. + apply (inj_pair2_eq_dec _ Nat.eq_dec) in He; subst; auto. +- induction v; intros Hin; constructor. + + apply Hin; constructor. + + apply IHv; intros a Ha. + apply Hin; now constructor. +Qed. + +Lemma Forall_nth_order A: forall P n (v : t A n), + Forall P v <-> forall i (Hi : i < n), P (nth_order v Hi). +Proof. +split; induction n. +- intros HF i Hi; inversion Hi. +- intros HF i Hi. + rewrite (eta v). + rewrite (eta v) in HF. + inversion HF as [| ? ? ? ? ? Heq1 [Heq2 He]]; subst. + apply (inj_pair2_eq_dec _ Nat.eq_dec) in He ; subst. + destruct i. + + now rewrite nth_order_hd. + + rewrite <- (nth_order_tl _ _ _ _ (proj2 (Nat.succ_lt_mono _ _) Hi) Hi). + now apply IHn. +- intros HP; apply case0; constructor. +- intros HP. + rewrite (eta v) in HP. + rewrite (eta v); constructor. + + specialize HP with 0 (Nat.lt_0_succ n). + now rewrite nth_order_hd in HP. + + apply IHn; intros. + specialize HP with (S i) (proj1 (Nat.succ_lt_mono _ _) Hi). + now rewrite <- (nth_order_tl _ _ _ _ Hi) in HP. +Qed. + +Lemma Forall2_nth_order A: forall P n (v1 v2 : t A n), + Forall2 P v1 v2 + <-> forall i (Hi1 : i < n) (Hi2 : i < n), P (nth_order v1 Hi1) (nth_order v2 Hi2). +Proof. +split; induction n. +- intros HF i Hi1 Hi2; inversion Hi1. +- intros HF i Hi1 Hi2. + rewrite (eta v1), (eta v2). + rewrite (eta v1), (eta v2) in HF. + inversion HF as [| ? ? ? ? ? ? ? Heq [Heq1 He1] [Heq2 He2]]. + apply (inj_pair2_eq_dec _ Nat.eq_dec) in He1. + apply (inj_pair2_eq_dec _ Nat.eq_dec) in He2; subst. + destruct i. + + now rewrite nth_order_hd. + + rewrite <- (nth_order_tl _ _ _ _ (proj2 (Nat.succ_lt_mono _ _) Hi1) Hi1). + rewrite <- (nth_order_tl _ _ _ _ (proj2 (Nat.succ_lt_mono _ _) Hi2) Hi2). + now apply IHn. +- intros _; revert v1; apply case0; revert v2; apply case0; constructor. +- intros HP. + rewrite (eta v1), (eta v2) in HP. + rewrite (eta v1), (eta v2); constructor. + + specialize HP with 0 (Nat.lt_0_succ _) (Nat.lt_0_succ _). + now rewrite nth_order_hd in HP. + + apply IHn; intros. + specialize HP with (S i) (proj1 (Nat.succ_lt_mono _ _) Hi1) + (proj1 (Nat.succ_lt_mono _ _) Hi2). + now rewrite <- (nth_order_tl _ _ _ _ Hi1), <- (nth_order_tl _ _ _ _ Hi2) in HP. +Qed. diff --git a/theories/micromega/ZArith_hints.v b/theories/micromega/ZArith_hints.v new file mode 100644 index 0000000000..a6d3d92a99 --- /dev/null +++ b/theories/micromega/ZArith_hints.v @@ -0,0 +1,43 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +Require Import Lia. +Import ZArith_base. + +Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l + Z.add_0_r Z.mul_1_l Z.add_opp_diag_l Z.add_opp_diag_r Z.mul_add_distr_r + Z.mul_add_distr_l: zarith. + +Require Export Zhints. + +Hint Extern 10 (_ = _ :>nat) => abstract lia: zarith. +Hint Extern 10 (_ <= _) => abstract lia: zarith. +Hint Extern 10 (_ < _) => abstract lia: zarith. +Hint Extern 10 (_ >= _) => abstract lia: zarith. +Hint Extern 10 (_ > _) => abstract lia: zarith. + +Hint Extern 10 (_ <> _ :>nat) => abstract lia: zarith. +Hint Extern 10 (~ _ <= _) => abstract lia: zarith. +Hint Extern 10 (~ _ < _) => abstract lia: zarith. +Hint Extern 10 (~ _ >= _) => abstract lia: zarith. +Hint Extern 10 (~ _ > _) => abstract lia: zarith. + +Hint Extern 10 (_ = _ :>Z) => abstract lia: zarith. +Hint Extern 10 (_ <= _)%Z => abstract lia: zarith. +Hint Extern 10 (_ < _)%Z => abstract lia: zarith. +Hint Extern 10 (_ >= _)%Z => abstract lia: zarith. +Hint Extern 10 (_ > _)%Z => abstract lia: zarith. + +Hint Extern 10 (_ <> _ :>Z) => abstract lia: zarith. +Hint Extern 10 (~ (_ <= _)%Z) => abstract lia: zarith. +Hint Extern 10 (~ (_ < _)%Z) => abstract lia: zarith. +Hint Extern 10 (~ (_ >= _)%Z) => abstract lia: zarith. +Hint Extern 10 (~ (_ > _)%Z) => abstract lia: zarith. + +Hint Extern 10 False => abstract lia: zarith. diff --git a/theories/omega/Omega.v b/theories/omega/Omega.v index 10a5aa47b3..5c52284621 100644 --- a/theories/omega/Omega.v +++ b/theories/omega/Omega.v @@ -19,38 +19,6 @@ Require Export ZArith_base. Require Export OmegaLemmas. Require Export PreOmega. -Require Import Lia. +Require Export ZArith_hints. Declare ML Module "omega_plugin". - -Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l - Z.add_0_r Z.mul_1_l Z.add_opp_diag_l Z.add_opp_diag_r Z.mul_add_distr_r - Z.mul_add_distr_l: zarith. - -Require Export Zhints. - -Hint Extern 10 (_ = _ :>nat) => abstract lia: zarith. -Hint Extern 10 (_ <= _) => abstract lia: zarith. -Hint Extern 10 (_ < _) => abstract lia: zarith. -Hint Extern 10 (_ >= _) => abstract lia: zarith. -Hint Extern 10 (_ > _) => abstract lia: zarith. - -Hint Extern 10 (_ <> _ :>nat) => abstract lia: zarith. -Hint Extern 10 (~ _ <= _) => abstract lia: zarith. -Hint Extern 10 (~ _ < _) => abstract lia: zarith. -Hint Extern 10 (~ _ >= _) => abstract lia: zarith. -Hint Extern 10 (~ _ > _) => abstract lia: zarith. - -Hint Extern 10 (_ = _ :>Z) => abstract lia: zarith. -Hint Extern 10 (_ <= _)%Z => abstract lia: zarith. -Hint Extern 10 (_ < _)%Z => abstract lia: zarith. -Hint Extern 10 (_ >= _)%Z => abstract lia: zarith. -Hint Extern 10 (_ > _)%Z => abstract lia: zarith. - -Hint Extern 10 (_ <> _ :>Z) => abstract lia: zarith. -Hint Extern 10 (~ (_ <= _)%Z) => abstract lia: zarith. -Hint Extern 10 (~ (_ < _)%Z) => abstract lia: zarith. -Hint Extern 10 (~ (_ >= _)%Z) => abstract lia: zarith. -Hint Extern 10 (~ (_ > _)%Z) => abstract lia: zarith. - -Hint Extern 10 False => abstract lia: zarith. diff --git a/theories/setoid_ring/Rings_Z.v b/theories/setoid_ring/Rings_Z.v index f489b00145..372bba7926 100644 --- a/theories/setoid_ring/Rings_Z.v +++ b/theories/setoid_ring/Rings_Z.v @@ -11,7 +11,6 @@ Require Export Cring. Require Export Integral_domain. Require Export Ncring_initial. -Require Export Omega. Instance Zcri: (Cring (Rr:=Zr)). red. exact Z.mul_comm. Defined. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 597351db9b..745bbb7e55 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -66,12 +66,12 @@ VERBOSE ?= TIMED?= TIMECMD?= # Use command time on linux, gtime on Mac OS -TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)" +TIMEFMT?="$@ (real: %e, user: %U, sys: %S, mem: %M ko)" ifneq (,$(TIMED)) -ifeq (0,$(shell command time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) +ifeq (0,$(shell command time -f "" true >/dev/null 2>/dev/null; echo $$?)) STDTIME?=command time -f $(TIMEFMT) else -ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) +ifeq (0,$(shell gtime -f "" true >/dev/null 2>/dev/null; echo $$?)) STDTIME?=gtime -f $(TIMEFMT) else STDTIME?=command time diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css index dbc930f5ec..48096e555a 100644 --- a/tools/coqdoc/coqdoc.css +++ b/tools/coqdoc/coqdoc.css @@ -230,6 +230,10 @@ tr.infrulemiddle hr { color: rgb(40%,0%,40%); } +.id[title="binder"] { + color: rgb(40%,0%,40%); +} + .id[type="definition"] { color: rgb(0%,40%,0%); } @@ -327,3 +331,8 @@ ul.doclist { margin-top: 0em; margin-bottom: 0em; } + +.code :target { + border: 2px solid #D4D4D4; + background-color: #e5eecc; +} diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty index f49f9f0066..aa9c414761 100644 --- a/tools/coqdoc/coqdoc.sty +++ b/tools/coqdoc/coqdoc.sty @@ -72,6 +72,7 @@ \newcommand{\coqdocinductive}[1]{\coqdocind{#1}} \newcommand{\coqdocdefinition}[1]{\coqdoccst{#1}} \newcommand{\coqdocvariable}[1]{\coqdocvar{#1}} +\newcommand{\coqdocbinder}[1]{\coqdocvar{#1}} \newcommand{\coqdocconstructor}[1]{\coqdocconstr{#1}} \newcommand{\coqdoclemma}[1]{\coqdoccst{#1}} \newcommand{\coqdocclass}[1]{\coqdocind{#1}} diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index 4cc82726f1..723918525d 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -31,6 +31,7 @@ type entry_type = | Abbreviation | Notation | Section + | Binder type index_entry = | Def of string * entry_type @@ -177,6 +178,7 @@ let type_name = function | Abbreviation -> "abbreviation" | Notation -> "notation" | Section -> "section" + | Binder -> "binder" let prepare_entry s = function | Notation -> @@ -268,6 +270,7 @@ let type_of_string = function | "mod" | "modtype" -> Module | "tac" -> TacticDefinition | "sec" -> Section + | "binder" -> Binder | s -> invalid_arg ("type_of_string:" ^ s) let ill_formed_glob_file f = diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli index 3426fdd3d3..7a3d401fd7 100644 --- a/tools/coqdoc/index.mli +++ b/tools/coqdoc/index.mli @@ -30,6 +30,7 @@ type entry_type = | Abbreviation | Notation | Section + | Binder val type_name : entry_type -> string diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index dd1b65d294..d6f51d7b78 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -337,11 +337,8 @@ module Latex = struct let id = if fid <> "" then (m ^ "." ^ fid) else m in match find_module m with | Local -> - if typ = Variable then - printf "\\coqdoc%s{%s}" (type_name typ) s - else - (printf "\\coqref{"; label_ident id; - printf "}{\\coqdoc%s{%s}}" (type_name typ) s) + printf "\\coqref{"; label_ident id; + printf "}{\\coqdoc%s{%s}}" (type_name typ) s | External m when !externals -> printf "\\coqexternalref{"; label_ident fid; printf "}{%s}{\\coqdoc%s{%s}}" (escaped m) (type_name typ) s @@ -615,6 +612,7 @@ module Html = struct else match s.[i] with | 'a'..'z' | 'A'..'Z' | '0'..'9' | '.' | '_' -> loop esc (i-1) | '<' | '>' | '&' | '\'' | '\"' -> loop true (i-1) + | '-' | ':' -> loop esc (i-1) (* should be safe in HTML5 attribute name syntax *) | _ -> (* This name contains complex characters: this is probably a notation string, we simply hash it. *) @@ -661,7 +659,8 @@ module Html = struct let reference s r = match r with | Def (fullid,ty) -> - printf "<a name=\"%s\">" (sanitize_name fullid); + let s' = sanitize_name fullid in + printf "<a id=\"%s\" class=\"idref\" href=\"#%s\">" s' s'; printf "<span class=\"id\" title=\"%s\">%s</span></a>" (type_name ty) s | Ref (m,fullid,ty) -> ident_ref m fullid (type_name ty) s diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 1e2e2e53e2..43e86fa9bd 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -161,7 +161,7 @@ let do_assumptions ~program_mode ~poly ~scope ~kind nl l = let env = EConstr.push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (make_annot id r,t)) idl) env in let ienv = List.fold_right (fun {CAst.v=id} ienv -> - let impls = compute_internalization_data env sigma Variable t imps in + let impls = compute_internalization_data env sigma id Variable t imps in Id.Map.add id impls ienv) idl ienv in ((sigma,env,ienv),((is_coe,idl),t,imps))) (sigma,env,empty_internalization_env) l diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 80e7e6ab96..bf38088f71 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -195,13 +195,14 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = let lift_lets = lift_rel_context 1 letbinders in let sigma, intern_body = let ctx = LocalAssum (make_annot (Name recname) Sorts.Relevant, get_type curry_fun) :: binders_rel in - let (r, impls, scopes) = - Constrintern.compute_internalization_data env sigma + let interning_data = + Constrintern.compute_internalization_data env sigma recname Constrintern.Recursive full_arity impls in let newimpls = Id.Map.singleton recname - (r, impls @ [Some (ExplByName (Id.of_string "recproof"), Impargs.Manual, (true, false))], - scopes @ [None]) in + (Constrintern.extend_internalization_data interning_data + (Some (ExplByName (Id.of_string "recproof"), Impargs.Manual, (true, false))) + None) in interp_casted_constr_evars ~program_mode:true (push_rel_context ctx env) sigma ~impls:newimpls body (lift 1 top_arity) in diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 08ba49f92b..13145d3757 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -938,23 +938,23 @@ GRAMMAR EXTEND Gram | IDENT "Print"; IDENT "Table"; table = option_table -> { VernacPrintOption table } - | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 option_ref_value + | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 table_value -> { VernacAddOption ([table;field], v) } (* A global value below will be hidden by a field above! *) (* In fact, we give priority to secondary tables *) (* No syntax for tertiary tables due to conflict *) (* (but they are unused anyway) *) - | IDENT "Add"; table = IDENT; v = LIST1 option_ref_value -> + | IDENT "Add"; table = IDENT; v = LIST1 table_value -> { VernacAddOption ([table], v) } - | IDENT "Test"; table = option_table; "for"; v = LIST1 option_ref_value + | IDENT "Test"; table = option_table; "for"; v = LIST1 table_value -> { VernacMemOption (table, v) } | IDENT "Test"; table = option_table -> { VernacPrintOption table } - | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value + | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 table_value -> { VernacRemoveOption ([table;field], v) } - | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value -> + | IDENT "Remove"; table = IDENT; v = LIST1 table_value -> { VernacRemoveOption ([table], v) } ]] ; query_command: (* TODO: rapprocher Eval et Check *) @@ -1047,9 +1047,9 @@ GRAMMAR EXTEND Gram | n = integer -> { OptionSetInt n } | s = STRING -> { OptionSetString s } ] ] ; - option_ref_value: - [ [ id = global -> { QualidRefValue id } - | s = STRING -> { StringRefValue s } ] ] + table_value: + [ [ id = global -> { Goptions.QualidRefValue id } + | s = STRING -> { Goptions.StringRefValue s } ] ] ; option_table: [ [ fl = LIST1 [ x = IDENT -> { x } ] -> { fl } ]] diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 7a2e6d8b03..36d79bfdb1 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -168,8 +168,8 @@ open Pputils keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search sl ++ pr_in_out_modules b let pr_option_ref_value = function - | QualidRefValue id -> pr_qualid id - | StringRefValue s -> qs s + | Goptions.QualidRefValue id -> pr_qualid id + | Goptions.StringRefValue s -> qs s let pr_printoption table b = prlist_with_sep spc str table ++ diff --git a/vernac/record.ml b/vernac/record.ml index 0b6e8cd8c1..9fda98d08e 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -71,7 +71,7 @@ let interp_fields_evars env sigma ~ninds ~nparams impls_env nots l = let impls = match i with | Anonymous -> impls - | Name id -> Id.Map.add id (compute_internalization_data env sigma Constrintern.Method t' impl) impls + | Name id -> Id.Map.add id (compute_internalization_data env sigma id Constrintern.Method t' impl) impls in let d = match b' with | None -> LocalAssum (make_annot i r,t') diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 044e479aeb..3926b91a55 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1554,26 +1554,11 @@ let vernac_set_option ~locality table v = match v with vernac_set_option0 ~locality table v | _ -> vernac_set_option0 ~locality table v -let vernac_add_option key lv = - let f = function - | StringRefValue s -> (get_string_table key).add (Global.env()) s - | QualidRefValue locqid -> (get_ref_table key).add (Global.env()) locqid - in - try List.iter f lv with Not_found -> error_undeclared_key key +let vernac_add_option = iter_table { aux = fun table -> table.add } -let vernac_remove_option key lv = - let f = function - | StringRefValue s -> (get_string_table key).remove (Global.env()) s - | QualidRefValue locqid -> (get_ref_table key).remove (Global.env()) locqid - in - try List.iter f lv with Not_found -> error_undeclared_key key +let vernac_remove_option = iter_table { aux = fun table -> table.remove } -let vernac_mem_option key lv = - let f = function - | StringRefValue s -> (get_string_table key).mem (Global.env()) s - | QualidRefValue locqid -> (get_ref_table key).mem (Global.env()) locqid - in - try List.iter f lv with Not_found -> error_undeclared_key key +let vernac_mem_option = iter_table { aux = fun table -> table.mem } let vernac_print_option key = try (get_ref_table key).print () diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index c32ac414ba..e46186288e 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -121,10 +121,6 @@ type option_setting = | OptionSetInt of int | OptionSetString of string -type option_ref_value = - | StringRefValue of string - | QualidRefValue of qualid - (** Identifier and optional list of bound universes and constraints. *) type sort_expr = Sorts.family @@ -406,9 +402,9 @@ type nonrec vernac_expr = | VernacSetStrategy of (Conv_oracle.level * qualid or_by_notation list) list | VernacSetOption of bool (* Export modifier? *) * Goptions.option_name * option_setting - | VernacAddOption of Goptions.option_name * option_ref_value list - | VernacRemoveOption of Goptions.option_name * option_ref_value list - | VernacMemOption of Goptions.option_name * option_ref_value list + | VernacAddOption of Goptions.option_name * Goptions.table_value list + | VernacRemoveOption of Goptions.option_name * Goptions.table_value list + | VernacMemOption of Goptions.option_name * Goptions.table_value list | VernacPrintOption of Goptions.option_name | VernacCheckMayEval of Genredexpr.raw_red_expr option * Goal_select.t option * constr_expr | VernacGlobalCheck of constr_expr |