diff options
132 files changed, 1912 insertions, 1267 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index bac6ccd823..267da478d7 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -46,6 +46,9 @@ /CONTRIBUTING.md @Zimmi48 # Secondary maintainer @maximedenes +/CODE_OF_CONDUCT.md @Zimmi48 +# Secondary maintainer @mattam82 + /dev/doc/ @Zimmi48 # Secondary maintainer @maximedenes @@ -148,9 +151,8 @@ /plugins/ltac/ @ppedrot # Secondary maintainer @herbelin -/plugins/micromega/ @fajb -/test-suite/micromega/ @fajb -# Secondary maintainer @bgregoir +/plugins/micromega/ @coq/micromega-maintainers +/test-suite/micromega/ @coq/micromega-maintainers /plugins/nsatz/ @thery # Secondary maintainer @ppedrot diff --git a/.gitignore b/.gitignore index 8fc3c802ad..582a8f43c7 100644 --- a/.gitignore +++ b/.gitignore @@ -99,6 +99,9 @@ doc/faq/axioms.eps doc/faq/axioms.eps_t doc/faq/axioms.pdf_t doc/faq/axioms.png +doc/sphinx/index.rst +doc/sphinx/zebibliography.rst +doc/sphinx/credits-wrapper.rst doc/stdlib/Library.out doc/stdlib/Library.ps doc/stdlib/Library.coqdoc.tex diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 0115ac9eff..039c02c4b9 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -9,7 +9,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2018-09-05-V1" + CACHEKEY: "bionic_coq-V2018-09-21-V2" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" diff --git a/.travis.yml b/.travis.yml index dd28410bec..1a2c909c7d 100644 --- a/.travis.yml +++ b/.travis.yml @@ -105,8 +105,8 @@ matrix: # Full Coq test-suite with two compilers - if: NOT (type = pull_request) env: - - TEST_TARGET="test-suite" - - EXTRA_CONF="-coqide opt -with-doc yes" + - TEST_TARGET="doc-html test-suite" + - EXTRA_CONF="-coqide opt" - EXTRA_OPAM="${LABLGTK} ounit" before_install: &sphinx-install - sudo pip3 install bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex @@ -119,26 +119,17 @@ matrix: - aspcud - libgtk2.0-dev - libgtksourceview2.0-dev - - texlive-latex-base - - texlive-latex-recommended - - texlive-latex-extra - - texlive-math-extra - - texlive-fonts-recommended - - texlive-fonts-extra - - latex-xcolor - - ghostscript - - tipa - python3 - python3-pip - python3-setuptools - if: NOT (type = pull_request) env: - - TEST_TARGET="test-suite" + - TEST_TARGET="doc-html test-suite" - COMPILER="${COMPILER_BE}" - FINDLIB_VER="${FINDLIB_VER_BE}" - CAMLP5_VER="${CAMLP5_VER_BE}" - - EXTRA_CONF="-coqide opt -with-doc yes" + - EXTRA_CONF="-coqide opt" - EXTRA_OPAM="${LABLGTK_BE} ounit" before_install: *sphinx-install addons: @@ -150,11 +141,11 @@ matrix: # Full test-suite with flambda - if: NOT (type = pull_request) env: - - TEST_TARGET="test-suite" + - TEST_TARGET="doc-html test-suite" - COMPILER="${COMPILER_BE}+flambda" - FINDLIB_VER="${FINDLIB_VER_BE}" - CAMLP5_VER="${CAMLP5_VER_BE}" - - EXTRA_CONF="-coqide opt -with-doc yes -flambda-opts -O3" + - EXTRA_CONF="-coqide opt -flambda-opts -O3" - EXTRA_OPAM="${LABLGTK_BE} ounit" before_install: *sphinx-install addons: @@ -175,7 +166,9 @@ matrix: before_install: - brew update - brew unlink python - - brew install opam gnu-time + - brew install gnu-time + # only way to continue using OPAM 1.2 + - brew install https://raw.githubusercontent.com/Homebrew/homebrew-core/d156edeeed7291f4bc1e08620b331bbd05d52b78/Formula/opam.rb - if: NOT (type = pull_request) os: osx @@ -192,7 +185,9 @@ matrix: before_install: - brew update - brew unlink python - - brew install opam gnu-time gtk+ expat gtksourceview gdk-pixbuf + - brew install gnu-time gtk+ expat gtksourceview gdk-pixbuf + # only way to continue using OPAM 1.2 + - brew install https://raw.githubusercontent.com/Homebrew/homebrew-core/d156edeeed7291f4bc1e08620b331bbd05d52b78/Formula/opam.rb - brew unlink python@2 - brew install python3 - pip3 install macpack @@ -75,6 +75,12 @@ Focusing e.g. `[x]: {` will focus on a goal (existential variable) named `x`. As usual, unfocus with `}` once the sub-goal is fully solved. +Specification language + +- A fix to unification (which was sensitive to the ascii name of + variables) may occasionally change type inference in incompatible + ways, especially regarding the inference of the return clause of "match". + Standard Library - Added `Ascii.eqb` and `String.eqb` and the `=?` notation for them, @@ -209,12 +215,30 @@ Notations Changes from 8.8.1 to 8.8.2 =========================== +Documentation + +- A PDF version of the reference manual is available once again. + Tools - The coq-makefile targets `print-pretty-timed`, `print-pretty-timed-diff`, and `print-pretty-single-time-diff` now correctly label the "before" and "after" columns, rather than swapping them. +Kernel + +- The kernel does not tolerate capture of global universes by + polymorphic universe binders, fixing a soundness break (triggered + only through custom plugins) + +Windows installer + +- The Windows installer now includes many more external packages that can be +individually selected for installation. + +Many other bug fixes and lots of documentation improvements (for details, +see the 8.8.2 milestone at https://github.com/coq/coq/milestone/15?closed=1). + Changes from 8.8.0 to 8.8.1 =========================== diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md new file mode 100644 index 0000000000..8eee2009c9 --- /dev/null +++ b/CODE_OF_CONDUCT.md @@ -0,0 +1,118 @@ +# Coq Code of Conduct # + +The Coq development team and the user community are made up of a mixture of +professionals and volunteers from all over the world. +Diversity brings variety of perspectives that can be very valuable, but it can +also lead to communication issues and unhappiness. Therefore, we have a few +ground rules that we ask people to adhere to. +These rules apply equally to core developers (who should lead by example), +occasional contributors and those seeking help and guidance. +Their goal is that everyone feels safe and welcome when contributing to Coq or +interacting with others in Coq related forums. + +These rules apply to all spaces managed by the Coq development team. +This includes the GitHub repository, the mailing lists, the Gitter channel, +physical events like Coq working groups and workshops, and any other forums +created or managed by the development team which the community uses for +communication. In addition, violations of these rules outside these spaces may +affect a person's ability to participate within them. + +- **Be friendly and patient.** +- **Be welcoming.** + We strive to be a community that welcomes and supports people of all + backgrounds and identities. This includes, but is not limited to people of + any origin, color, status, educational level, gender identity, sexual + orientation, age, culture and beliefs, and mental and physical ability. +- **Be considerate.** + Your work will be used by other people, and you in turn will depend on the + work of others. Any decision you take will affect users and colleagues, and + you should take those consequences into account when making decisions. +- **Be respectful.** + Not all of us will agree all the time, but disagreement is no excuse for poor + behavior and poor manners. We might all experience some frustration now and + then, but we cannot allow that frustration to turn into a personal attack. + It's important to remember that a community where people feel uncomfortable + or threatened is not a productive one. Members of the Coq development team + and user community should be respectful when dealing with other members as + well as with people outside the community. +- **Be careful in the words that you choose.** + Be kind to others. Do not insult or put down other participants. Harassment + and other exclusionary behavior aren't acceptable. + * Violent language or threats or personal insults have no chance to + resolve a dispute or to let a discussion florish. Worse, they can + hurt durably, or generate durable fears. They are thus unwelcome. + * Not everyone is comfortable with sexually explicit or violent + material, even as a joke. In an online open multicultural world, you + don't know who might be listening. So be cautious and responsible + with your words. + * Discussions are online and recorded for posterity; we all have our + right for privacy and online gossiping as well as posting or threatening to + post other people's personally identifying information is prohibited. +- **Remember that what you write in a public online forum might be read by + many people you don't know.** + Consider what image your words will give to outsiders of the development + team / the user community as a whole. Try to avoid references to private + knowledge to be understandable by anyone. +- **Coq online forums are only to discuss Coq-related subjects.** + Unrelated political discussions or long digressions are unwelcome, + even for illustration or comparison purposes. +- **When we disagree, try to understand why.** + Disagreements, both social and technical, happen all the time and Coq is no + exception. It is important that we resolve disagreements and differing views + constructively. Remember that we are different. Different people + have different perspectives on issues. Being unable to understand why someone + holds a viewpoint doesn't mean that they're wrong. +- **It is human to make errors, and please try not to take things personally.** + Please do not answer aggressively to problematic behavior and simply + signal the issue. If actions have been taken with you (e.g. bans or simple + demands of apology, of rephrasing or keeping personal beliefs or troubles + private), please understand that they are not intended as aggression or + punishment ― even if you they feel harsh to you ― but as ways to enforce a + calm communication for the other participants and to give you the opportunity + to change your behavior. We understand you may feel hurt, or maybe you had a + bad day, so please take this opportunity to question yourself, cool down if + necessary and do not persist in the exact same behavior you have been + reported for. + +## Enforcement ## + +If you believe someone is violating the code of conduct, we ask that you report +it by emailing the Coq Code of Conduct enforcement team at +<coq-conduct@inria.fr>. Confidentiality with regard to the reporter of an +incident will be maintained while dealing with it. + +In particular, you should seek support from the team instead of dealing by +yourself with a behavior that you consider hurtful. This applies to members of +the enforcement team as well, who shouldn't deal by themselves with violations +in discussions in which they are a participant. + +Depending on the violation, the team can choose to address a private or public +warning to the offender, request an apology, or ban them for a short or a long +period from interacting on one or all of our forums. + +Except in case of serious violations, the team will always try a pedagogical +approach first (the offender does not necessarily realize immediately why their +behavior is wrong). We consider short bans to form part of the pedagogical +approach, especially when they come with explanatory comments, as this can give +some time to the offender to calm down and think about their actions. + +## Questions? ## + +If you have questions, feel free to write to <coq-conduct@inria.fr>. + +## Attribution ## + +This text is adapted from the [Django Code of Conduct][django-code-of-conduct] +which itself was adapted from the Speak Up! Community Code of Conduct. + +## License ## + +<a rel="license" href="http://creativecommons.org/licenses/by/4.0/"> +<img alt="Creative Commons License" style="border-width:0" src="https://i.creativecommons.org/l/by/4.0/88x31.png"> +</a><br> +This work is licensed under a +<a rel="license" href="http://creativecommons.org/licenses/by/4.0/"> +Creative Commons Attribution 4.0 International License +</a>. + +[django-code-of-conduct]: https://web.archive.org/web/20180714161115/https://www.djangoproject.com/conduct/ diff --git a/Makefile.doc b/Makefile.doc index 0dcf9daf27..788e4e61e7 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -58,17 +58,24 @@ ifndef QUICK SPHINX_DEPS := coq endif +# sphinx-html and sphinx-latex +sphinx-%: $(SPHINX_DEPS) + $(SHOW)'SPHINXBUILD doc/sphinx ($*)' + $(HIDE)$(SPHINXENV) $(SPHINXBUILD) -b $* \ + $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/$* + +sphinx-pdf: sphinx-latex + +$(MAKE) -C $(SPHINXBUILDDIR)/latex + sphinx: $(SPHINX_DEPS) - $(SHOW)'SPHINXBUILD doc/sphinx' - $(HIDE)$(SPHINXENV) $(SPHINXBUILD) -b html $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/html - @echo - @echo "Build finished. The HTML pages are in $(SPHINXBUILDDIR)/html." + +$(MAKE) sphinx-html + +$(MAKE) sphinx-pdf doc-html:\ - doc/stdlib/html/index.html sphinx + doc/stdlib/html/index.html sphinx-html doc-pdf:\ - doc/stdlib/Library.pdf + doc/stdlib/Library.pdf sphinx-pdf doc-ps:\ doc/stdlib/Library.ps @@ -181,7 +188,7 @@ install-doc-meta: $(MKDIR) $(FULLDOCDIR) $(INSTALLLIB) doc/LICENSE $(FULLDOCDIR)/LICENSE.doc -install-doc-html: install-doc-stdlib-html install-doc-sphinx +install-doc-html: install-doc-stdlib-html install-doc-sphinx-html install-doc-stdlib-html: $(MKDIR) $(FULLDOCDIR)/html/stdlib @@ -192,7 +199,7 @@ install-doc-printable: $(INSTALLLIB) doc/stdlib/Library.pdf $(FULLDOCDIR)/pdf $(INSTALLLIB) doc/stdlib/Library.ps $(FULLDOCDIR)/ps -install-doc-sphinx: +install-doc-sphinx-html: $(MKDIR) $(FULLDOCDIR)/sphinx (for f in `cd doc/sphinx/_build; find . -type f`; do \ $(MKDIR) $$(dirname $(FULLDOCDIR)/sphinx/$$f);\ diff --git a/Makefile.dune b/Makefile.dune index e04982650f..cac1bdd6a1 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -7,11 +7,15 @@ # DUNEOPT=--display=short BUILD_CONTEXT=_build/default +COQ_CONFIGURE_PREFIX?=_build/install/default + +export COQ_CONFIGURE_PREFIX help: @echo "Welcome to Coq's Dune-based build system. Targets are:" @echo " - states: build a minimal functional coqtop" @echo " - world: build all binaries and libraries" + @echo " - watch: build all binaries and libraries [continuous build]" @echo " - release: build Coq in release mode" @echo " - apidoc: build ML API documentation" @echo " - clean: remove build directory and autogenerated files" @@ -27,6 +31,9 @@ states: voboot world: voboot dune build $(DUNEOPT) @install +watch: voboot + dune build $(DUNEOPT) @install -w + release: voboot dune build $(DUNEOPT) -p coq diff --git a/config/dune b/config/dune index 30faf1233e..cf2bc71363 100644 --- a/config/dune +++ b/config/dune @@ -9,5 +9,5 @@ (rule (targets coq_config.ml) (mode fallback) - (deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run) - (action (chdir %{project_root} (run %{ocaml} configure.ml -local -warn-error yes -native-compiler yes)))) + (deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run (env_var COQ_CONFIGURE_PREFIX)) + (action (chdir %{project_root} (run %{ocaml} configure.ml -native-compiler no)))) diff --git a/configure.ml b/configure.ml index 00ec559a1b..1c2edefc5c 100644 --- a/configure.ml +++ b/configure.ml @@ -1038,7 +1038,16 @@ let find_suffix prefix path = match prefix with let do_one_instdir (var,msg,uservalue,selfcontainedlayout,unixlayout,locallayout) = let dir,suffix = if !prefs.local then (use_suffix coqtop locallayout,locallayout) - else match uservalue, !prefs.prefix with + else + let env_prefix = + match !prefs.prefix with + | None -> + begin + try Some (Sys.getenv "COQ_CONFIGURE_PREFIX") + with Not_found -> None + end + | p -> p + in match uservalue, env_prefix with | Some d, p -> d,find_suffix p d | _, Some p -> let suffix = if arch_is_win32 then selfcontainedlayout else relativize unixlayout in @@ -15,8 +15,12 @@ depends: [ "camlp5" ] +build-env: [ + [ COQ_CONFIGURE_PREFIX = "%{prefix}" ] +] + build: [ [ "dune" "build" "@vodeps" ] [ "dune" "exec" "coq_dune" "_build/default/.vfiles.d" ] - [ "dune" "build" "-p" package "-j" jobs ] + [ "dune" "build" "-p" name "-j" jobs ] ] diff --git a/default.nix b/default.nix index 6f759f41d1..88992a30a3 100644 --- a/default.nix +++ b/default.nix @@ -23,8 +23,8 @@ { pkgs ? (import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/4477cf04b6779a537cdb5f0bd3dd30e75aeb4a3b.tar.gz"; - sha256 = "1i39wsfwkvj9yryj8di3jibpdg3b3j86ych7s9rb6z79k08yaaxc"; + url = "https://github.com/NixOS/nixpkgs/archive/947ae71dcec680b5075ece14e38eae64831b9819.tar.gz"; + sha256 = "15nryymfch4fzxk6nacli4gw4cyicpdjwzai5v3bc0azaslww2x5"; }) {}) , ocamlPackages ? pkgs.ocaml-ng.ocamlPackages_4_06 , buildIde ? true @@ -38,18 +38,6 @@ with pkgs; with stdenv.lib; -let dune = - overrideDerivation jbuilder (o: { - name = "dune-1.1.1"; - src = fetchFromGitHub { - owner = "ocaml"; - repo = "dune"; - rev = "1.1.1"; - sha256 = "0v2pnxpmqsvrvidpwxvbsypzhqfdnjs5crjp9y61qi8nyj8d75zw"; - }; - }); -in - stdenv.mkDerivation rec { name = "coq"; diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 8a49b97dac..2a29b0d3b6 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -878,7 +878,7 @@ function make_num { function make_findlib { make_ocaml - if build_prep https://opam.ocaml.org/archives ocamlfind.1.8.0+opam tar.gz 1 ; then + if build_prep https://opam.ocaml.org/1.2.2/archives ocamlfind.1.8.0+opam tar.gz 1 ; then logn configure ./configure -bindir "$PREFIXOCAML\\bin" -sitelib "$PREFIXOCAML\\libocaml\\site-lib" -config "$PREFIXOCAML\\etc\\findlib.conf" # Note: findlib doesn't support -j 8, so don't pass MAKE_OPT log2 make all diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 8b26294d8f..d943795258 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-09-05-V1" +# CACHEKEY: "bionic_coq-V2018-09-21-V2" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -7,13 +7,19 @@ LABEL maintainer="e@x80.org" ENV DEBIAN_FRONTEND="noninteractive" RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ + # Dependencies of the image, the test-suite and external projects m4 automake autoconf time wget rsync git gcc-multilib opam \ + # Dependencies of lablgtk (for CoqIDE) libgtk2.0-dev libgtksourceview2.0-dev \ - texlive-latex-extra texlive-fonts-recommended texlive-science tipa \ - python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex \ - python3-setuptools python3-wheel python3-pip + # Dependencies of stdlib and sphinx doc + texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \ + xindy python3-pip python3-setuptools python3-pexpect python3-bs4 \ + # Dependencies of source-doc and coq-makefile + texlive-science tipa -RUN pip3 install antlr4-python3-runtime +# More dependencies of the sphinx doc +RUN pip3 install sphinx==1.7.8 sphinx_rtd_theme==0.2.5b2 \ + antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0 # Basic OPAM setup ENV NJOBS="2" \ @@ -28,7 +34,7 @@ RUN opam init -a -y -j $NJOBS --compiler="$COMPILER" default https://opam.ocaml. # Common OPAM packages. # `num` does not have a version number as the right version to install varies # with the compiler version. -ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.1.1 ounit.2.0.8" \ +ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8" \ CI_OPAM="menhir.20180530 elpi.1.0.5 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. diff --git a/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh b/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh new file mode 100644 index 0000000000..019cb8054d --- /dev/null +++ b/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh @@ -0,0 +1,4 @@ +if [ "$CI_PULL_REQUEST" = "7257" ] || [ "$CI_BRANCH" = "master+fix-yet-another-unif-dep-in-alphabet" ]; then + cross_crypto_CI_REF=master+fix-coq7257-ascii-sensitive-unification + cross_crypto_CI_GITURL=https://github.com/herbelin/cross-crypto +fi diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index 6166d24b70..8d78559c0d 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -109,6 +109,16 @@ Universes GH issue number: none risk: unlikely to be activated by chance + component: universe polymorphism + summary: universe polymorphism can capture global universes + impacted released versions: V8.5 to V8.8 + impacted coqchk versions: V8.5 to current (NOT FIXED) + fixed in: 2385b5c1ef + found by: Gaëtan Gilbert + exploit: test-suite/misc/poly-capture-global-univs + GH issue number: #8341 + risk: unlikely to be activated by chance (requires a plugin) + Primitive projections component: primitive projections, guard condition diff --git a/doc/README.md b/doc/README.md index 47507de52d..1461fa2e2c 100644 --- a/doc/README.md +++ b/doc/README.md @@ -28,18 +28,18 @@ To produce the complete documentation in HTML, you will need Coq dependencies listed in [`INSTALL`](../INSTALL). Additionally, the Sphinx-based reference manual requires Python 3, and the following Python packages: - sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect sphinxcontrib-bibtex + - sphinx >= 1.7.8 + - sphinx_rtd_theme >= 0.2.5b2 + - beautifulsoup4 >= 4.0.6 + - antlr4-python3-runtime >= 4.7.1 + - pexpect >= 4.2.1 + - sphinxcontrib-bibtex >= 0.4.0 -You can install them using `pip3 install` or using your distribution's package -manager. E.g. under recent Debian-based operating systems (Debian 10 "Buster", -Ubuntu 18.04, ...) you can use: +To install them, you should first install pip and setuptools (for instance, +with `apt install python3-pip python3-setuptools` on Debian / Ubuntu) then run: - apt install python3-sphinx python3-pexpect python3-sphinx-rtd-theme \ - python3-bs4 python3-sphinxcontrib.bibtex python3-pip - -Then, install the missing Python3 Antlr4 package: - - pip3 install antlr4-python3-runtime + pip3 install sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime \ + pexpect sphinxcontrib-bibtex Nix users should get the correct development environment to build the HTML documentation from Coq's [`default.nix`](../default.nix) (note this @@ -54,10 +54,19 @@ additional tools are required: - pdflatex - dvips - makeindex + - xelatex + - latexmk + - xindy + +All of them are part of the TexLive distribution. E.g. on Debian / Ubuntu, +install them with: + + apt install texlive-full -Install them using your package manager. E.g. on Debian / Ubuntu: +Or if you want to use less disk space: - apt install texlive-latex-extra texlive-fonts-recommended + apt install texlive-latex-extra texlive-fonts-recommended texlive-xetex \ + latexmk xindy Compilation ----------- @@ -80,7 +89,7 @@ Alternatively, you can use some specific targets: to produce all HTML documents - `make sphinx` - to produce the HTML version of the reference manual + to produce the HTML and PDF versions of the reference manual - `make stdlib` to produce all formats of the Coq standard library @@ -94,7 +103,7 @@ to avoid treating Sphinx warnings as errors. Otherwise, Sphinx quits upon detecting the first warning. You can set this on the Sphinx `make` command line or as an environment variable: -- `make sphinx SPINXWARNERROR=0` +- `make sphinx SPHINXWARNERROR=0` - ~~~ export SPHINXWARNERROR=0 diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 4673107e3d..c1f3f7b4d0 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -114,15 +114,33 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica Raised if :n:`@tactic` does not fully solve the goal. -``.. opt::`` :black_nib: A Coq option. +``.. flag::`` :black_nib: A Coq flag (i.e a binary-valued setting). Example:: - .. opt:: Nonrecursive Elimination Schemes + .. flag:: Nonrecursive Elimination Schemes This option controls whether types declared with the keywords :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the induction principles. +``.. opt::`` :black_nib: A Coq option (with a string or numeric value; use "flag" for binary options) + Example:: + + .. opt:: Printing Width @num + :name: Printing Width + + This command sets which left-aligned part of the width of the screen is used + for display. At the time of writing this documentation, the default value + is 78. + +``.. table::`` :black_nib: A Coq table (i.e a setting whose value is a set). + Example:: + + .. table:: Search Blacklist @string + :name: Search Blacklist + + This table controls ... + ``.. prodn::`` A grammar production. This is useful if you intend to document individual grammar productions. Otherwise, use Sphinx's `production lists @@ -260,8 +278,8 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo .. inference:: name - newline-separated premisses - ------------------------ + newline-separated premises + -------------------------- conclusion Example:: @@ -274,14 +292,12 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo ----------------------------- \WTEG{\forall~x:T,U}{\Prop} -``.. preamble::`` A reST directive for hidden math. - Mostly useful to let MathJax know about `\def`\ s and `\newcommand`\ s. - - Example:: +``.. preamble::`` A reST directive to include a TeX file. + Mostly useful to let MathJax know about `\def`s and `\newcommand`s. - .. preamble:: + Usage:: - \newcommand{\paren}[#1]{\left(#1\right)} + .. preamble:: preamble.tex Coq roles ========= @@ -364,6 +380,32 @@ DON'T This is equivalent to ``Axiom`` :token`ident` : :token:`term`. +.. + +DO + .. code:: + + :n:`power_tac @term [@ltac]` + allows :tacn:`ring` and :tacn:`ring_simplify` to recognize … + +DON'T + .. code:: + + power_tac :n:`@term` [:n:`@ltac`] + allows :tacn:`ring` and :tacn:`ring_simplify` to recognize … + +.. + +DO + .. code:: + + :n:`name={*; attr}` + +DON'T + .. code:: + + ``name=``:n:`{*; attr}` + Omitting annotations -------------------- @@ -377,6 +419,86 @@ DON'T .. tacv:: assert form as intro_pattern +Using the ``.. coqtop::`` directive for syntax highlighting +----------------------------------------------------------- + +DO + .. code:: + + A tactic of the form: + + .. coqdoc:: + + do [ t1 | … | tn ]. + + is equivalent to the standard Ltac expression: + + .. coqdoc:: + + first [ t1 | … | tn ]. + +DON'T + .. code:: + + A tactic of the form: + + .. coqtop:: in + + do [ t1 | … | tn ]. + + is equivalent to the standard Ltac expression: + + .. coqtop:: in + + first [ t1 | … | tn ]. + +Overusing plain quotes +---------------------- + +DO + .. code:: + + The :tacn:`refine` tactic can raise the :exn:`Invalid argument` exception. + The term :g:`let a = 1 in a a` is ill-typed. + +DON'T + .. code:: + + The ``refine`` tactic can raise the ``Invalid argument`` exception. + The term ``let a = 1 in a a`` is ill-typed. + +Plain quotes produce plain text, without highlighting or cross-references. + +Overusing the ``example`` directive +----------------------------------- + +DO + .. code:: + + Here is a useful axiom: + + .. coqdoc:: + + Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. + +DO + .. code:: + + .. example:: Using proof-irrelevance + + If you assume the axiom above, … + +DON'T + .. code:: + + Here is a useful axiom: + + .. example:: + + .. coqdoc:: + + Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. + Tips and tricks =============== @@ -398,7 +520,7 @@ Add either ``undo`` to the first block or ``reset`` to the second block to avoid Abbreviations and macros ------------------------ -Abbreviations and placeholders for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``) are defined in a `separate file </doc/sphinx/replaces.rst>`_ included by most chapters of the manual. Some useful LaTeX macros are defined in `</doc/sphinx/preamble.rst>`_. +Substitutions for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``), along with some useful LaTeX macros, are defined in a `separate file </doc/sphinx/refman-preamble.rst>`_. This file is automatically included in all manual pages. Emacs ----- diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index c333d6e9d5..86914a71df 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -140,6 +140,32 @@ DON'T This is equivalent to ``Axiom`` :token`ident` : :token:`term`. +.. + +DO + .. code:: + + :n:`power_tac @term [@ltac]` + allows :tacn:`ring` and :tacn:`ring_simplify` to recognize … + +DON'T + .. code:: + + power_tac :n:`@term` [:n:`@ltac`] + allows :tacn:`ring` and :tacn:`ring_simplify` to recognize … + +.. + +DO + .. code:: + + :n:`name={*; attr}` + +DON'T + .. code:: + + ``name=``:n:`{*; attr}` + Omitting annotations -------------------- @@ -153,6 +179,86 @@ DON'T .. tacv:: assert form as intro_pattern +Using the ``.. coqtop::`` directive for syntax highlighting +----------------------------------------------------------- + +DO + .. code:: + + A tactic of the form: + + .. coqdoc:: + + do [ t1 | … | tn ]. + + is equivalent to the standard Ltac expression: + + .. coqdoc:: + + first [ t1 | … | tn ]. + +DON'T + .. code:: + + A tactic of the form: + + .. coqtop:: in + + do [ t1 | … | tn ]. + + is equivalent to the standard Ltac expression: + + .. coqtop:: in + + first [ t1 | … | tn ]. + +Overusing plain quotes +---------------------- + +DO + .. code:: + + The :tacn:`refine` tactic can raise the :exn:`Invalid argument` exception. + The term :g:`let a = 1 in a a` is ill-typed. + +DON'T + .. code:: + + The ``refine`` tactic can raise the ``Invalid argument`` exception. + The term ``let a = 1 in a a`` is ill-typed. + +Plain quotes produce plain text, without highlighting or cross-references. + +Overusing the ``example`` directive +----------------------------------- + +DO + .. code:: + + Here is a useful axiom: + + .. coqdoc:: + + Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. + +DO + .. code:: + + .. example:: Using proof-irrelevance + + If you assume the axiom above, … + +DON'T + .. code:: + + Here is a useful axiom: + + .. example:: + + .. coqdoc:: + + Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. + Tips and tricks =============== @@ -174,7 +280,7 @@ Add either ``undo`` to the first block or ``reset`` to the second block to avoid Abbreviations and macros ------------------------ -Abbreviations and placeholders for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``) are defined in a `separate file </doc/sphinx/replaces.rst>`_ included by most chapters of the manual. Some useful LaTeX macros are defined in `</doc/sphinx/preamble.rst>`_. +Substitutions for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``), along with some useful LaTeX macros, are defined in a `separate file </doc/sphinx/refman-preamble.rst>`_. This file is automatically included in all manual pages. Emacs ----- diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst index 2cc1f95c08..3e414a714c 100644 --- a/doc/sphinx/addendum/canonical-structures.rst +++ b/doc/sphinx/addendum/canonical-structures.rst @@ -1,4 +1,3 @@ -.. include:: ../replaces.rst .. _canonicalstructures: Canonical Structures diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index e507a224c6..cb267576b2 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -1,15 +1,13 @@ -.. include:: ../replaces.rst - .. _extendedpatternmatching: -Extended pattern-matching +Extended pattern matching ========================= :Authors: Cristina Cornes and Hugo Herbelin .. TODO links to figures -This section describes the full form of pattern-matching in |Coq| terms. +This section describes the full form of pattern matching in |Coq| terms. .. |rhs| replace:: right hand sides @@ -38,7 +36,7 @@ same values as ``pattern`` does and ``identifier`` is bound to the matched value. A pattern of the form :n:`pattern | pattern` is called disjunctive. A list of patterns separated with commas is also considered as a pattern and is called *multiple pattern*. However multiple patterns can only -occur at the root of pattern-matching equations. Disjunctions of +occur at the root of pattern matching equations. Disjunctions of *multiple patterns* are allowed though. Since extended ``match`` expressions are compiled into the primitive ones, @@ -46,7 +44,7 @@ the expressiveness of the theory remains the same. Once parsing has finished only simple patterns remain. The original nesting of the ``match`` expressions is recovered at printing time. An easy way to see the result of the expansion is to toggle off the nesting performed at printing -(use here :opt:`Printing Matching`), then by printing the term with :cmd:`Print` +(use here :flag:`Printing Matching`), then by printing the term with :cmd:`Print` if the term is a constant, or using the command :cmd:`Check`. The extended ``match`` still accepts an optional *elimination predicate* @@ -88,7 +86,7 @@ Using multiple patterns in the definition of ``max`` lets us write: which will be compiled into the previous form. -The pattern-matching compilation strategy examines patterns from left +The pattern matching compilation strategy examines patterns from left to right. A match expression is generated **only** when there is at least one constructor in the column of patterns. E.g. the following example does not build a match expression. @@ -262,9 +260,9 @@ When we use parameters in patterns there is an error message: | cons A _ l' => l' end). -.. opt:: Asymmetric Patterns +.. flag:: Asymmetric Patterns -This option (off by default) removes parameters from constructors in patterns: + This flag (off by default) removes parameters from constructors in patterns: .. coqtop:: all @@ -597,7 +595,7 @@ situation: incorrect (because constructors are not applied to the correct number of the arguments, because they are not linear or they are wrongly typed). -.. exn:: Non exhaustive pattern-matching. +.. exn:: Non exhaustive pattern matching. The pattern matching is not exhaustive. diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index e3d25cf5cf..3d58f522dd 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _extraction: Extraction of programs in |OCaml| and Haskell @@ -131,14 +129,14 @@ order to produce more readable code. The type-preserving optimizations are controlled by the following |Coq| options: -.. opt:: Extraction Optimize +.. flag:: Extraction Optimize Default is on. This controls all type-preserving optimizations made on the ML terms (mostly reduction of dummy beta/iota redexes, but also simplifications on Cases, etc). Turn this option off if you want a ML term as close as possible to the Coq term. -.. opt:: Extraction Conservative Types +.. flag:: Extraction Conservative Types Default is off. This controls the non type-preserving optimizations made on ML terms (which try to avoid function abstraction of dummy @@ -146,7 +144,7 @@ The type-preserving optimizations are controlled by the following |Coq| options: implies that ``e':t'`` where ``e'`` and ``t'`` are the extracted code of ``e`` and ``t`` respectively. -.. opt:: Extraction KeepSingleton +.. flag:: Extraction KeepSingleton Default is off. Normally, when the extraction of an inductive type produces a singleton type (i.e. a type with only one constructor, and @@ -155,7 +153,7 @@ The type-preserving optimizations are controlled by the following |Coq| options: The typical example is ``sig``. This option allows disabling this optimization when one wishes to preserve the inductive structure of types. -.. opt:: Extraction AutoInline +.. flag:: Extraction AutoInline Default is on. The extraction mechanism inlines the bodies of some defined constants, according to some heuristics @@ -227,7 +225,7 @@ When an actual extraction takes place, an error is normally raised if the if any of the implicit arguments still occurs in the final code. This behavior can be relaxed via the following option: -.. opt:: Extraction SafeImplicits +.. flag:: Extraction SafeImplicits Default is on. When this option is off, a warning is emitted instead of an error if some implicit arguments still occur in the @@ -319,15 +317,15 @@ native boolean type instead of the |Coq| one. The syntax is the following: extractions for the type itself (first `string`) and all its constructors (all the `string` between square brackets). In this form, the ML extraction must be an ML inductive datatype, and the native - pattern-matching of the language will be used. + pattern matching of the language will be used. .. cmdv:: Extract Inductive @qualid => @string [ {+ @string } ] @string Same as before, with a final extra `string` that indicates how to - perform pattern-matching over this inductive type. In this form, + perform pattern matching over this inductive type. In this form, the ML extraction could be an arbitrary type. For an inductive type with `k` constructors, the function used to - emulate the pattern-matching should expect `(k+1)` arguments, first the `k` + emulate the pattern matching should expect `(k+1)` arguments, first the `k` branches in functional form, and then the inductive element to destruct. For instance, the match branch ``| S n => foo`` gives the functional form ``(fun n -> foo)``. Note that a constructor with no @@ -344,7 +342,7 @@ native boolean type instead of the |Coq| one. The syntax is the following: * Extracting an inductive type to a pre-existing ML inductive type is quite sound. But extracting to a general type (by providing an - ad-hoc pattern-matching) will often **not** be fully rigorously + ad-hoc pattern matching) will often **not** be fully rigorously correct. For instance, when extracting ``nat`` to |OCaml| ``int``, it is theoretically possible to build ``nat`` values that are larger than |OCaml| ``max_int``. It is the user's responsibility to diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index e0babb6c4e..403b163196 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _generalizedrewriting: Generalized rewriting @@ -126,10 +123,10 @@ parameters is any term :math:`f \, t_1 \ldots t_n`. .. coqtop:: in - forall (A : Type) (S1 S1’ S2 S2’ : list A), - set_eq A S1 S1’ -> - set_eq A S2 S2’ -> - set_eq A (union A S1 S2) (union A S1’ S2’). + forall (A: Type) (S1 S1' S2 S2': list A), + set_eq A S1 S1' -> + set_eq A S2 S2' -> + set_eq A (union A S1 S2) (union A S1' S2'). The signature of the function ``union A`` is ``set_eq A ==> set_eq A ==> set_eq A`` for all ``A``. @@ -451,7 +448,7 @@ various combinations of properties on relations and morphisms are represented as records and instances of theses classes are put in a hint database. For example, the declaration: -.. coqtop:: in +.. coqdoc:: Add Parametric Relation (x1 : T1) ... (xn : Tn) : (A t1 ... tn) (Aeq t′1 ... t′m) [reflexivity proved by refl] @@ -462,7 +459,7 @@ hint database. For example, the declaration: is equivalent to an instance declaration: -.. coqtop:: in +.. coqdoc:: Instance (x1 : T1) ... (xn : Tn) => id : @Equivalence (A t1 ... tn) (Aeq t′1 ... t′m) := [Equivalence_Reflexive := refl] diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 23cbd76eda..fc5a366caf 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _implicitcoercions: Implicit Coercions @@ -256,19 +254,16 @@ Displaying Available Coercions Activating the Printing of Coercions ------------------------------------- -.. opt:: Printing Coercions +.. flag:: Printing Coercions When on, this option forces all the coercions to be printed. By default, coercions are not printed. -.. cmd:: Add Printing Coercion @qualid - - This command forces coercion denoted by :n:`@qualid` to be printed. - By default, a coercion is never printed. - -.. cmd:: Remove Printing Coercion @qualid +.. table:: Printing Coercion @qualid + :name: Printing Coercion - Use this command, to skip the printing of coercion :n:`@qualid`. + Specifies a set of qualids for which coercions are always displayed. Use the + :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of qualids. .. _coercions-classes-as-records: @@ -315,7 +310,7 @@ are also forgotten. Coercions and Modules --------------------- -.. opt:: Automatic Coercions Import +.. flag:: Automatic Coercions Import Since |Coq| version 8.3, the coercions present in a module are activated only when the module is explicitly imported. Formerly, the coercions diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index 0f2d35d044..2cde65dcdc 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _miscellaneousextensions: Miscellaneous extensions diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst index 9adeca46fc..e7a8c238ac 100644 --- a/doc/sphinx/addendum/nsatz.rst +++ b/doc/sphinx/addendum/nsatz.rst @@ -1,5 +1,3 @@ -.. include:: ../preamble.rst - .. _nsatz_chapter: Nsatz: tactics for proving equalities in integral domains diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index f7a431ef29..828505b850 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -116,23 +116,23 @@ loaded by Options ------- -.. opt:: Stable Omega +.. flag:: Stable Omega .. deprecated:: 8.5 This deprecated option (on by default) is for compatibility with Coq pre 8.5. It resets internal name counters to make executions of :tacn:`omega` independent. -.. opt:: Omega UseLocalDefs +.. flag:: Omega UseLocalDefs This option (on by default) allows :tacn:`omega` to use the bodies of local variables. -.. opt:: Omega System +.. flag:: Omega System This option (off by default) activate the printing of debug information -.. opt:: Omega Action +.. flag:: Omega Action This option (off by default) activate the printing of debug information diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index 8ee8f52227..8b7214e2ab 100644 --- a/doc/sphinx/addendum/parallel-proof-processing.rst +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _asynchronousandparallelproofprocessing: Asynchronous and Parallel Proof Processing @@ -60,7 +58,7 @@ variables used. Automatic suggestion of proof annotations ````````````````````````````````````````` -The command ``Set Suggest Proof Using`` makes |Coq| suggest, when a ``Qed`` +The flag :flag:`Suggest Proof Using` makes |Coq| suggest, when a ``Qed`` command is processed, a correct proof annotation. It is up to the user to modify the proof script accordingly. diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index d6895f5fe5..fad45995d2 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. this should be just "_program", but refs to it don't work .. _programs: @@ -45,7 +42,7 @@ be considered as an object of type :g:`{x : T | P}` for any well-formed will generate an obligation for every such coercion. In the other direction, Russell will automatically insert a projection. -Another distinction is the treatment of pattern-matching. Apart from +Another distinction is the treatment of pattern matching. Apart from the following differences, it is equivalent to the standard match operation (see :ref:`extendedpatternmatching`). @@ -84,15 +81,15 @@ operation (see :ref:`extendedpatternmatching`). There are options to control the generation of equalities and coercions. -.. opt:: Program Cases +.. flag:: Program Cases - This controls the special treatment of pattern-matching generating equalities + This controls the special treatment of pattern matching generating equalities and disequalities when using |Program| (it is on by default). All pattern-matches and let-patterns are handled using the standard algorithm of |Coq| (see :ref:`extendedpatternmatching`) when this option is deactivated. -.. opt:: Program Generalized Coercion +.. flag:: Program Generalized Coercion This controls the coercion of general inductive types when using |Program| (the option is on by default). Coercion of subset types and pairs is still @@ -105,7 +102,7 @@ Syntactic control over equalities To give more control over the generation of equalities, the type checker will fall back directly to |Coq|’s usual typing of dependent -pattern-matching if a return or in clause is specified. Likewise, the +pattern matching if a return or in clause is specified. Likewise, the if construct is not treated specially by |Program| so boolean tests in the code are not automatically reflected in the obligations. One can use the :g:`dec` combinator to get the correct hypotheses as in: @@ -213,7 +210,7 @@ with mutually recursive definitions too. end. Here we have one obligation for each branch (branches for :g:`0` and -``(S 0)`` are automatically generated by the pattern-matching +``(S 0)`` are automatically generated by the pattern matching compilation algorithm). .. coqtop:: all @@ -320,19 +317,19 @@ optional tactic is replaced by the default one if not specified. Shows the term that will be fed to the kernel once the obligations are solved. Useful for debugging. -.. opt:: Transparent Obligations +.. flag:: Transparent Obligations Controls whether all obligations should be declared as transparent (the default), or if the system should infer which obligations can be declared opaque. -.. opt:: Hide Obligations +.. flag:: Hide Obligations Controls whether obligations appearing in the term should be hidden as implicit arguments of the special constantProgram.Tactics.obligation. -.. opt:: Shrink Obligations +.. flag:: Shrink Obligations *Deprecated since 8.7* @@ -378,6 +375,3 @@ Frequently Asked Questions using lazy evaluation; #. Mutual recursion on the underlying inductive type isn’t possible anymore, but nested mutual recursion is always possible. - -.. bibliography:: ../biblio.bib - :keyprefix: p- diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 8cb86e2267..58617916c0 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -1,11 +1,9 @@ -.. include:: ../replaces.rst .. |ra| replace:: :math:`\rightarrow_{\beta\delta\iota}` .. |la| replace:: :math:`\leftarrow_{\beta\delta\iota}` .. |eq| replace:: `=`:sub:`(by the main correctness theorem)` .. |re| replace:: ``(PEeval`` `v` `ap`\ ``)`` .. |le| replace:: ``(Pphi_dev`` `v` ``(norm`` `ap`\ ``))`` - .. _theringandfieldtacticfamilies: The ring and field tactic families diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index ab4b4a9824..369dae0ead 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _typeclasses: Type Classes @@ -458,7 +456,7 @@ This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``. Options ~~~~~~~ -.. opt:: Typeclasses Dependency Order +.. flag:: Typeclasses Dependency Order This option (on by default since 8.6) respects the dependency order between subgoals, meaning that subgoals on which other subgoals depend @@ -467,7 +465,7 @@ Options quite different performance behaviors of proof search. -.. opt:: Typeclasses Filtered Unification +.. flag:: Typeclasses Filtered Unification This option, available since Coq 8.6 and off by default, switches the hint application procedure to a filter-then-unify strategy. To apply a @@ -481,7 +479,7 @@ Options where there is a hole in that place. -.. opt:: Typeclasses Limit Intros +.. flag:: Typeclasses Limit Intros This option (on by default) controls the ability to apply hints while avoiding (functional) eta-expansions in the generated proof term. It @@ -495,7 +493,7 @@ Options status of the product introduction rule, resulting in potentially more expensive proof-search (i.e. more useless backtracking). -.. opt:: Typeclass Resolution For Conversion +.. flag:: Typeclass Resolution For Conversion This option (on by default) controls the use of typeclass resolution when a unification problem cannot be solved during elaboration/type @@ -503,7 +501,7 @@ Options resolution is tried before launching unification once again. -.. opt:: Typeclasses Strict Resolution +.. flag:: Typeclasses Strict Resolution Typeclass declarations introduced when this option is set have a stricter resolution behavior (the option is off by default). When @@ -513,28 +511,33 @@ Options instantiated. -.. opt:: Typeclasses Unique Solutions +.. flag:: Typeclasses Unique Solutions When a typeclass resolution is launched we ensure that it has a single solution or fail. This ensures that the resolution is canonical, but can make proof search much more expensive. -.. opt:: Typeclasses Unique Instances +.. flag:: Typeclasses Unique Instances Typeclass declarations introduced when this option is set have a more efficient resolution behavior (the option is off by default). When a solution to the typeclass goal of this class is found, we never backtrack on it, assuming that it is canonical. -.. opt:: Typeclasses Debug {? Verbosity @num} +.. flag:: Typeclasses Debug + + Controls whether typeclass resolution steps are shown during search. Setting this flag + also sets :opt:`Typeclasses Debug Verbosity` to 1. + +.. opt:: Typeclasses Debug Verbosity @num + :name: Typeclasses Debug Verbosity - These options allow to see the resolution steps of typeclasses that are - performed during search. The ``Debug`` option is synonymous to ``Debug - Verbosity 1``, and ``Debug Verbosity 2`` provides more information - (tried tactics, shelving of goals, etc…). + Determines how much information is shown for typeclass resolution steps during search. + 1 is the default level. 2 shows additional information such as tried tactics and shelving + of goals. Setting this option also sets :flag:`Typeclasses Debug`. -.. opt:: Refine Instance Mode +.. flag:: Refine Instance Mode This option allows to switch the behavior of instance declarations made through the Instance command. diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 7e77dea457..41afe3c312 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _polymorphicuniverses: Polymorphic Universes @@ -59,7 +57,7 @@ so: Definition selfpid := pidentity (@pidentity). Of course, the two instances of :g:`pidentity` in this definition are -different. This can be seen when the :opt:`Printing Universes` option is on: +different. This can be seen when the :flag:`Printing Universes` flag is on: .. coqtop:: none @@ -79,7 +77,7 @@ levels. When printing :g:`pidentity`, we can see the universes it binds in the annotation :g:`@{Top.2}`. Additionally, when -:opt:`Printing Universes` is on we print the "universe context" of +:flag:`Printing Universes` is on we print the "universe context" of :g:`pidentity` consisting of the bound universes and the constraints they must verify (for :g:`pidentity` there are no constraints). @@ -129,14 +127,14 @@ Polymorphic, Monomorphic As shown in the examples, polymorphic definitions and inductives can be declared using the ``Polymorphic`` prefix. -.. opt:: Universe Polymorphism +.. flag:: Universe Polymorphism Once enabled, this option will implicitly prepend ``Polymorphic`` to any definition of the user. .. cmd:: Monomorphic @definition - When the :opt:`Universe Polymorphism` option is set, to make a definition + When the :flag:`Universe Polymorphism` option is set, to make a definition producing global universe constraints, one can use the ``Monomorphic`` prefix. Many other commands support the ``Polymorphic`` flag, including: @@ -169,7 +167,7 @@ declared cumulative using the :g:`Cumulative` prefix. Declares the inductive as cumulative -Alternatively, there is an option :opt:`Polymorphic Inductive +Alternatively, there is a flag :flag:`Polymorphic Inductive Cumulativity` which when set, makes all subsequent *polymorphic* inductive definitions cumulative. When set, inductive types and the like can be enforced to be non-cumulative using the :g:`NonCumulative` @@ -179,7 +177,7 @@ prefix. Declares the inductive as non-cumulative -.. opt:: Polymorphic Inductive Cumulativity +.. flag:: Polymorphic Inductive Cumulativity When this option is on, it sets all following polymorphic inductive types as cumulative (it is off by default). @@ -229,7 +227,7 @@ Cumulative inductive types, coninductive types, variants and records only make sense when they are universe polymorphic. Therefore, an error is issued whenever the user uses the :g:`Cumulative` or :g:`NonCumulative` prefix in a monomorphic context. -Notice that this is not the case for the option :opt:`Polymorphic Inductive Cumulativity`. +Notice that this is not the case for the option :flag:`Polymorphic Inductive Cumulativity`. That is, this option, when set, makes all subsequent *polymorphic* inductive declarations cumulative (unless, of course the :g:`NonCumulative` prefix is used) but has no effect on *monomorphic* inductive declarations. @@ -277,18 +275,18 @@ An example of a proof using cumulativity Cumulativity Weak Constraints ----------------------------- -.. opt:: Cumulativity Weak Constraints +.. flag:: Cumulativity Weak Constraints -This option, on by default, causes "weak" constraints to be produced -when comparing universes in an irrelevant position. Processing weak -constraints is delayed until minimization time. A weak constraint -between `u` and `v` when neither is smaller than the other and -one is flexible causes them to be unified. Otherwise the constraint is -silently discarded. + When set, which is the default, causes "weak" constraints to be produced + when comparing universes in an irrelevant position. Processing weak + constraints is delayed until minimization time. A weak constraint + between `u` and `v` when neither is smaller than the other and + one is flexible causes them to be unified. Otherwise the constraint is + silently discarded. -This heuristic is experimental and may change in future versions. -Disabling weak constraints is more predictable but may produce -arbitrary numbers of universes. + This heuristic is experimental and may change in future versions. + Disabling weak constraints is more predictable but may produce + arbitrary numbers of universes. Global and local universes @@ -354,9 +352,9 @@ This minimization process is applied only to fresh universe variables. It simply adds an equation between the variable and its lower bound if it is an atomic universe (i.e. not an algebraic max() universe). -.. opt:: Universe Minimization ToSet +.. flag:: Universe Minimization ToSet - Turning this option off (it is on by default) disallows minimization + Turning this flag off (it is on by default) disallows minimization to the sort :g:`Set` and only collapses floating universes between themselves. @@ -436,7 +434,7 @@ underscore or by omitting the annotation to a polymorphic definition. Check le@{k _}. Check le. -.. opt:: Strict Universe Declaration. +.. flag:: Strict Universe Declaration Turning this option off allows one to freely use identifiers for universes without declaring them first, with the diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index c74d8f540c..aa8537c92d 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -121,7 +121,7 @@ s}, volume = {7998}, editor = {Sandrine Blazy and Christine Paulin and David Pichardie }, series = {LNCS }, - doi = {10.1007/978-3-642-39634-2\_5 }, + doi = {10.1007/978-3-642-39634-2_5}, year = {2013}, } @@ -136,7 +136,7 @@ s}, pages = {85--95}, month = {November}, year = {2000}, - url = {http://www.lirmm.fr/\%7Edelahaye/papers/ltac\%20(LPAR\%2700).pdf} + url = {http://www.lirmm.fr/%7Edelahaye/papers/ltac%20(LPAR%2700).pdf} } @Article{Dyc92, diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 8127d3df3f..b43d5fb6f0 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -24,6 +24,8 @@ import sys import os +from shutil import copyfile +import sphinx # Increase recursion limit for sphinx sys.setrecursionlimit(1500) @@ -36,6 +38,12 @@ sys.path.append(os.path.abspath('../../config/')) import coq_config +# -- Prolog --------------------------------------------------------------- + +# Include substitution definitions in all files +with open("refman-preamble.rst") as s: + rst_prolog = s.read() + # -- General configuration ------------------------------------------------ # If your documentation needs a minimal Sphinx version, state it here. @@ -66,11 +74,39 @@ source_suffix = '.rst' # The encoding of source files. #source_encoding = 'utf-8-sig' +# Add extra cases here to support more formats + +SUPPORTED_FORMATS = ["html", "latex"] + +def readbin(fname): + try: + with open(fname, mode="rb") as f: + return f.read() + except FileNotFoundError: + return None + +def copy_formatspecific_files(app): + ext = ".{}.rst".format(app.builder.name) + for fname in sorted(os.listdir(app.srcdir)): + if fname.endswith(ext): + src = os.path.join(app.srcdir, fname) + dst = os.path.join(app.srcdir, fname[:-len(ext)] + ".rst") + logger = sphinx.util.logging.getLogger(__name__) + if readbin(src) == readbin(dst): + logger.info("Skipping {}: {} is up to date".format(src, dst)) + else: + logger.info("Copying {} to {}".format(src, dst)) + copyfile(src, dst) + +def setup(app): + app.connect('builder-inited', copy_formatspecific_files) + # The master toctree document. -master_doc = 'index' +# We create this file in `copy_master_doc` above. +master_doc = "index" # General information about the project. -project = 'Coq' +project = 'The Coq Reference Manual' copyright = '1999-2018, Inria' author = 'The Coq Development Team' @@ -104,9 +140,10 @@ exclude_patterns = [ 'Thumbs.db', '.DS_Store', 'introduction.rst', + 'refman-preamble.rst', 'README.rst', 'README.template.rst' -] +] + ["*.{}.rst".format(fmt) for fmt in SUPPORTED_FORMATS] # The reST default role (used for this markup: `text`) to use for all # documents. @@ -129,6 +166,7 @@ primary_domain = 'coq' # The name of the Pygments (syntax highlighting) style to use. pygments_style = 'sphinx' highlight_language = 'text' +suppress_warnings = ["misc.highlighting_failure"] # A list of ignored prefixes for module index sorting. #modindex_common_prefix = [] @@ -257,57 +295,57 @@ smartquotes = False ########################### # Set things up for XeTeX # ########################### + latex_elements = { 'babel': '', 'fontenc': '', 'inputenc': '', 'utf8extra': '', 'cmappkg': '', - # https://www.topbug.net/blog/2015/12/10/a-collection-of-issues-about-the-latex-output-in-sphinx-and-the-solutions/ 'papersize': 'letterpaper', 'classoptions': ',openany', # No blank pages - 'polyglossia' : '\\usepackage{polyglossia}', - 'unicode-math' : '\\usepackage{unicode-math}', - 'microtype' : '\\usepackage{microtype}', - "preamble": r"\usepackage{coqnotations}" + 'polyglossia': '\\usepackage{polyglossia}', + 'sphinxsetup': 'verbatimwithframe=false', + 'preamble': r""" + \usepackage{unicode-math} + \usepackage{microtype} + + % Macro definitions + \usepackage{refman-preamble} + + % Style definitions for notations + \usepackage{coqnotations} + + % Style tweaks + \newcssclass{sigannot}{\textrm{#1:}} + + % Silence 'LaTeX Warning: Command \nobreakspace invalid in math mode' + \everymath{\def\nobreakspace{\ }} + """ } -from sphinx.builders.latex import LaTeXBuilder +latex_engine = "xelatex" ######## # done # ######## -latex_additional_files = ["_static/coqnotations.sty"] +latex_additional_files = [ + "refman-preamble.sty", + "_static/coqnotations.sty" +] -# Grouping the document tree into LaTeX files. List of tuples -# (source start file, target name, title, -# author, documentclass [howto, manual, or own class]). -# latex_documents = [ -# (master_doc, 'CoqRefMan.tex', 'Coq Documentation', -# 'The Coq Development Team', 'manual'), -#] +latex_documents = [('index', 'CoqRefMan.tex', project, author, 'manual')] # The name of an image file (relative to this directory) to place at the top of # the title page. -#latex_logo = None - -# For "manual" documents, if this is true, then toplevel headings are parts, -# not chapters. -#latex_use_parts = False +# latex_logo = "../../ide/coq.png" # If true, show page references after internal links. #latex_show_pagerefs = False # If true, show URL addresses after external links. -#latex_show_urls = False - -# Documents to append as an appendix to all manuals. -#latex_appendices = [] - -# If false, no module index is generated. -#latex_domain_indices = True - +latex_show_urls = 'footnote' # -- Options for manual page output --------------------------------------- diff --git a/doc/sphinx/coq-cmdindex.rst b/doc/sphinx/coq-cmdindex.rst index 7df6cb36c5..fd0b342ae4 100644 --- a/doc/sphinx/coq-cmdindex.rst +++ b/doc/sphinx/coq-cmdindex.rst @@ -1,3 +1,5 @@ +:orphan: + .. hack to get index in TOC ----------------- diff --git a/doc/sphinx/coq-exnindex.rst b/doc/sphinx/coq-exnindex.rst index 100c57b085..fc55e91eee 100644 --- a/doc/sphinx/coq-exnindex.rst +++ b/doc/sphinx/coq-exnindex.rst @@ -1,5 +1,7 @@ +:orphan: + .. hack to get index in TOC ----------------------- -Errors, warnings index ----------------------- +------------------------- +Errors and warnings index +------------------------- diff --git a/doc/sphinx/coq-optindex.rst b/doc/sphinx/coq-optindex.rst index f8046a800b..0961bea61f 100644 --- a/doc/sphinx/coq-optindex.rst +++ b/doc/sphinx/coq-optindex.rst @@ -1,5 +1,7 @@ +:orphan: + .. hack to get index in TOC ------------------ -Option index ------------------ +------------------------------- +Flags, options and tables index +------------------------------- diff --git a/doc/sphinx/coq-tacindex.rst b/doc/sphinx/coq-tacindex.rst index 588104f465..31b2f7f8cb 100644 --- a/doc/sphinx/coq-tacindex.rst +++ b/doc/sphinx/coq-tacindex.rst @@ -1,3 +1,5 @@ +:orphan: + .. hack to get index in TOC ------------- diff --git a/doc/sphinx/credits-wrapper.html.rst b/doc/sphinx/credits-wrapper.html.rst new file mode 100644 index 0000000000..2d35a12dc2 --- /dev/null +++ b/doc/sphinx/credits-wrapper.html.rst @@ -0,0 +1,7 @@ +.. _credits: + +------- +Credits +------- + +.. include:: credits.rst diff --git a/doc/sphinx/credits-wrapper.latex.rst b/doc/sphinx/credits-wrapper.latex.rst new file mode 100644 index 0000000000..9f7dd49af8 --- /dev/null +++ b/doc/sphinx/credits-wrapper.latex.rst @@ -0,0 +1,3 @@ +.. _credits: + +.. include:: credits.rst diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst index be0b5d5f12..212f0a65b0 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -1,12 +1,3 @@ -.. include:: preamble.rst -.. include:: replaces.rst - -.. _credits: - -------------------------------------------- -Credits -------------------------------------------- - Coq is a proof assistant for higher-order logic, allowing the development of computer programs consistent with their formal specification. It is the result of about ten years of research of the @@ -205,7 +196,7 @@ between sorts. The new version provides powerful tools for easier developments. Cristina Cornes designed an extension of the |Coq| syntax to allow -definition of terms using a powerful pattern-matching analysis in the +definition of terms using a powerful pattern matching analysis in the style of ML programs. Amokrane Saïbi wrote a mechanism to simulate inheritance between types @@ -249,7 +240,7 @@ names to Caml functions corresponding to |Coq| tactic names. Bruno Barras wrote new, more efficient reduction functions. Hugo Herbelin introduced more uniform notations in the |Coq| specification -language: the definitions by fixpoints and pattern-matching have a more +language: the definitions by fixpoints and pattern matching have a more readable syntax. Patrick Loiseleur introduced user-friendly notations for arithmetic expressions. @@ -326,14 +317,14 @@ modules and also to get closer to a certified kernel. Hugo Herbelin introduced a new structure of terms with local definitions. He introduced “qualified” names, wrote a new -pattern-matching compilation algorithm and designed a more compact +pattern matching compilation algorithm and designed a more compact algorithm for checking the logical consistency of universes. He contributed to the simplification of |Coq| internal structures and the optimisation of the system. He added basic tactics for forward reasoning and coercions in patterns. David Delahaye introduced a new language for tactics. General tactics -using pattern-matching on goals and context can directly be written from +using pattern matching on goals and context can directly be written from the |Coq| toplevel. He also provided primitives for the design of user-defined tactics in Caml. @@ -624,8 +615,8 @@ with the library of integers he developed. Beside the libraries, various improvements were contributed to provide a more comfortable end-user language and more expressive tactic language. Hugo -Herbelin and Matthieu Sozeau improved the pattern-matching compilation -algorithm (detection of impossible clauses in pattern-matching, +Herbelin and Matthieu Sozeau improved the pattern matching compilation +algorithm (detection of impossible clauses in pattern matching, automatic inference of the return type). Hugo Herbelin, Pierre Letouzey and Matthieu Sozeau contributed various new convenient syntactic constructs and new tactics or tactic features: more inference of @@ -801,7 +792,7 @@ through :math:`\beta`-redexes that are blocked by the “match” construction (blocked commutative cuts). Relying on the added permissiveness of the guard condition, Hugo -Herbelin could extend the pattern-matching compilation algorithm so that +Herbelin could extend the pattern matching compilation algorithm so that matching over a sequence of terms involving dependencies of a term or of the indices of the type of a term in the type of other terms is systematically supported. @@ -979,7 +970,7 @@ principle than the previously added :math:`\eta`-conversion for function types, based on formulations of the Calculus of Inductive Constructions with typed equality. Primitive projections, which do not carry the parameters of the record and are rigid names (not defined as a -pattern-matching construct), make working with nested records more +pattern matching construct), make working with nested records more manageable in terms of time and space consumption. This extension and universe polymorphism were carried out partly while Matthieu Sozeau was working at the IAS in Princeton. diff --git a/doc/sphinx/genindex.rst b/doc/sphinx/genindex.rst index a991c7f9f8..29f792b3aa 100644 --- a/doc/sphinx/genindex.rst +++ b/doc/sphinx/genindex.rst @@ -1,3 +1,5 @@ +:orphan: + .. hack to get index in TOC ----- diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.html.rst index baf2e0d981..9d90857061 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.html.rst @@ -1,11 +1,16 @@ -.. include:: preamble.rst -.. include:: replaces.rst +========================== + The Coq Reference Manual +========================== + +.. _introduction: + +Introduction +------------ .. include:: introduction.rst ------------------- Table of contents ------------------- +----------------- .. toctree:: :caption: Indexes @@ -23,7 +28,7 @@ Table of contents :caption: Preamble self - credits + credits-wrapper .. toctree:: :caption: The language @@ -80,12 +85,7 @@ Table of contents zebibliography -This material (the Coq Reference Manual) may be distributed only subject to the -terms and conditions set forth in the Open Publication License, v1.0 or later -(the latest version is presently available at -http://www.opencontent.org/openpub). Options A and B are not elected. +License +------- -.. [#PG] Proof-General is available at https://proofgeneral.github.io/. - Optionally, you can enhance it with the minor mode - Company-Coq :cite:`Pit16` - (see https://github.com/cpitclaudel/company-coq). +.. include:: license.rst diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst new file mode 100644 index 0000000000..0f2f7b4897 --- /dev/null +++ b/doc/sphinx/index.latex.rst @@ -0,0 +1,81 @@ +========================== + The Coq Reference Manual +========================== + +Introduction +------------ + +.. include:: introduction.rst + +Credits +------- + +.. include:: credits-wrapper.rst + +License +------- + +.. include:: license.rst + +The language +------------ + +.. toctree:: + + language/gallina-specification-language + language/gallina-extensions + language/coq-library + language/cic + language/module-system + +The proof engine +---------------- + +.. toctree:: + + proof-engine/vernacular-commands + proof-engine/proof-handling + proof-engine/tactics + proof-engine/ltac + proof-engine/detailed-tactic-examples + proof-engine/ssreflect-proof-language + +User extensions +--------------- + +.. toctree:: + + user-extensions/syntax-extensions + user-extensions/proof-schemes + +Practical tools +--------------- + +.. toctree:: + + practical-tools/coq-commands + practical-tools/utilities + practical-tools/coqide + +Addendum +-------- + +.. toctree:: + + addendum/extended-pattern-matching + addendum/implicit-coercions + addendum/canonical-structures + addendum/type-classes + addendum/omega + addendum/micromega + addendum/extraction + addendum/program + addendum/ring + addendum/nsatz + addendum/generalized-rewriting + addendum/parallel-proof-processing + addendum/miscellaneous-extensions + addendum/universe-polymorphism + +.. toctree:: + zebibliography diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index b57e4b209c..b8d2f6b6dc 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -1,9 +1,3 @@ -.. _introduction: - ------------------------- -Introduction ------------------------- - This document is the Reference Manual of the |Coq| proof assistant. To start using Coq, it is advised to first read a tutorial. Links to several tutorials can be found at @@ -41,6 +35,11 @@ are processed from a file. The `coqtop` read-eval-print-loop can also be used directly, for debugging purposes. + .. [#PG] Proof-General is available at https://proofgeneral.github.io/. + Optionally, you can enhance it with the minor mode + Company-Coq :cite:`Pit16` + (see https://github.com/cpitclaudel/company-coq). + - The compiled mode acts as a proof checker taking a file containing a whole development in order to ensure its correctness. Moreover, |Coq|’s compiler provides an output file containing a compact diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 35f45e2e0e..381f8bb661 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _calculusofinductiveconstructions: @@ -605,7 +602,7 @@ Subtyping rules At the moment, we did not take into account one rule between universes which says that any term in a universe of index i is also a term in -the universe of index i+1 (this is the *cumulativity* rule of|Cic|). +the universe of index i+1 (this is the *cumulativity* rule of |Cic|). This property extends the equivalence relation of convertibility into a *subtyping* relation inductively defined by: @@ -640,7 +637,7 @@ a *subtyping* relation inductively defined by: respectively then .. math:: - E[Γ] ⊢ t~w_1 … w_m ≤_{βδιζη} t~w_1' … w_m' + E[Γ] ⊢ t~w_1 … w_m ≤_{βδιζη} t'~w_1' … w_m' (notice that :math:`t` and :math:`t'` are both fully applied, i.e., they have a sort as a type) if @@ -1010,7 +1007,7 @@ the Type hierarchy. It is possible to declare the same inductive definition in the universe :math:`\Type`. The :g:`exType` inductive definition has type - :math:`(\Type(i)→\Prop)→\Type(j)` with the constraint that the parameter :math:`X` of :math:`\kw{exT_intro}` + :math:`(\Type(i)→\Prop)→\Type(j)` with the constraint that the parameter :math:`X` of :math:`\kw{exT}_{\kw{intro}}` has type :math:`\Type(k)` with :math:`k<j` and :math:`k≤ i`. .. coqtop:: all @@ -1028,21 +1025,21 @@ Template polymorphism Inductive types can be made polymorphic over their arguments in :math:`\Type`. -.. opt:: Auto Template Polymorphism +.. flag:: Auto Template Polymorphism - This option, enabled by default, makes every inductive type declared - at level :math:`Type` (without annotations or hiding it behind a - definition) template polymorphic. + This option, enabled by default, makes every inductive type declared + at level :math:`Type` (without annotations or hiding it behind a + definition) template polymorphic. - This can be prevented using the ``notemplate`` attribute. + This can be prevented using the ``notemplate`` attribute. - An inductive type can be forced to be template polymorphic using the - ``template`` attribute. + An inductive type can be forced to be template polymorphic using the + ``template`` attribute. - Template polymorphism and universe polymorphism (see Chapter - :ref:`polymorphicuniverses`) are incompatible, so if the later is - enabled it will prevail over automatic template polymorphism and - cause an error when using the ``template`` attribute. + Template polymorphism and universe polymorphism (see Chapter + :ref:`polymorphicuniverses`) are incompatible, so if the later is + enabled it will prevail over automatic template polymorphism and + cause an error when using the ``template`` attribute. If :math:`A` is an arity of some sort and :math:`s` is a sort, we write :math:`A_{/s}` for the arity obtained from :math:`A` by replacing its sort with :math:`s`. @@ -1123,7 +1120,7 @@ and otherwise in the Type hierarchy. Note that the side-condition about allowed elimination sorts in the rule **Ind-Family** is just to avoid to recompute the allowed elimination -sorts at each instance of a pattern-matching (see Section :ref:`Destructors`). As +sorts at each instance of a pattern matching (see Section :ref:`Destructors`). As an example, let us consider the following definition: .. example:: @@ -1247,7 +1244,7 @@ primitive recursion over the structure. But this operator is rather tedious to implement and use. We choose in this version of |Coq| to factorize the operator for primitive recursion into two more primitive operations as was first suggested by Th. -Coquand in :cite:`Coq92`. One is the definition by pattern-matching. The +Coquand in :cite:`Coq92`. One is the definition by pattern matching. The second one is a definition by guarded fixpoints. @@ -1264,14 +1261,14 @@ The |Coq| term for this proof will be written: .. math:: - \Match~m~\with~(c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | … | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n \endkw + \Match~m~\with~(c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | … | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n \kwend In this expression, if :math:`m` eventually happens to evaluate to :math:`(c_i~u_1 … u_{p_i})` then the expression will behave as specified in its :math:`i`-th branch and it will reduce to :math:`f_i` where the :math:`x_{i1} …x_{ip_i}` are replaced by the :math:`u_1 … u_{p_i}` according to the ι-reduction. -Actually, for type checking a :math:`\Match…\with…\endkw` expression we also need +Actually, for type checking a :math:`\Match…\with…\kwend` expression we also need to know the predicate P to be proved by case analysis. In the general case where :math:`I` is an inductively defined :math:`n`-ary relation, :math:`P` is a predicate over :math:`n+1` arguments: the :math:`n` first ones correspond to the arguments of :math:`I` @@ -1285,7 +1282,7 @@ using the syntax: .. math:: \Match~m~\as~x~\In~I~\_~a~\return~P~\with~ (c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | … - | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n~\endkw + | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n~\kwend The :math:`\as` part can be omitted if either the result type does not depend on :math:`m` (non-dependent elimination) or :math:`m` is a variable (in this case, :math:`m` @@ -1471,6 +1468,8 @@ We write :math:`\{c\}^P` for :math:`\{c:C\}^P` with :math:`C` the type of :math: where .. math:: + :nowrap: + \begin{eqnarray*} P & = & \lambda~l~.~P^\prime\\ f_1 & = & t_1\\ @@ -1711,13 +1710,15 @@ for primitive recursive operators. The following reductions are now possible: .. math:: - \def\plus{\mathsf{plus}} - \def\tri{\triangleright_\iota} - \begin{eqnarray*} - \plus~(\nS~(\nS~\nO))~(\nS~\nO) & \tri & \nS~(\plus~(\nS~\nO)~(\nS~\nO))\\ - & \tri & \nS~(\nS~(\plus~\nO~(\nS~\nO)))\\ - & \tri & \nS~(\nS~(\nS~\nO))\\ - \end{eqnarray*} + :nowrap: + + {\def\plus{\mathsf{plus}} + \def\tri{\triangleright_\iota} + \begin{eqnarray*} + \plus~(\nS~(\nS~\nO))~(\nS~\nO) & \tri & \nS~(\plus~(\nS~\nO)~(\nS~\nO))\\ + & \tri & \nS~(\nS~(\plus~\nO~(\nS~\nO)))\\ + & \tri & \nS~(\nS~(\nS~\nO))\\ + \end{eqnarray*}} .. _Mutual-induction: diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 9de30e2190..85474a3e98 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _thecoqlibrary: The |Coq| library @@ -620,7 +618,7 @@ Finally, it gives the definition of the usual orderings ``le``, Properties of these relations are not initially known, but may be required by the user from modules ``Le`` and ``Lt``. Finally, -``Peano`` gives some lemmas allowing pattern-matching, and a double +``Peano`` gives some lemmas allowing pattern matching, and a double induction principle. .. index:: diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 0fbe7ac70b..636144e0c8 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _extensionsofgallina: Extensions of |Gallina| @@ -22,7 +20,7 @@ expressions. In this sense, the :cmd:`Record` construction allows defining .. _record_grammar: - .. productionlist:: `sentence` + .. productionlist:: sentence record : `record_keyword` `record_body` with … with `record_body` record_keyword : Record | Inductive | CoInductive record_body : `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }. @@ -82,11 +80,13 @@ To build an object of type :n:`@ident`, one should provide the constructor Definition half := mkRat true 1 2 (O_S 1) one_two_irred. Check half. +.. FIXME: move this to the main grammar in the spec chapter + .. _record-named-fields-grammar: .. productionlist:: - term : {| [`field_def` ; … ; `field_def`] |} - field_def : name [binders] := `term` + record_term : {| [`field_def` ; … ; `field_def`] |} + field_def : name [binders] := `record_term` Alternatively, the following syntax allows creating objects by using named fields, as shown in this grammar. The fields do not have to be in any particular order, nor do they have @@ -100,19 +100,25 @@ to be all present if the missing ones can be inferred or prompted for Rat_bottom_cond := O_S 1; Rat_irred_cond := one_two_irred |}. -This syntax can be disabled globally for printing by +The following settings let you control the display format for types: + +.. flag:: Printing Records -.. cmd:: Unset Printing Records + If set, use the record syntax (shown above) as the default display format. -For a given type, one can override this using either +You can override the display format for specified types by adding entries to these tables: -.. cmd:: Add Printing Record @ident +.. table:: Printing Record @qualid + :name: Printing Record -to get record syntax or + Specifies a set of qualids which are displayed as records. Use the + :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of qualids. -.. cmd:: Add Printing Constructor @ident +.. table:: Printing Constructor @qualid + :name: Printing Constructor -to get constructor syntax. + Specifies a set of qualids which are displayed as constructors. Use the + :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of qualids. This syntax can also be used for pattern matching. @@ -145,7 +151,7 @@ available: It can be activated for printing with -.. opt:: Printing Projections +.. flag:: Printing Projections .. example:: @@ -154,12 +160,14 @@ It can be activated for printing with Set Printing Projections. Check top half. +.. FIXME: move this to the main grammar in the spec chapter + .. _record_projections_grammar: .. productionlist:: terms - term : term `.` ( qualid ) - : | term `.` ( qualid arg … arg ) - : | term `.` ( @`qualid` `term` … `term` ) + projection : projection `.` ( `qualid` ) + : | projection `.` ( `qualid` `arg` … `arg` ) + : | projection `.` ( @`qualid` `term` … `term` ) Syntax of Record projections @@ -219,35 +227,35 @@ the errors of inductive definitions, as described in Section Primitive Projections ~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Primitive Projections +.. flag:: Primitive Projections -Turns on the use of primitive -projections when defining subsequent records (even through the ``Inductive`` -and ``CoInductive`` commands). Primitive projections -extended the Calculus of Inductive Constructions with a new binary -term constructor `r.(p)` representing a primitive projection `p` applied -to a record object `r` (i.e., primitive projections are always applied). -Even if the record type has parameters, these do not appear at -applications of the projection, considerably reducing the sizes of -terms when manipulating parameterized records and type checking time. -On the user level, primitive projections can be used as a replacement -for the usual defined ones, although there are a few notable differences. + Turns on the use of primitive + projections when defining subsequent records (even through the ``Inductive`` + and ``CoInductive`` commands). Primitive projections + extended the Calculus of Inductive Constructions with a new binary + term constructor `r.(p)` representing a primitive projection `p` applied + to a record object `r` (i.e., primitive projections are always applied). + Even if the record type has parameters, these do not appear at + applications of the projection, considerably reducing the sizes of + terms when manipulating parameterized records and type checking time. + On the user level, primitive projections can be used as a replacement + for the usual defined ones, although there are a few notable differences. -.. opt:: Printing Primitive Projection Parameters +.. flag:: Printing Primitive Projection Parameters -This compatibility option reconstructs internally omitted parameters at -printing time (even though they are absent in the actual AST manipulated -by the kernel). + This compatibility option reconstructs internally omitted parameters at + printing time (even though they are absent in the actual AST manipulated + by the kernel). -.. opt:: Printing Primitive Projection Compatibility +.. flag:: Printing Primitive Projection Compatibility -This compatibility option (on by default) governs the -printing of pattern-matching over primitive records. + This compatibility option (on by default) governs the + printing of pattern matching over primitive records. Primitive Record Types ++++++++++++++++++++++ -When the :opt:`Primitive Projections` option is on, definitions of +When the :flag:`Primitive Projections` option is on, definitions of record types change meaning. When a type is declared with primitive projections, its :g:`match` construct is disabled (see :ref:`primitive_projections` though). To eliminate the (co-)inductive type, one must use its defined primitive projections. @@ -257,9 +265,9 @@ To eliminate the (co-)inductive type, one must use its defined primitive project For compatibility, the parameters still appear to the user when printing terms even though they are absent in the actual AST manipulated by the kernel. This can be changed by unsetting the -``Printing Primitive Projection Parameters`` flag. Further compatibility +:flag:`Printing Primitive Projection Parameters` flag. Further compatibility printing can be deactivated thanks to the ``Printing Primitive Projection -Compatibility`` option which governs the printing of pattern-matching +Compatibility`` option which governs the printing of pattern matching over primitive records. There are currently two ways to introduce primitive records types: @@ -289,7 +297,7 @@ the folded version delta-reduces to the unfolded version. This allows to precisely mimic the usual unfolding rules of constants. Projections obey the usual ``simpl`` flags of the ``Arguments`` command in particular. There is currently no way to input unfolded primitive projections at the -user-level, and one must use the ``Printing Primitive Projection Compatibility`` +user-level, and one must use the :flag:`Printing Primitive Projection Compatibility` to display unfolded primitive projections as matches and distinguish them from folded ones. @@ -302,7 +310,7 @@ an object of the record type as arguments, and whose body is an application of the unfolded primitive projection of the same name. These constants are used when elaborating partial applications of the projection. One can distinguish them from applications of the primitive -projection if the ``Printing Primitive Projection Parameters`` option +projection if the :flag`Printing Primitive Projection Parameters` option is off: For a primitive projection application, parameters are printed as underscores while for the compatibility projections they are printed as usual. @@ -316,17 +324,17 @@ Variants and extensions of :g:`match` .. _mult-match: -Multiple and nested pattern-matching +Multiple and nested pattern matching ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The basic version of :g:`match` allows pattern-matching on simple +The basic version of :g:`match` allows pattern matching on simple patterns. As an extension, multiple nested patterns or disjunction of patterns are allowed, as in ML-like languages. The extension just acts as a macro that is expanded during parsing into a sequence of match on simple patterns. Especially, a construction defined using the extended match is generally printed -under its expanded form (see :opt:`Printing Matching`). +under its expanded form (see :flag:`Printing Matching`). .. seealso:: :ref:`extendedpatternmatching`. @@ -335,7 +343,7 @@ under its expanded form (see :opt:`Printing Matching`). Pattern-matching on boolean values: the if expression ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -For inductive types with exactly two constructors and for pattern-matching +For inductive types with exactly two constructors and for pattern matching expressions that do not depend on the arguments of the constructors, it is possible to use a ``if … then … else`` notation. For instance, the definition @@ -474,123 +482,93 @@ of :g:`match` expressions. Printing nested patterns +++++++++++++++++++++++++ -.. opt:: Printing Matching +.. flag:: Printing Matching -The Calculus of Inductive Constructions knows pattern-matching only -over simple patterns. It is however convenient to re-factorize nested -pattern-matching into a single pattern-matching over a nested -pattern. + The Calculus of Inductive Constructions knows pattern matching only + over simple patterns. It is however convenient to re-factorize nested + pattern matching into a single pattern matching over a nested + pattern. -When this option is on (default), |Coq|’s printer tries to do such -limited re-factorization. -Turning it off tells |Coq| to print only simple pattern-matching problems -in the same way as the |Coq| kernel handles them. + When this option is on (default), |Coq|’s printer tries to do such + limited re-factorization. + Turning it off tells |Coq| to print only simple pattern matching problems + in the same way as the |Coq| kernel handles them. Factorization of clauses with same right-hand side ++++++++++++++++++++++++++++++++++++++++++++++++++ -.. opt:: Printing Factorizable Match Patterns +.. flag:: Printing Factorizable Match Patterns -When several patterns share the same right-hand side, it is additionally -possible to share the clauses using disjunctive patterns. Assuming that the -printing matching mode is on, this option (on by default) tells |Coq|'s -printer to try to do this kind of factorization. + When several patterns share the same right-hand side, it is additionally + possible to share the clauses using disjunctive patterns. Assuming that the + printing matching mode is on, this option (on by default) tells |Coq|'s + printer to try to do this kind of factorization. Use of a default clause +++++++++++++++++++++++ -.. opt:: Printing Allow Default Clause +.. flag:: Printing Allow Match Default Clause -When several patterns share the same right-hand side which do not depend on the -arguments of the patterns, yet an extra factorization is possible: the -disjunction of patterns can be replaced with a `_` default clause. Assuming that -the printing matching mode and the factorization mode are on, this option (on by -default) tells |Coq|'s printer to use a default clause when relevant. + When several patterns share the same right-hand side which do not depend on the + arguments of the patterns, yet an extra factorization is possible: the + disjunction of patterns can be replaced with a `_` default clause. Assuming that + the printing matching mode and the factorization mode are on, this option (on by + default) tells |Coq|'s printer to use a default clause when relevant. Printing of wildcard patterns ++++++++++++++++++++++++++++++ -.. opt:: Printing Wildcard +.. flag:: Printing Wildcard -Some variables in a pattern may not occur in the right-hand side of -the pattern-matching clause. When this option is on (default), the -variables having no occurrences in the right-hand side of the -pattern-matching clause are just printed using the wildcard symbol -“_”. + Some variables in a pattern may not occur in the right-hand side of + the pattern matching clause. When this option is on (default), the + variables having no occurrences in the right-hand side of the + pattern matching clause are just printed using the wildcard symbol + “_”. Printing of the elimination predicate +++++++++++++++++++++++++++++++++++++ -.. opt:: Printing Synth +.. flag:: Printing Synth -In most of the cases, the type of the result of a matched term is -mechanically synthesizable. Especially, if the result type does not -depend of the matched term. When this option is on (default), -the result type is not printed when |Coq| knows that it can re- -synthesize it. + In most of the cases, the type of the result of a matched term is + mechanically synthesizable. Especially, if the result type does not + depend of the matched term. When this option is on (default), + the result type is not printed when |Coq| knows that it can re- + synthesize it. Printing matching on irrefutable patterns ++++++++++++++++++++++++++++++++++++++++++ -If an inductive type has just one constructor, pattern-matching can be +If an inductive type has just one constructor, pattern matching can be written using the first destructuring let syntax. -.. cmd:: Add Printing Let @ident - - This adds `ident` to the list of inductive types for which pattern-matching - is written using a let expression. - -.. cmd:: Remove Printing Let @ident - - This removes ident from this list. Note that removing an inductive - type from this list has an impact only for pattern-matching written - using :g:`match`. Pattern-matching explicitly written using a destructuring - :g:`let` are not impacted. - -.. cmd:: Test Printing Let for @ident - - This tells if `ident` belongs to the list. - -.. cmd:: Print Table Printing Let +.. table:: Printing Let @qualid + :name: Printing Let - This prints the list of inductive types for which pattern-matching is - written using a let expression. - - The list of inductive types for which pattern-matching is written - using a :g:`let` expression is managed synchronously. This means that it is - sensitive to the command ``Reset``. + Specifies a set of qualids for which pattern matching is displayed using a let expression. + Note that this only applies to pattern matching instances entered with :g:`match`. + It doesn't affect pattern matching explicitly entered with a destructuring + :g:`let`. + Use the :cmd:`Add @table` and :cmd:`Remove @table` commands to update this set. Printing matching on booleans +++++++++++++++++++++++++++++ -If an inductive type is isomorphic to the boolean type, pattern-matching -can be written using ``if`` … ``then`` … ``else`` …: - -.. cmd:: Add Printing If @ident - - This adds ident to the list of inductive types for which pattern-matching is - written using an if expression. - -.. cmd:: Remove Printing If @ident - - This removes ident from this list. +If an inductive type is isomorphic to the boolean type, pattern matching +can be written using ``if`` … ``then`` … ``else`` …. This table controls +which types are written this way: -.. cmd:: Test Printing If for @ident +.. table:: Printing If @qualid + :name: Printing If - This tells if ident belongs to the list. - -.. cmd:: Print Table Printing If - - This prints the list of inductive types for which pattern-matching is - written using an if expression. - -The list of inductive types for which pattern-matching is written -using an ``if`` expression is managed synchronously. This means that it is -sensitive to the command ``Reset``. + Specifies a set of qualids for which pattern matching is displayed using + ``if`` … ``then`` … ``else`` …. Use the :cmd:`Add @table` and :cmd:`Remove @table` + commands to update this set. This example emphasizes what the printing options offer. @@ -672,7 +650,7 @@ than like this: *Limitations* -|term_0| must be built as a *pure pattern-matching tree* (:g:`match … with`) +|term_0| must be built as a *pure pattern matching tree* (:g:`match … with`) with applications only *at the end* of each branch. Function does not support partial application of the function being @@ -700,7 +678,7 @@ terminating functions. - the definition uses pattern matching on dependent types, which ``Function`` cannot deal with yet. - - the definition is not a *pattern-matching tree* as explained above. + - the definition is not a *pattern matching tree* as explained above. .. warn:: Cannot define principle(s) for @ident. @@ -1238,7 +1216,7 @@ component is equal ``nat`` and hence ``M1.T`` as specified. Prints the module type corresponding to :n:`@ident`. -.. opt:: Short Module Printing +.. flag:: Short Module Printing This option (off by default) disables the printing of the types of fields, leaving only their names, for the commands :cmd:`Print Module` and @@ -1513,7 +1491,7 @@ says that the implicit argument is maximally inserted. Each implicit argument can be declared to have to be inserted maximally or non maximally. This can be governed argument per argument by the command -:cmd:`Arguments (implicits)` or globally by the :opt:`Maximal Implicit Insertion` option. +:cmd:`Arguments (implicits)` or globally by the :flag:`Maximal Implicit Insertion` option. .. seealso:: :ref:`displaying-implicit-args`. @@ -1745,65 +1723,65 @@ appear strictly in the body of the type, they are implicit. Mode for automatic declaration of implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Implicit Arguments +.. flag:: Implicit Arguments -This option (off by default) allows to systematically declare implicit -the arguments detectable as such. Auto-detection of implicit arguments is -governed by options controlling whether strict and contextual implicit -arguments have to be considered or not. + This option (off by default) allows to systematically declare implicit + the arguments detectable as such. Auto-detection of implicit arguments is + governed by options controlling whether strict and contextual implicit + arguments have to be considered or not. .. _controlling-strict-implicit-args: Controlling strict implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Strict Implicit +.. flag:: Strict Implicit -When the mode for automatic declaration of implicit arguments is on, -the default is to automatically set implicit only the strict implicit -arguments plus, for historical reasons, a small subset of the non-strict -implicit arguments. To relax this constraint and to set -implicit all non strict implicit arguments by default, you can turn this -option off. + When the mode for automatic declaration of implicit arguments is on, + the default is to automatically set implicit only the strict implicit + arguments plus, for historical reasons, a small subset of the non-strict + implicit arguments. To relax this constraint and to set + implicit all non strict implicit arguments by default, you can turn this + option off. -.. opt:: Strongly Strict Implicit +.. flag:: Strongly Strict Implicit -Use this option (off by default) to capture exactly the strict implicit -arguments and no more than the strict implicit arguments. + Use this option (off by default) to capture exactly the strict implicit + arguments and no more than the strict implicit arguments. .. _controlling-contextual-implicit-args: Controlling contextual implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Contextual Implicit +.. flag:: Contextual Implicit -By default, |Coq| does not automatically set implicit the contextual -implicit arguments. You can turn this option on to tell |Coq| to also -infer contextual implicit argument. + By default, |Coq| does not automatically set implicit the contextual + implicit arguments. You can turn this option on to tell |Coq| to also + infer contextual implicit argument. .. _controlling-rev-pattern-implicit-args: Controlling reversible-pattern implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Reversible Pattern Implicit +.. flag:: Reversible Pattern Implicit -By default, |Coq| does not automatically set implicit the reversible-pattern -implicit arguments. You can turn this option on to tell |Coq| to also infer -reversible-pattern implicit argument. + By default, |Coq| does not automatically set implicit the reversible-pattern + implicit arguments. You can turn this option on to tell |Coq| to also infer + reversible-pattern implicit argument. .. _controlling-insertion-implicit-args: Controlling the insertion of implicit arguments not followed by explicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Maximal Implicit Insertion +.. flag:: Maximal Implicit Insertion -Assuming the implicit argument mode is on, this option (off by default) -declares implicit arguments to be automatically inserted when a -function is partially applied and the next argument of the function is -an implicit one. + Assuming the implicit argument mode is on, this option (off by default) + declares implicit arguments to be automatically inserted when a + function is partially applied and the next argument of the function is + an implicit one. .. _explicit-applications: @@ -1875,20 +1853,20 @@ if each of them is to be used maximally or not, use the command Explicit displaying of implicit arguments for pretty-printing ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Printing Implicit +.. flag:: Printing Implicit -By default, the basic pretty-printing rules hide the inferable implicit -arguments of an application. Turn this option on to force printing all -implicit arguments. + By default, the basic pretty-printing rules hide the inferable implicit + arguments of an application. Turn this option on to force printing all + implicit arguments. -.. opt:: Printing Implicit Defensive +.. flag:: Printing Implicit Defensive -By default, the basic pretty-printing rules display the implicit -arguments that are not detected as strict implicit arguments. This -“defensive” mode can quickly make the display cumbersome so this can -be deactivated by turning this option off. + By default, the basic pretty-printing rules display the implicit + arguments that are not detected as strict implicit arguments. This + “defensive” mode can quickly make the display cumbersome so this can + be deactivated by turning this option off. -.. seealso:: :opt:`Printing All`. +.. seealso:: :flag:`Printing All`. Interaction with subtyping ~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1913,14 +1891,14 @@ but succeeds in Deactivation of implicit arguments for parsing ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Parsing Explicit +.. flag:: Parsing Explicit -Turning this option on (it is off by default) deactivates the use of implicit arguments. + Turning this option on (it is off by default) deactivates the use of implicit arguments. -In this case, all arguments of constants, inductive types, -constructors, etc, including the arguments declared as implicit, have -to be given as if no arguments were implicit. By symmetry, this also -affects printing. + In this case, all arguments of constants, inductive types, + constructors, etc, including the arguments declared as implicit, have + to be given as if no arguments were implicit. By symmetry, this also + affects printing. Canonical structures ~~~~~~~~~~~~~~~~~~~~ @@ -2132,32 +2110,32 @@ to coercions are provided in :ref:`implicitcoercions`. Printing constructions in full ------------------------------ -.. opt:: Printing All +.. flag:: Printing All -Coercions, implicit arguments, the type of pattern-matching, but also -notations (see :ref:`syntaxextensionsandinterpretationscopes`) can obfuscate the behavior of some -tactics (typically the tactics applying to occurrences of subterms are -sensitive to the implicit arguments). Turning this option on -deactivates all high-level printing features such as coercions, -implicit arguments, returned type of pattern-matching, notations and -various syntactic sugar for pattern-matching or record projections. -Otherwise said, :opt:`Printing All` includes the effects of the options -:opt:`Printing Implicit`, :opt:`Printing Coercions`, :opt:`Printing Synth`, -:opt:`Printing Projections`, and :opt:`Printing Notations`. To reactivate -the high-level printing features, use the command ``Unset Printing All``. + Coercions, implicit arguments, the type of pattern matching, but also + notations (see :ref:`syntaxextensionsandinterpretationscopes`) can obfuscate the behavior of some + tactics (typically the tactics applying to occurrences of subterms are + sensitive to the implicit arguments). Turning this option on + deactivates all high-level printing features such as coercions, + implicit arguments, returned type of pattern matching, notations and + various syntactic sugar for pattern matching or record projections. + Otherwise said, :flag:`Printing All` includes the effects of the options + :flag:`Printing Implicit`, :flag:`Printing Coercions`, :flag:`Printing Synth`, + :flag:`Printing Projections`, and :flag:`Printing Notations`. To reactivate + the high-level printing features, use the command ``Unset Printing All``. .. _printing-universes: Printing universes ------------------ -.. opt:: Printing Universes +.. flag:: Printing Universes -Turn this option on to activate the display of the actual level of each -occurrence of :g:`Type`. See :ref:`Sorts` for details. This wizard option, in -combination with :opt:`Printing All` can help to diagnose failures to unify -terms apparently identical but internally different in the Calculus of Inductive -Constructions. + Turn this option on to activate the display of the actual level of each + occurrence of :g:`Type`. See :ref:`Sorts` for details. This wizard option, in + combination with :flag:`Printing All` can help to diagnose failures to unify + terms apparently identical but internally different in the Calculus of Inductive + Constructions. The constraints on the internal level of the occurrences of Type (see :ref:`Sorts`) can be printed using the command @@ -2219,7 +2197,7 @@ form is appending to its name, indicating how the variables of its defining context are instantiated. The variables of the context of the existential variables which are -instantiated by themselves are not written, unless the flag ``Printing Existential Instances`` +instantiated by themselves are not written, unless the flag :flag:`Printing Existential Instances` is on (see Section :ref:`explicit-display-existentials`), and this is why an existential variable used in the same context as its context of definition is written with no instance. @@ -2241,11 +2219,11 @@ with a named-goal selector, see :ref:`goal-selectors`). Explicit displaying of existential instances for pretty-printing ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Printing Existential Instances +.. flag:: Printing Existential Instances -This option (off by default) activates the full display of how the -context of an existential variable is instantiated at each of the -occurrences of the existential variable. + This option (off by default) activates the full display of how the + context of an existential variable is instantiated at each of the + occurrences of the existential variable. .. _tactics-in-terms: diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 075235a8e2..daf34500bf 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -216,6 +216,11 @@ numbers (see :ref:`datatypes`). Negative integers are not at the same level as :token:`num`, for this would make precedence unnatural. +.. index:: + single: Set (sort) + single: Prop + single: Type + Sorts ----- @@ -262,6 +267,8 @@ fun and forall gets identical. Moreover, parentheses can be omitted in the case of a single sequence of bindings sharing the same type (e.g.: :g:`fun (x y z : A) => t` can be shortened in :g:`fun x y z : A => t`). +.. index:: fun ... => ... + Abstractions ------------ @@ -282,6 +289,8 @@ a let-binder occurs in the list of binders, it is expanded to a let-in definition (see Section :ref:`let-in`). +.. index:: forall + Products -------- @@ -320,6 +329,11 @@ The notation :n:`(@ident := @term)` for arguments is used for making explicit the value of implicit arguments (see Section :ref:`explicit-applications`). +.. index:: + single: ... : ... (type cast) + single: ... <: ... + single: ... <<: ... + Type cast --------- @@ -329,6 +343,11 @@ the type of :token:`term` to be :token:`type`. :n:`@term <: @type` locally sets up the virtual machine for checking that :token:`term` has type :token:`type`. +:n:`@term <<: @type` uses native compilation for checking that :token:`term` +has type :token:`type`. + +.. index:: _ + Inferable subterms ------------------ @@ -336,6 +355,8 @@ Expressions often contain redundant pieces of information. Subterms that can be automatically inferred by Coq can be replaced by the symbol ``_`` and Coq will guess the missing piece of information. +.. index:: let ... := ... (term) + .. _let-in: Let-in definitions @@ -347,17 +368,19 @@ denotes the local binding of :token:`term` to the variable definition of functions: :n:`let @ident {+ @binder} := @term in @term’` stands for :n:`let @ident := fun {+ @binder} => @term in @term’`. +.. index:: match ... with ... + Definition by case analysis --------------------------- Objects of inductive types can be destructurated by a case-analysis -construction called *pattern-matching* expression. A pattern-matching +construction called *pattern matching* expression. A pattern matching expression is used to analyze the structure of an inductive object and to apply specific treatments accordingly. -This paragraph describes the basic form of pattern-matching. See +This paragraph describes the basic form of pattern matching. See Section :ref:`Mult-match` and Chapter :ref:`extendedpatternmatching` for the description -of the general form. The basic form of pattern-matching is characterized +of the general form. The basic form of pattern matching is characterized by a single :token:`match_item` expression, a :token:`mult_pattern` restricted to a single :token:`pattern` and :token:`pattern` restricted to the form :n:`@qualid {* @ident}`. @@ -365,9 +388,9 @@ single :token:`pattern` and :token:`pattern` restricted to the form The expression match ":token:`term`:math:`_0` :token:`return_type` with :token:`pattern`:math:`_1` => :token:`term`:math:`_1` :math:`|` … :math:`|` :token:`pattern`:math:`_n` => :token:`term`:math:`_n` end" denotes a -*pattern-matching* over the term :token:`term`:math:`_0` (expected to be +*pattern matching* over the term :token:`term`:math:`_0` (expected to be of an inductive type :math:`I`). The terms :token:`term`:math:`_1`\ …\ -:token:`term`:math:`_n` are the *branches* of the pattern-matching +:token:`term`:math:`_n` are the *branches* of the pattern matching expression. Each of :token:`pattern`:math:`_i` has a form :token:`qualid` :token:`ident` where :token:`qualid` must denote a constructor. There should be exactly one branch for every constructor of :math:`I`. @@ -380,7 +403,7 @@ inferred from the type of the branches [2]_. In the *dependent* case, there are three subcases. In the first subcase, the type in each branch may depend on the exact value being matched in -the branch. In this case, the whole pattern-matching itself depends on +the branch. In this case, the whole pattern matching itself depends on the term being matched. This dependency of the term being matched in the return type is expressed with an “as :token:`ident`” clause where :token:`ident` is dependent in the return type. For instance, in the following example: @@ -401,7 +424,7 @@ is dependent in the return type. For instance, in the following example: the branches have respective types ":g:`or (eq bool true true) (eq bool true false)`" and ":g:`or (eq bool false true) (eq bool false false)`" while the whole -pattern-matching expression has type ":g:`or (eq bool b true) (eq bool b false)`", +pattern matching expression has type ":g:`or (eq bool b true) (eq bool b false)`", the identifier :g:`b` being used to represent the dependency. .. note:: @@ -424,7 +447,7 @@ as the equality predicate (see Section :ref:`coq-equality`), the order predicate on natural numbers or the type of lists of a given length (see Section :ref:`matching-dependent`). In this configuration, the type of each branch can depend on the type dependencies specific to the -branch and the whole pattern-matching expression has a type determined +branch and the whole pattern matching expression has a type determined by the specific dependencies in the type of the term being matched. This dependency of the return type in the annotations of the inductive type is expressed using a “:g:`in` :math:`I` :g:`_ … _` :token:`pattern`:math:`_1` … @@ -453,13 +476,13 @@ For instance, in the following example: the type of the branch is :g:`eq A x x` because the third argument of :g:`eq` is :g:`x` in the type of the pattern :g:`eq_refl`. On the contrary, the -type of the whole pattern-matching expression has type :g:`eq A y x` because the +type of the whole pattern matching expression has type :g:`eq A y x` because the third argument of eq is y in the type of H. This dependency of the case analysis in the third argument of :g:`eq` is expressed by the identifier :g:`z` in the return type. Finally, the third subcase is a combination of the first and second -subcase. In particular, it only applies to pattern-matching on terms in +subcase. In particular, it only applies to pattern matching on terms in a type with annotations. For this third subcase, both the clauses ``as`` and ``in`` are available. @@ -467,6 +490,10 @@ There are specific notations for case analysis on types with one or two constructors: ``if … then … else …`` and ``let (…,…) := … in …`` (see Sections :ref:`if-then-else` and :ref:`irrefutable-patterns`). +.. index:: + single: fix + single: cofix + Recursive functions ------------------- @@ -916,7 +943,7 @@ Parametrized inductive types sort for the inductive definition and will produce a less convenient rule for case elimination. -.. opt:: Uniform Inductive Parameters +.. flag:: Uniform Inductive Parameters When this option is set (it is off by default), inductive definitions are abstracted over their parameters @@ -953,7 +980,7 @@ Variants The :cmd:`Variant` command is identical to the :cmd:`Inductive` command, except that it disallows recursive definition of types (for instance, lists cannot be defined using :cmd:`Variant`). No induction scheme is generated for - this variant, unless option :opt:`Nonrecursive Elimination Schemes` is on. + this variant, unless option :flag:`Nonrecursive Elimination Schemes` is on. .. exn:: The @num th argument of @ident must be @ident in @type. :undocumented: @@ -1099,7 +1126,7 @@ constructions. .. cmd:: Fixpoint @ident @binders {? {struct @ident} } {? : @type } := @term - This command allows defining functions by pattern-matching over inductive + This command allows defining functions by pattern matching over inductive objects using a fixed point construction. The meaning of this declaration is to define :token:`ident` a recursive function with arguments specified by the :token:`binders` such that :token:`ident` applied to arguments @@ -1302,7 +1329,7 @@ Chapter :ref:`Tactics`. The basic assertion command is: You are asserting a new statement while already being in proof editing mode. This feature, called nested proofs, is disabled by default. - To activate it, turn option :opt:`Nested Proofs Allowed` on. + To activate it, turn option :flag:`Nested Proofs Allowed` on. .. cmdv:: Lemma @ident {? @binders } : @type Remark @ident {? @binders } : @type @@ -1376,7 +1403,7 @@ using the keyword :cmd:`Qed`. .. note:: #. Several statements can be simultaneously asserted provided option - :opt:`Nested Proofs Allowed` was turned on. + :flag:`Nested Proofs Allowed` was turned on. #. Not only other assertions but any vernacular command can be given while in the process of proving a given assertion. In this case, the diff --git a/doc/sphinx/language/module-system.rst b/doc/sphinx/language/module-system.rst index e6a6736654..15fee91245 100644 --- a/doc/sphinx/language/module-system.rst +++ b/doc/sphinx/language/module-system.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _themodulesystem: The Module System diff --git a/doc/sphinx/license.rst b/doc/sphinx/license.rst new file mode 100644 index 0000000000..232b04211c --- /dev/null +++ b/doc/sphinx/license.rst @@ -0,0 +1,4 @@ +This material (the Coq Reference Manual) may be distributed only subject to the +terms and conditions set forth in the Open Publication License, v1.0 or later +(the latest version is presently available at +http://www.opencontent.org/openpub). Options A and B are not elected. diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 9498f37c7e..343ca9ed7d 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _thecoqcommands: The |Coq| commands diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index bc6a074a27..9455228e7d 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _coqintegrateddevelopmentenvironment: |Coq| Integrated Development Environment @@ -263,7 +261,7 @@ for the ∀ symbol. A list of symbol codes is available at An alternative method which does not require to know the hexadecimal code of the character is to use an Input Method Editor. On POSIX systems (Linux distributions, BSD variants and MacOS X), you can -use `uim` version 1.6 or later which provides a :math:`\LaTeX`-style input +use `uim` version 1.6 or later which provides a LaTeX-style input method. To configure uim, execute uim-pref-gtk as your regular user. In the diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index b9a4d2a7bd..5d300c3d6d 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _utilities: --------------------- diff --git a/doc/sphinx/preamble.rst b/doc/sphinx/preamble.rst deleted file mode 100644 index 395f558a85..0000000000 --- a/doc/sphinx/preamble.rst +++ /dev/null @@ -1,92 +0,0 @@ -.. preamble:: - - \[ - \newcommand{\alors}{\textsf{then}} - \newcommand{\alter}{\textsf{alter}} - \newcommand{\as}{\kw{as}} - \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} - \newcommand{\bool}{\textsf{bool}} - \newcommand{\case}{\kw{case}} - \newcommand{\conc}{\textsf{conc}} - \newcommand{\cons}{\textsf{cons}} - \newcommand{\consf}{\textsf{consf}} - \newcommand{\conshl}{\textsf{cons\_hl}} - \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} - \newcommand{\emptyf}{\textsf{emptyf}} - \newcommand{\End}{\kw{End}} - \newcommand{\endkw}{\kw{end}} - \newcommand{\EqSt}{\textsf{EqSt}} - \newcommand{\even}{\textsf{even}} - \newcommand{\evenO}{\textsf{even_O}} - \newcommand{\evenS}{\textsf{even_S}} - \newcommand{\false}{\textsf{false}} - \newcommand{\filter}{\textsf{filter}} - \newcommand{\Fix}{\kw{Fix}} - \newcommand{\fix}{\kw{fix}} - \newcommand{\for}{\textsf{for}} - \newcommand{\forest}{\textsf{forest}} - \newcommand{\from}{\textsf{from}} - \newcommand{\Functor}{\kw{Functor}} - \newcommand{\haslength}{\textsf{has\_length}} - \newcommand{\hd}{\textsf{hd}} - \newcommand{\ident}{\textsf{ident}} - \newcommand{\In}{\kw{in}} - \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} - \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} - \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} - \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} - \newcommand{\injective}{\kw{injective}} - \newcommand{\kw}[1]{\textsf{#1}} - \newcommand{\lb}{\lambda} - \newcommand{\length}{\textsf{length}} - \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} - \newcommand{\List}{\textsf{list}} - \newcommand{\lra}{\longrightarrow} - \newcommand{\Match}{\kw{match}} - \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} - \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} - \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} - \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} - \newcommand{\mto}{.\;} - \newcommand{\Nat}{\mathbb{N}} - \newcommand{\nat}{\textsf{nat}} - \newcommand{\Nil}{\textsf{nil}} - \newcommand{\nilhl}{\textsf{nil\_hl}} - \newcommand{\nO}{\textsf{O}} - \newcommand{\node}{\textsf{node}} - \newcommand{\nS}{\textsf{S}} - \newcommand{\odd}{\textsf{odd}} - \newcommand{\oddS}{\textsf{odd_S}} - \newcommand{\ovl}[1]{\overline{#1}} - \newcommand{\Pair}{\textsf{pair}} - \newcommand{\Prod}{\textsf{prod}} - \newcommand{\Prop}{\textsf{Prop}} - \newcommand{\return}{\kw{return}} - \newcommand{\Set}{\textsf{Set}} - \newcommand{\si}{\textsf{if}} - \newcommand{\sinon}{\textsf{else}} - \newcommand{\Sort}{\cal S} - \newcommand{\Str}{\textsf{Stream}} - \newcommand{\Struct}{\kw{Struct}} - \newcommand{\subst}[3]{#1\{#2/#3\}} - \newcommand{\tl}{\textsf{tl}} - \newcommand{\tree}{\textsf{tree}} - \newcommand{\true}{\textsf{true}} - \newcommand{\Type}{\textsf{Type}} - \newcommand{\unfold}{\textsf{unfold}} - \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} - \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} - \newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]} - \newcommand{\WFE}[1]{\WF{E}{#1}} - \newcommand{\WFT}[2]{#1[] \vdash {\cal W\!F}(#2)} - \newcommand{\WFTWOLINES}[2]{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} - \newcommand{\with}{\kw{with}} - \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} - \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} - \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} - \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} - \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} - \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} - \newcommand{\zeroone}[1]{[{#1}]} - \newcommand{\zeros}{\textsf{zeros}} - \] diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 70d46e034a..edd83b7cee 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _ltac: The tactic language @@ -27,14 +24,14 @@ represent respectively the natural and integer numbers, the authorized identificators and qualified names, Coq terms and patterns and all the atomic tactics described in Chapter :ref:`tactics`. The syntax of :token:`cpattern` is the same as that of terms, but it is extended with pattern matching -metavariables. In :token:`cpattern`, a pattern-matching metavariable is +metavariables. In :token:`cpattern`, a pattern matching metavariable is represented with the syntax :g:`?id` where :g:`id` is an :token:`ident`. The notation :g:`_` can also be used to denote metavariable whose instance is irrelevant. In the notation :g:`?id`, the identifier allows us to keep instantiations and to make constraints whereas :g:`_` shows that we are not -interested in what will be matched. On the right hand side of pattern-matching +interested in what will be matched. On the right hand side of pattern matching clauses, the named metavariables are used without the question mark prefix. There -is also a special notation for second-order pattern-matching problems: in an +is also a special notation for second-order pattern matching problems: in an applicative pattern of the form :g:`@?id id1 … idn`, the variable id matches any complex expression with (possible) dependencies in the variables :g:`id1 … idn` and returns a functional term of the form :g:`fun id1 … idn => term`. @@ -717,6 +714,7 @@ Local definitions Local definitions can be done as follows: .. tacn:: let @ident__1 := @expr__1 {* with @ident__i := @expr__i} in @expr + :name: let ... := ... each :n:`@expr__i` is evaluated to :n:`v__i`, then, :n:`@expr` is evaluated by substituting :n:`v__i` to each occurrence of :n:`@ident__i`, for @@ -835,7 +833,7 @@ We can carry out pattern matching on terms with: matching subterm is tried. If no further subterm matches, the next clause is tried. Matching subterms are considered top-bottom and from left to right (with respect to the raw printing obtained by setting option - :opt:`Printing All`). + :flag:`Printing All`). .. example:: @@ -1189,6 +1187,7 @@ Info trace not printed. .. opt:: Info Level @num + :name: Info Level This option is an alternative to the :cmd:`Info` command. @@ -1199,7 +1198,7 @@ Info trace Interactive debugger ~~~~~~~~~~~~~~~~~~~~ -.. opt:: Ltac Debug +.. flag:: Ltac Debug This option governs the step-by-step debugger that comes with the |Ltac| interpreter @@ -1227,7 +1226,7 @@ following: A non-interactive mode for the debugger is available via the option: -.. opt:: Ltac Batch Debug +.. flag:: Ltac Batch Debug This option has the effect of presenting a newline at every prompt, when the debugger is on. The debug log thus created, which does not require @@ -1248,7 +1247,7 @@ indicates the time spent in a tactic depending on its calling context. Thus it allows to locate the part of a tactic definition that contains the performance issue. -.. opt:: Ltac Profiling +.. flag:: Ltac Profiling This option enables and disables the profiler. @@ -1334,7 +1333,7 @@ performance issue. benchmarking purposes. You can also pass the ``-profile-ltac`` command line option to ``coqc``, which -turns the :opt:`Ltac Profiling` option on at the beginning of each document, +turns the :flag:`Ltac Profiling` option on at the beginning of each document, and performs a :cmd:`Show Ltac Profile` at the end. .. warning:: diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index b1e769c571..4b1b7719c5 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -1,4 +1,3 @@ -.. include:: ../replaces.rst .. _proofhandling: ------------------- @@ -113,7 +112,7 @@ list of assertion commands is given in :ref:`Assertions`. The command Aborts the editing of the proof named :token:`ident` (in case you have nested proofs). - .. seealso:: :opt:`Nested Proofs Allowed` + .. seealso:: :flag:`Nested Proofs Allowed` .. cmdv:: Abort All @@ -201,13 +200,14 @@ The following options modify the behavior of ``Proof using``. .. opt:: Default Proof Using "@expression" + :name: Default Proof Using Use :n:`@expression` as the default ``Proof using`` value. E.g. ``Set Default Proof Using "a b"`` will complete all ``Proof`` commands not followed by a ``using`` part with ``using a b``. -.. opt:: Suggest Proof Using +.. flag:: Suggest Proof Using When :cmd:`Qed` is performed, suggest a ``using`` annotation if the user did not provide one. @@ -442,13 +442,19 @@ The following example script illustrates all these features: You tried to apply a tactic but no goals were under focus. Using :n:`@bullet` is mandatory here. -.. exn:: No such goal. Try unfocusing with %{. +.. FIXME: the :noindex: below works around a Sphinx issue. + (https://github.com/sphinx-doc/sphinx/issues/4979) + It should be removed once that issue is fixed. + +.. exn:: No such goal. Try unfocusing with %}. + :noindex: You just finished a goal focused by ``{``, you must unfocus it with ``}``. Set Bullet Behavior ``````````````````` .. opt:: Bullet Behavior %( "None" %| "Strict Subproofs" %) + :name: Bullet Behavior This option controls the bullet behavior and can take two possible values: @@ -581,6 +587,7 @@ Controlling the effect of proof editing commands .. opt:: Hyps Limit @num + :name: Hyps Limit This option controls the maximum number of hypotheses displayed in goals after the application of a tactic. All the hypotheses remain usable @@ -589,7 +596,7 @@ Controlling the effect of proof editing commands available hypotheses. -.. opt:: Automatic Introduction +.. flag:: Automatic Introduction This option controls the way binders are handled in assertion commands such as :n:`Theorem @ident {? @binders} : @term`. When the @@ -601,7 +608,7 @@ Controlling the effect of proof editing commands has to be used to move the assumptions to the local context. -.. opt:: Nested Proofs Allowed +.. flag:: Nested Proofs Allowed When turned on (it is off by default), this option enables support for nested proofs: a new assertion command can be inserted before the current proof is diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 8656e5eb3e..52609546d5 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _thessreflectprooflanguage: ------------------------------ @@ -104,8 +102,8 @@ this corresponds to working in the following context: Unset Printing Implicit Defensive. .. seealso:: - :opt:`Implicit Arguments`, :opt:`Strict Implicit`, - :opt:`Printing Implicit Defensive` + :flag:`Implicit Arguments`, :flag:`Strict Implicit`, + :flag:`Printing Implicit Defensive` .. _compatibility_issues_ssr: @@ -2703,7 +2701,7 @@ typeclass inference. No inference for ``t``. Unresolved instances are quantified in the (inferred) type of ``t`` and abstracted in ``t``. -.. opt:: SsrHave NoTCResolution +.. flag:: SsrHave NoTCResolution This option restores the behavior of |SSR| 1.4 and below (never resolve typeclasses). @@ -3867,7 +3865,7 @@ duplication of function arguments. These copies usually end up in types hidden by the implicit arguments machinery or by user-defined notations. In these situations computing the right occurrence numbers is very tedious because they must be counted on the goal as printed -after setting the Printing All flag. Moreover the resulting script is +after setting the :flag:`Printing All` flag. Moreover the resulting script is not really informative for the reader, since it refers to occurrence numbers he cannot easily see. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index fb121c82ec..f99c539251 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _tactics: Tactics @@ -51,7 +48,8 @@ specified, the default selector is used. tactic_invocation : toplevel_selector : tactic. : |tactic . -.. opt:: Default Goal Selector @toplevel_selector +.. opt:: Default Goal Selector "@toplevel_selector" + :name: Default Goal Selector This option controls the default selector, used when no selector is specified when applying a tactic. The initial value is 1, hence the @@ -127,7 +125,7 @@ that occurrences have to be selected in the hypotheses named :token:`ident`. If no numbers are given for hypothesis :token:`ident`, then all the occurrences of :token:`term` in the hypothesis are selected. If numbers are given, they refer to occurrences of :token:`term` when the term is printed -using option :opt:`Printing All`, counting from left to right. In particular, +using option :flag:`Printing All`, counting from left to right. In particular, occurrences of :token:`term` in implicit arguments (see :ref:`ImplicitArguments`) or coercions (see :ref:`Coercions`) are counted. @@ -451,7 +449,7 @@ Applying theorems ``forall A, ... -> A``. Excluding this kind of lemma can be avoided by setting the following option: -.. opt:: Universal Lemma Under Conjunction +.. flag:: Universal Lemma Under Conjunction This option, which preserves compatibility with versions of Coq prior to 8.4 is also available for :n:`apply @term in @ident` (see :tacn:`apply ... in`). @@ -476,7 +474,7 @@ Applying theorems :token:`ident`. Tuples are decomposed in a width-first left-to-right order (for instance if the type of :g:`H1` is :g:`A <-> B` and the type of :g:`H2` is :g:`A` then :g:`apply H1 in H2` transforms the type of :g:`H2` - into :g:`B`). The tactic :tacn:`apply` relies on first-order pattern-matching + into :g:`B`). The tactic :tacn:`apply` relies on first-order pattern matching with dependent types. .. exn:: Statement without assumptions. @@ -855,7 +853,7 @@ Managing the local context so that all the arguments of the i-th constructors of the corresponding inductive type are introduced can be controlled with the following option: - .. opt:: Bracketing Last Introduction Pattern + .. flag:: Bracketing Last Introduction Pattern Force completion, if needed, when the last introduction pattern is a disjunctive or conjunctive pattern (on by default). @@ -1298,7 +1296,7 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. This is equivalent to :n:`generalize @term` but it generalizes only over the specified occurrences of :n:`@term` (counting from left to right on the - expression printed using option :opt:`Printing All`). + expression printed using option :flag:`Printing All`). .. tacv:: generalize @term as @ident @@ -2041,14 +2039,14 @@ and an explanation of the underlying technique. to the number of new equalities. The original equality is erased if it corresponds to a hypothesis. - .. opt:: Structural Injection + .. flag:: Structural Injection This option ensure that :n:`injection @term` erases the original hypothesis and leaves the generated equalities in the context rather than putting them as antecedents of the current goal, as if giving :n:`injection @term as` (with an empty list of names). This option is off by default. - .. opt:: Keep Proof Equalities + .. flag:: Keep Proof Equalities By default, :tacn:`injection` only creates new equalities between :n:`@terms` whose type is in sort :g:`Type` or :g:`Set`, thus implementing a special @@ -2080,7 +2078,7 @@ and an explanation of the underlying technique. being processed. By default, no equalities are generated if they relate two proofs (i.e. equalities between :n:`@terms` whose type is in sort :g:`Prop`). This behavior can be turned off by using the option - :opt`Keep Proof Equalities`. + :flag`Keep Proof Equalities`. .. tacv:: inversion @num @@ -2590,7 +2588,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. context for which an equality of the form :n:`@ident = t` or :n:`t = @ident` or :n:`@ident := t` exists, with :n:`@ident` not occurring in ``t``. - .. opt:: Regular Subst Tactic + .. flag:: Regular Subst Tactic This option controls the behavior of :tacn:`subst`. When it is activated (it is by default), :tacn:`subst` also deals with the following corner cases: @@ -2725,7 +2723,7 @@ the conversion in hypotheses :n:`{+ @ident}`. :math:`\beta` (reduction of functional application), :math:`\delta` (unfolding of transparent constants, see :ref:`vernac-controlling-the-reduction-strategies`), :math:`\iota` (reduction of - pattern-matching over a constructed term, and unfolding of :g:`fix` and + pattern matching over a constructed term, and unfolding of :g:`fix` and :g:`cofix` expressions) and :math:`\zeta` (contraction of local definitions), the flags are either ``beta``, ``delta``, ``match``, ``fix``, ``cofix``, ``iota`` or ``zeta``. The ``iota`` flag is a shorthand for ``match``, ``fix`` @@ -2808,12 +2806,13 @@ the conversion in hypotheses :n:`{+ @ident}`. compilation cost is higher, so it is worth using only for intensive computations. - .. opt:: NativeCompute Profiling + .. flag:: NativeCompute Profiling On Linux, if you have the ``perf`` profiler installed, this option makes it possible to profile ``native_compute`` evaluations. - .. opt:: NativeCompute Profile Filename + .. opt:: NativeCompute Profile Filename @string + :name: NativeCompute Profile Filename This option specifies the profile output; the default is ``native_compute_profile.data``. The actual filename used @@ -2824,7 +2823,7 @@ the conversion in hypotheses :n:`{+ @ident}`. on the profile file to see the results. Consult the ``perf`` documentation for more details. -.. opt:: Debug Cbv +.. flag:: Debug Cbv This option makes :tacn:`cbv` (and its derivative :tacn:`compute`) print information about the constants it encounters and the unfolding decisions it @@ -2991,7 +2990,7 @@ the conversion in hypotheses :n:`{+ @ident}`. This applies ``simpl`` only to the :n:`{+ @num}` applicative subterms whose head occurrence is :n:`@qualid` (or :n:`@string`). -.. opt:: Debug RAKAM +.. flag:: Debug RAKAM This option makes :tacn:`cbn` print various debugging information. ``RAKAM`` is the Refolding Algebraic Krivine Abstract Machine. @@ -3198,10 +3197,11 @@ hints of the database named core. The following options enable printing of informative or debug information for the :tacn:`auto` and :tacn:`trivial` tactics: -.. opt:: Info Auto -.. opt:: Debug Auto -.. opt:: Info Trivial -.. opt:: Debug Trivial +.. flag:: Info Auto + Debug Auto + Info Trivial + Debug Trivial + :undocumented: .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` @@ -3231,8 +3231,9 @@ Note that ``ex_intro`` should be declared as a hint. :tacn:`eauto` also obeys the following options: -.. opt:: Info Eauto -.. opt:: Debug Eauto +.. flag:: Info Eauto + Debug Eauto + :undocumented: .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` @@ -3566,7 +3567,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is .. note:: - One can use an ``Extern`` hint with no pattern to do pattern-matching on + One can use an ``Extern`` hint with no pattern to do pattern matching on hypotheses using ``match goal`` with inside the tactic. @@ -3862,7 +3863,7 @@ some incompatibilities. ``Empty_set``, ``unit``, ``True``, :tacn:`dintuition` also recognizes all inductive types with one constructor and no indices, i.e. record-style connectives. -.. opt:: Intuition Negation Unfolding +.. flag:: Intuition Negation Unfolding Controls whether :tacn:`intuition` unfolds inner negations which do not need to be unfolded. This option is on by default. @@ -3891,6 +3892,7 @@ usual logical connectives but instead may reason about any first-order class inductive definition. .. opt:: Firstorder Solver @tactic + :name: Firstorder Solver The default tactic used by :tacn:`firstorder` when no rule applies is :g:`auto with *`, it can be reset locally or globally using this option. @@ -3919,6 +3921,7 @@ inductive definition. This combines the effects of the different variants of :tacn:`firstorder`. .. opt:: Firstorder Depth @num + :name: Firstorder Depth This option controls the proof-search depth bound. @@ -3981,7 +3984,7 @@ match against it. additional arguments can be given to congruence by filling in the holes in the terms given in the error message, using the :tacn:`congruence with` variant described above. -.. opt:: Congruence Verbose +.. flag:: Congruence Verbose This option makes :tacn:`congruence` print debug information. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 584193b9c6..837d3f10a2 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _vernacularcommands: Vernacular commands @@ -78,145 +75,106 @@ Displaying Flags, Options and Tables ----------------------------- -|Coq| configurability is based on flags (e.g. :opt:`Printing All`), options -(e.g. :opt:`Printing Width`), or tables (e.g. :cmd:`Add Printing Record`). The -names of flags, options and tables are made of non-empty sequences of -identifiers (conventionally with capital initial letter). The general commands -handling flags, options and tables are given below. - -.. TODO : flag is not a syntax entry - -.. cmd:: Set @flag - - This command switches :n:`@flag` on. The original state of :n:`@flag` - is restored when the current module ends. - - .. cmdv:: Local Set @flag - - This command switches :n:`@flag` on. The original state - of :n:`@flag` is restored when the current *section* ends. - - .. cmdv:: Global Set @flag - - This command switches :n:`@flag` on. The original state - of :n:`@flag` is *not* restored at the end of the module. Additionally, if - set in a file, :n:`@flag` is switched on when the file is `Require`-d. +Coq has many settings to control its behavior. Setting types include flags, options +and tables: - .. cmdv:: Export Set @flag +* A :production:`flag` has a boolean value, such as :flag:`Asymmetric Patterns`. +* An :production:`option` generally has a numeric or string value, such as :opt:`Firstorder Depth`. +* A :production:`table` contains a set of strings or qualids. +* In addition, some commands provide settings, such as :cmd:`Extraction Language OCaml`. - This command switches :n:`@flag` on. The original state - of :n:`@flag` is restored at the end of the current module, but :n:`@flag` - is switched on when this module is imported. +.. FIXME Convert `Extraction Language OCaml` to an option. +Flags, options and tables are identified by a series of identifiers, each with an initial +capital letter. -.. cmd:: Unset @flag +.. cmd:: {? Local | Global | Export } Set @flag + :name: Set - This command switches :n:`@flag` off. The original state of - :n:`@flag` is restored when the current module ends. + Sets :token:`flag` on. Scoping qualifiers are + described :ref:`here <set_unset_scope_qualifiers>`. - .. cmdv:: Local Unset @flag - - This command switches :n:`@flag` off. The original - state of :n:`@flag` is restored when the current *section* ends. - - .. cmdv:: Global Unset @flag - - This command switches :n:`@flag` off. The original - state of :n:`@flag` is *not* restored at the end of the module. Additionally, - if set in a file, :n:`@flag` is switched off when the file is `Require`-d. - - .. cmdv:: Export Unset @flag - - This command switches :n:`@flag` off. The original state - of :n:`@flag` is restored at the end of the current module, but :n:`@flag` - is switched off when this module is imported. +.. cmd:: {? Local | Global | Export } Unset @flag + :name: Unset + Sets :token:`flag` off. Scoping qualifiers are + described :ref:`here <set_unset_scope_qualifiers>`. .. cmd:: Test @flag - This command prints whether :n:`@flag` is on or off. - - -.. cmd:: Set @option @value + Prints the current value of :token:`flag`. - This command sets :n:`@option` to :n:`@value`. The original value of ` option` is - restored when the current module ends. - .. TODO : option and value are not syntax entries +.. cmd:: {? Local | Global | Export } Set @option ( @num | @string ) + :name: Set @option - .. cmdv:: Local Set @option @value + Sets :token:`option` to the specified value. Scoping qualifiers are + described :ref:`here <set_unset_scope_qualifiers>`. - This command sets :n:`@option` to :n:`@value`. The - original value of :n:`@option` is restored at the end of the module. +.. cmd:: {? Local | Global | Export } Unset @option + :name: Unset @option - .. cmdv:: Global Set @option @value + Sets :token:`option` to its default value. Scoping qualifiers are + described :ref:`here <set_unset_scope_qualifiers>`. - This command sets :n:`@option` to :n:`@value`. The - original value of :n:`@option` is *not* restored at the end of the module. - Additionally, if set in a file, :n:`@option` is set to value when the file - is `Require`-d. - - .. cmdv:: Export Set @option - - This command set :n:`@option` to :n:`@value`. The original state - of :n:`@option` is restored at the end of the current module, but :n:`@option` - is set to :n:`@value` when this module is imported. - - -.. cmd:: Unset @option - - This command turns off :n:`@option`. - - .. cmdv:: Local Unset @option +.. cmd:: Test @option - This command turns off :n:`@option`. The original state of :n:`@option` - is restored when the current *section* ends. + Prints the current value of :token:`option`. - .. cmdv:: Global Unset @option +.. cmd:: Print Options - This command turns off :n:`@option`. The original state of :n:`@option` - is *not* restored at the end of the module. Additionally, if unset in a file, - :n:`@option` is reset to its default value when the file is `Require`-d. + Prints the current value of all flags and options, and the names of all tables. - .. cmdv:: Export Unset @option - This command turns off :n:`@option`. The original state of :n:`@option` - is restored at the end of the current module, but :n:`@option` is set to - its default value when this module is imported. +.. cmd:: Add @table ( @string | @qualid ) + :name: Add @table + Adds the specified value to :token:`table`. -.. cmd:: Test @option +.. cmd:: Remove @table ( @string | @qualid ) + :name: Remove @table - This command prints the current value of :n:`@option`. + Removes the specified value from :token:`table`. +.. cmd:: Test @table for ( @string | @qualid ) + :name: Test @table for -.. TODO : table is not a syntax entry + Reports whether :token:`table` contains the specified value. -.. cmd:: Add @table @value - :name: Add `table` `value` +.. cmd:: Print Table @table + :name: Print Table @table -.. cmd:: Remove @table @value - :name: Remove `table` `value` + Prints the values in :token:`table`. -.. cmd:: Test @table @value - :name: Test `table` `value` +.. cmd:: Test @table -.. cmd:: Test @table for @value - :name: Test `table` for `value` + A synonym for :cmd:`Print Table @table`. -.. cmd:: Print Table @table +.. cmd:: Print Tables -These are general commands for tables. + A synonym for :cmd:`Print Options`. +.. _set_unset_scope_qualifiers: -.. cmd:: Print Options +Scope qualifiers for :cmd:`Set` and :cmd:`Unset` +````````````````````````````````````````````````` - This command lists all available flags, options and tables. +:n:`{? Local | Global | Export }` - .. cmdv:: Print Tables +Flag and option settings can be global in scope or local to nested scopes created by +:cmd:`Module` and :cmd:`Section` commands. There are four alternatives: - This is a synonymous of :cmd:`Print Options`. +* no qualifier: the original setting is *not* restored at the end of the current module or section. +* **Local**: the setting is applied within the current scope. The original value of the option + or flag is restored at the end of the current module or section. +* **Global**: similar to no qualifier, the original setting is *not* restored at the end of the current + module or section. In addition, if the value is set in a file, then :cmd:`Require`-ing + the file sets the option. +* **Export**: similar to **Local**, the original value of the option or flag is restored at the + end of the current module or section. In addition, if the value is set in a file, then :cmd:`Import`-ing + the file sets the option. +Newly opened scopes inherit the current settings. .. _requests-to-the-environment: @@ -502,19 +460,16 @@ Requests to the environment .. note:: - .. cmd:: Add Search Blacklist @string + .. table:: Search Blacklist @string - For the ``Search``, ``SearchHead``, ``SearchPattern`` and ``SearchRewrite`` - queries, it is possible to globally filter the search results using this - command. A lemma whose fully-qualified name - contains any of the declared strings will be removed from the - search results. The default blacklisted substrings are ``_subproof`` and + Specifies a set of strings used to exclude lemmas from the results of :cmd:`Search`, + :cmd:`SearchHead`, :cmd:`SearchPattern` and :cmd:`SearchRewrite` queries. A lemma whose + fully-qualified name contains any of the strings will be excluded from the + search results. The default blacklisted substrings are ``_subterm``, ``_subproof`` and ``Private_``. - .. cmd:: Remove Search Blacklist @string - - This command allows expunging this blacklist. - + Use the :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of + blacklisted strings. .. cmd:: Locate @qualid @@ -979,6 +934,7 @@ Quitting and debugging displayed. .. opt:: Default Timeout @num + :name: Default Timeout This option controls a default timeout for subsequent commands, as if they were passed to a :cmd:`Timeout` command. Commands already starting by a @@ -1003,11 +959,12 @@ Quitting and debugging Controlling display ----------------------- -.. opt:: Silent +.. flag:: Silent This option controls the normal displaying. .. opt:: Warnings "{+, {? %( - %| + %) } @ident }" + :name: Warnings This option configures the display of warnings. It is experimental, and expects, between quotes, a comma-separated list of warning names or @@ -1017,7 +974,7 @@ Controlling display interpreted from left to right, so in case of an overlap, the flags on the right have higher priority, meaning that `A,-A` is equivalent to `-A`. -.. opt:: Search Output Name Only +.. flag:: Search Output Name Only This option restricts the output of search commands to identifier names; turning it on causes invocations of :cmd:`Search`, :cmd:`SearchHead`, @@ -1038,7 +995,7 @@ Controlling display printing. Beyond this depth, display of subterms is replaced by dots. At the time of writing this documentation, the default value is 50. -.. opt:: Printing Compact Contexts +.. flag:: Printing Compact Contexts This option controls the compact display mode for goals contexts. When on, the printer tries to reduce the vertical size of goals contexts by putting @@ -1046,13 +1003,13 @@ Controlling display does not exceed the printing width (see :opt:`Printing Width`). At the time of writing this documentation, it is off by default. -.. opt:: Printing Unfocused +.. flag:: Printing Unfocused This option controls whether unfocused goals are displayed. Such goals are created by focusing other goals with bullets (see :ref:`bullets` or :ref:`curly braces <curly-braces>`). It is off by default. -.. opt:: Printing Dependent Evars Line +.. flag:: Printing Dependent Evars Line This option controls the printing of the “(dependent evars: …)” line when ``-emacs`` is passed. diff --git a/doc/sphinx/replaces.rst b/doc/sphinx/refman-preamble.rst index 28a04f90ce..c662028773 100644 --- a/doc/sphinx/replaces.rst +++ b/doc/sphinx/refman-preamble.rst @@ -1,4 +1,13 @@ -.. some handy replacements for common items +.. This file is automatically prepended to all other files using the ``rst_prolog`` option. + +.. only:: html + + .. This is included once per page in the HTML build, and a single time (in the + document's preamble) in the LaTeX one. + + .. preamble:: /refman-preamble.sty + +.. Some handy replacements for common items .. role:: smallcaps @@ -21,7 +30,7 @@ .. |class_2| replace:: `class`\ :math:`_{2}` .. |Coq| replace:: :smallcaps:`Coq` .. |CoqIDE| replace:: :smallcaps:`CoqIDE` -.. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{\small{\beta\delta\iota\zeta}}` +.. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{\beta\delta\iota\zeta}` .. |Gallina| replace:: :smallcaps:`Gallina` .. |ident_0| replace:: `ident`\ :math:`_{0}` .. |ident_1,1| replace:: `ident`\ :math:`_{1,1}` diff --git a/doc/sphinx/refman-preamble.sty b/doc/sphinx/refman-preamble.sty new file mode 100644 index 0000000000..b4fc608e47 --- /dev/null +++ b/doc/sphinx/refman-preamble.sty @@ -0,0 +1,88 @@ +\newcommand{\alors}{\textsf{then}} +\newcommand{\alter}{\textsf{alter}} +\newcommand{\as}{\kw{as}} +\newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} +\newcommand{\bool}{\textsf{bool}} +\newcommand{\case}{\kw{case}} +\newcommand{\conc}{\textsf{conc}} +\newcommand{\cons}{\textsf{cons}} +\newcommand{\consf}{\textsf{consf}} +\newcommand{\conshl}{\textsf{cons\_hl}} +\newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} +\newcommand{\emptyf}{\textsf{emptyf}} +\newcommand{\End}{\kw{End}} +\newcommand{\kwend}{\kw{end}} +\newcommand{\EqSt}{\textsf{EqSt}} +\newcommand{\even}{\textsf{even}} +\newcommand{\evenO}{\textsf{even}_\textsf{O}} +\newcommand{\evenS}{\textsf{even}_\textsf{S}} +\newcommand{\false}{\textsf{false}} +\newcommand{\filter}{\textsf{filter}} +\newcommand{\Fix}{\kw{Fix}} +\newcommand{\fix}{\kw{fix}} +\newcommand{\for}{\textsf{for}} +\newcommand{\forest}{\textsf{forest}} +\newcommand{\from}{\textsf{from}} +\newcommand{\Functor}{\kw{Functor}} +\newcommand{\haslength}{\textsf{has\_length}} +\newcommand{\hd}{\textsf{hd}} +\newcommand{\ident}{\textsf{ident}} +\newcommand{\In}{\kw{in}} +\newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} +\newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} +\newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} +\newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} +\newcommand{\injective}{\kw{injective}} +\newcommand{\kw}[1]{\textsf{#1}} +\newcommand{\lb}{\lambda} +\newcommand{\length}{\textsf{length}} +\newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} +\newcommand{\List}{\textsf{list}} +\newcommand{\lra}{\longrightarrow} +\newcommand{\Match}{\kw{match}} +\newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} +\newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} +\newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} +\newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} +\newcommand{\mto}{.\;} +\newcommand{\Nat}{\mathbb{N}} +\newcommand{\nat}{\textsf{nat}} +\newcommand{\Nil}{\textsf{nil}} +\newcommand{\nilhl}{\textsf{nil\_hl}} +\newcommand{\nO}{\textsf{O}} +\newcommand{\node}{\textsf{node}} +\newcommand{\nS}{\textsf{S}} +\newcommand{\odd}{\textsf{odd}} +\newcommand{\oddS}{\textsf{odd}_\textsf{S}} +\newcommand{\ovl}[1]{\overline{#1}} +\newcommand{\Pair}{\textsf{pair}} +\newcommand{\Prod}{\textsf{prod}} +\newcommand{\Prop}{\textsf{Prop}} +\newcommand{\return}{\kw{return}} +\newcommand{\Set}{\textsf{Set}} +\newcommand{\si}{\textsf{if}} +\newcommand{\sinon}{\textsf{else}} +\newcommand{\Sort}{\cal S} +\newcommand{\Str}{\textsf{Stream}} +\newcommand{\Struct}{\kw{Struct}} +\newcommand{\subst}[3]{#1\{#2/#3\}} +\newcommand{\tl}{\textsf{tl}} +\newcommand{\tree}{\textsf{tree}} +\newcommand{\true}{\textsf{true}} +\newcommand{\Type}{\textsf{Type}} +\newcommand{\unfold}{\textsf{unfold}} +\newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} +\newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} +\newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]} +\newcommand{\WFE}[1]{\WF{E}{#1}} +\newcommand{\WFT}[2]{#1[] \vdash {\cal W\!F}(#2)} +\newcommand{\WFTWOLINES}[2]{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} +\newcommand{\with}{\kw{with}} +\newcommand{\WS}[3]{#1[] \vdash #2 <: #3} +\newcommand{\WSE}[2]{\WS{E}{#1}{#2}} +\newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} +\newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} +\newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} +\newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} +\newcommand{\zeroone}[1]{[{#1}]} +\newcommand{\zeros}{\textsf{zeros}} diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index ab1edc0b27..59cad3bea2 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -103,26 +103,23 @@ induction for objects in type `identᵢ`. Automatic declaration of schemes ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Elimination Schemes +.. flag:: Elimination Schemes - It is possible to deactivate the automatic declaration of the - induction principles when defining a new inductive type with the - ``Unset Elimination Schemes`` command. It may be reactivated at any time with - ``Set Elimination Schemes``. + Enables automatic declaration of induction principles when defining a new + inductive type. Defaults to on. -.. opt:: Nonrecursive Elimination Schemes +.. flag:: Nonrecursive Elimination Schemes - This option controls whether types declared with the keywords :cmd:`Variant` and - :cmd:`Record` get an automatic declaration of the induction principles. + Enables automatic declaration of induction principles for types declared with the :cmd:`Variant` and + :cmd:`Record` commands. Defaults to off. -.. opt:: Case Analysis Schemes +.. flag:: Case Analysis Schemes This flag governs the generation of case analysis lemmas for inductive types, - i.e. corresponding to the pattern-matching term alone and without fixpoint. + i.e. corresponding to the pattern matching term alone and without fixpoint. -.. opt:: Boolean Equality Schemes - -.. opt:: Decidable Equality Schemes +.. flag:: Boolean Equality Schemes + Decidable Equality Schemes These flags control the automatic declaration of those Boolean equalities (see the second variant of ``Scheme``). @@ -132,7 +129,7 @@ Automatic declaration of schemes You have to be careful with this option since Coq may now reject well-defined inductive types because it cannot compute a Boolean equality for them. -.. opt:: Rewriting Schemes +.. flag:: Rewriting Schemes This flag governs generation of equality-related schemes such as congruence. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 4c0e85bdd4..705d67e6c6 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _syntaxextensionsandinterpretationscopes: Syntax extensions and interpretation scopes @@ -378,17 +376,14 @@ for records. Here are examples: Displaying information about notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Printing Notations - - To deactivate the printing of all notations, use the command - ``Unset Printing Notations``. To reactivate it, use the command - ``Set Printing Notations``. +.. flag:: Printing Notations - The default is to use notations for printing terms wherever possible. + Controls whether to use notations for printing terms wherever possible. + Default is on. .. seealso:: - :opt:`Printing All` + :flag:`Printing All` To disable other elements in addition to notations. .. _locating-notations: diff --git a/doc/sphinx/zebibliography.html.rst b/doc/sphinx/zebibliography.html.rst new file mode 100644 index 0000000000..756edd5482 --- /dev/null +++ b/doc/sphinx/zebibliography.html.rst @@ -0,0 +1,17 @@ +.. There are multiple issues with sphinxcontrib-bibtex that we have to work around: + - The list of cited entries is computed right after encountering + `.. bibliography`, so the file containing that command has to come last + alphabetically: + https://sphinxcontrib-bibtex.readthedocs.io/en/latest/usage.html#unresolved-citations-across-documents + - `.. bibliography::` puts the bibliography on its own page with its own + title in LaTeX, but includes it inline without a title in HTML: + https://sphinxcontrib-bibtex.readthedocs.io/en/latest/usage.html#mismatch-between-output-of-html-and-latex-backends + +.. _bibliography: + +============== + Bibliography +============== + +.. bibliography:: biblio.bib + :cited: diff --git a/doc/sphinx/zebibliography.rst b/doc/sphinx/zebibliography.latex.rst index 0000caa301..2c0396f1c9 100644 --- a/doc/sphinx/zebibliography.rst +++ b/doc/sphinx/zebibliography.latex.rst @@ -1,8 +1,6 @@ -.. _bibliography: +.. See zebibliography.html.rst for details -============ -Bibliography -============ +.. _bibliography: .. bibliography:: biblio.bib :cited: diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 40554c3ca3..7992c10abb 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -34,7 +34,7 @@ from sphinx.util.logging import getLogger from sphinx.directives import ObjectDescription from sphinx.domains import Domain, ObjType, Index from sphinx.domains.std import token_xrefs -from sphinx.ext.mathbase import MathDirective, displaymath +from sphinx.ext import mathbase from . import coqdoc from .repl import ansicolors @@ -58,6 +58,15 @@ def make_target(objtype, targetid): """Create a target to an object of type objtype and id targetid""" return "coq:{}.{}".format(objtype, targetid) +def make_math_node(latex, docname, nowrap): + node = mathbase.displaymath() + node['latex'] = latex + node['label'] = None # Otherwise equations are numbered + node['nowrap'] = nowrap + node['docname'] = docname + node['number'] = None + return node + class CoqObject(ObjectDescription): """A generic Coq object for Sphinx; all Coq objects are subclasses of this. @@ -101,7 +110,9 @@ class CoqObject(ObjectDescription): # Explicit object naming 'name': directives.unchanged, # Silence warnings produced by report_undocumented_coq_objects - 'undocumented': directives.flag + 'undocumented': directives.flag, + # noindex omits this object from its index + 'noindex': directives.flag } def subdomain_data(self): @@ -138,6 +149,13 @@ class CoqObject(ObjectDescription): msg = MSG.format(name, self.env.doc2path(objects[name][0])) self.state_machine.reporter.warning(msg, line=self.lineno) + def _warn_if_duplicate_name(self, objects, name): + """Check that two objects in the same domain don't have the same name.""" + if name in objects: + MSG = 'Duplicate object: {}; other is at {}' + msg = MSG.format(name, self.env.doc2path(objects[name][0])) + self.state_machine.reporter.warning(msg, line=self.lineno) + def _record_name(self, name, target_id): """Record a name, mapping it to target_id @@ -165,13 +183,16 @@ class CoqObject(ObjectDescription): """Add `name` (pointing to `target`) to the main index.""" assert isinstance(name, str) if not name.startswith("_"): - index_text = name + # 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)) def add_target_and_index(self, name, _, signode): - """Attach a link target to `signode` and an index entry for `name`.""" + """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: target = self._add_target(signode, name) self._add_index_entry(name, target) @@ -316,11 +337,10 @@ class OptionObject(NotationObject): Example:: - .. opt:: Nonrecursive Elimination Schemes + .. opt:: Hyps Limit @num - This option controls whether types declared with the keywords - :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the - induction principles. + This option controls the maximum number of hypotheses displayed in goals after + the application of a tactic. """ subdomain = "opt" index_suffix = "(opt)" @@ -329,6 +349,42 @@ class OptionObject(NotationObject): def _name_from_signature(self, signature): return stringify_with_ellipses(signature) + +class FlagObject(NotationObject): + """A Coq flag, i.e. a boolean Option. + + Example:: + + .. flag:: Nonrecursive Elimination Schemes + + This flag controls whether types declared with the keywords + :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the + induction principles. + """ + subdomain = "flag" + index_suffix = "(flag)" + annotation = "Flag" + + def _name_from_signature(self, signature): + return stringify_with_ellipses(signature) + + +class TableObject(NotationObject): + """A Coq table, i.e. a setting that is a set of values. + + Example:: + + .. table:: Search Blacklist + + This table controls ... + """ + subdomain = "table" + index_suffix = "(table)" + annotation = "Table" + + def _name_from_signature(self, signature): + return stringify_with_ellipses(signature) + class ProductionObject(CoqObject): r"""A grammar production. @@ -487,7 +543,7 @@ def coq_code_role(role, rawtext, text, lineno, inliner, options={}, content=[]): CoqCodeRole = coq_code_role class CoqtopDirective(Directive): - """A reST directive to describe interactions with Coqtop. + r"""A reST directive to describe interactions with Coqtop. Usage:: @@ -525,16 +581,17 @@ class CoqtopDirective(Directive): required_arguments = 0 optional_arguments = 1 final_argument_whitespace = True + option_spec = { 'name': directives.unchanged } directive_name = "coqtop" def run(self): # Uses a ‘container’ instead of a ‘literal_block’ to disable # Pygments-based post-processing (we could also set rawsource to '') content = '\n'.join(self.content) - options = self.arguments[0].split() if self.arguments else ['in'] - if 'all' in options: - options.extend(['in', 'out']) - node = nodes.container(content, coqtop_options = list(set(options)), + args = self.arguments[0].split() if self.arguments else ['in'] + if 'all' in args: + args.extend(['in', 'out']) + node = nodes.container(content, coqtop_options = list(set(args)), classes=['coqtop', 'literal-block']) self.add_name(node) return [node] @@ -559,6 +616,7 @@ class CoqdocDirective(Directive): required_arguments = 0 optional_arguments = 0 final_argument_whitespace = True + option_spec = { 'name': directives.unchanged } directive_name = "coqdoc" def run(self): @@ -567,6 +625,7 @@ class CoqdocDirective(Directive): content = '\n'.join(self.content) node = nodes.inline(content, '', *highlight_using_coqdoc(content)) wrapper = nodes.container(content, node, classes=['coqdoc', 'literal-block']) + self.add_name(wrapper) return [wrapper] class ExampleDirective(BaseAdmonition): @@ -602,24 +661,39 @@ class ExampleDirective(BaseAdmonition): self.options['classes'] = ['admonition', 'note'] return super().run() -class PreambleDirective(MathDirective): - r"""A reST directive for hidden math. +class PreambleDirective(Directive): + r"""A reST directive to include a TeX file. - Mostly useful to let MathJax know about `\def`\ s and `\newcommand`\ s. + Mostly useful to let MathJax know about `\def`s and `\newcommand`s. - Example:: - - .. preamble:: + Usage:: - \newcommand{\paren}[#1]{\left(#1\right)} + .. preamble:: preamble.tex """ - + has_content = False + required_arguments = 1 + optional_arguments = 0 + final_argument_whitespace = True + option_spec = {} directive_name = "preamble" def run(self): - self.options['nowrap'] = True - [node] = super().run() + document = self.state.document + env = document.settings.env + + if not document.settings.file_insertion_enabled: + msg = 'File insertion disabled' + return [document.reporter.warning(msg, line=self.lineno)] + + rel_fname, abs_fname = env.relfn2path(self.arguments[0]) + env.note_dependency(rel_fname) + + with open(abs_fname, encoding="utf-8") as ltx: + latex = ltx.read() + + node = make_math_node(latex, env.docname, nowrap=True) node['classes'] = ["math-preamble"] + set_source_info(self, node) return [node] class InferenceDirective(Directive): @@ -632,8 +706,8 @@ class InferenceDirective(Directive): .. inference:: name - newline-separated premisses - ------------------------ + newline-separated premises + -------------------------- conclusion Example:: @@ -652,15 +726,6 @@ class InferenceDirective(Directive): final_argument_whitespace = True directive_name = "inference" - def make_math_node(self, latex): - node = displaymath() - node['latex'] = latex - node['label'] = None # Otherwise equations are numbered - node['nowrap'] = False - node['docname'] = self.state.document.settings.env.docname - node['number'] = None - return node - @staticmethod def prepare_latex_operand(op): # TODO: Could use a fancier inference class in LaTeX @@ -680,7 +745,8 @@ class InferenceDirective(Directive): title = self.arguments[0] content = '\n'.join(self.content) latex = self.prepare_latex(content) - math_node = self.make_math_node(latex) + docname = self.state.document.settings.env.docname + math_node = make_math_node(latex, docname, nowrap=False) tid = nodes.make_id(title) target = nodes.target('', '', ids=['inference-' + tid]) @@ -827,23 +893,28 @@ class CoqtopBlocksTransform(Transform): kept_node['classes'] = [c for c in kept_node['classes'] if c != 'coqtop-hidden'] - def merge_consecutive_coqtop_blocks(self): + @staticmethod + def merge_consecutive_coqtop_blocks(app, doctree, _): """Merge consecutive divs wrapping lists of Coq sentences; keep ‘dl’s separate.""" - for node in self.document.traverse(CoqtopBlocksTransform.is_coqtop_block): + for node in doctree.traverse(CoqtopBlocksTransform.is_coqtop_block): if node.parent: + rawsources, names = [node.rawsource], set(node['names']) for sibling in node.traverse(include_self=False, descend=False, siblings=True, ascend=False): if CoqtopBlocksTransform.is_coqtop_block(sibling): - self.merge_coqtop_classes(node, sibling) + CoqtopBlocksTransform.merge_coqtop_classes(node, sibling) + rawsources.append(sibling.rawsource) + names.update(sibling['names']) node.extend(sibling.children) node.parent.remove(sibling) sibling.parent = None else: break + node.rawsource = "\n\n".join(rawsources) + node['names'] = list(names) def apply(self): self.add_coqtop_output() - self.merge_consecutive_coqtop_blocks() class CoqSubdomainsIndex(Index): """Index subclass to provide subdomain-specific indices. @@ -876,7 +947,7 @@ class CoqTacticIndex(CoqSubdomainsIndex): name, localname, shortname, subdomains = "tacindex", "Tactic Index", "tactics", ["tacn"] class CoqOptionIndex(CoqSubdomainsIndex): - name, localname, shortname, subdomains = "optindex", "Option Index", "options", ["opt"] + name, localname, shortname, subdomains = "optindex", "Flags, options and Tables Index", "options", ["flag", "opt", "table"] class CoqGallinaIndex(CoqSubdomainsIndex): name, localname, shortname, subdomains = "thmindex", "Gallina Index", "theorems", ["thm"] @@ -949,6 +1020,8 @@ class CoqDomain(Domain): 'tacn': ObjType('tacn', 'tacn'), 'tacv': ObjType('tacv', 'tacn'), 'opt': ObjType('opt', 'opt'), + 'flag': ObjType('flag', 'flag'), + 'table': ObjType('table', 'table'), 'thm': ObjType('thm', 'thm'), 'prodn': ObjType('prodn', 'prodn'), 'exn': ObjType('exn', 'exn'), @@ -965,6 +1038,8 @@ class CoqDomain(Domain): 'tacn': TacticNotationObject, 'tacv': TacticNotationVariantObject, 'opt': OptionObject, + 'flag': FlagObject, + 'table': TableObject, 'thm': GallinaObject, 'prodn' : ProductionObject, 'exn': ExceptionObject, @@ -976,6 +1051,8 @@ class CoqDomain(Domain): 'cmd': XRefRole(warn_dangling=True), 'tacn': XRefRole(warn_dangling=True), 'opt': XRefRole(warn_dangling=True), + 'flag': XRefRole(warn_dangling=True), + 'table': XRefRole(warn_dangling=True), 'thm': XRefRole(warn_dangling=True), 'prodn' : XRefRole(warn_dangling=True), 'exn': XRefRole(warn_dangling=True), @@ -997,6 +1074,8 @@ class CoqDomain(Domain): 'cmd': {}, 'tacn': {}, 'opt': {}, + 'flag': {}, + 'table': {}, 'thm': {}, 'prodn' : {}, 'exn': {}, @@ -1059,7 +1138,6 @@ def simplify_source_code_blocks_for_latex(app, doctree, fromdocname): # pylint: pygments if available. This prevents the LaTeX builder from getting confused. """ - is_html = app.builder.tags.has("html") for node in doctree.traverse(is_coqtop_or_coqdoc_block): if is_html: @@ -1096,6 +1174,7 @@ def setup(app): app.add_transform(CoqtopBlocksTransform) app.connect('doctree-resolved', simplify_source_code_blocks_for_latex) + app.connect('doctree-resolved', CoqtopBlocksTransform.merge_consecutive_coqtop_blocks) # Add extra styles app.add_stylesheet("fonts.css") @@ -1108,4 +1187,11 @@ def setup(app): # Tell Sphinx about extra settings app.add_config_value("report_undocumented_coq_objects", None, 'env') - return {'version': '0.1', "parallel_read_safe": True} + # ``env_version`` is used by Sphinx to know when to invalidate + # coqdomain-specific bits in its caches. It should be incremented when the + # contents of ``env.domaindata['coq']`` change. See + # `https://github.com/sphinx-doc/sphinx/issues/4460`. + meta = { "version": "0.1", + "env_version": 1, + "parallel_read_safe": True } + return meta diff --git a/ide/coqide.opam b/ide/coqide.opam index 1b46efdee2..ba05b9edcf 100644 --- a/ide/coqide.opam +++ b/ide/coqide.opam @@ -16,4 +16,4 @@ depends: [ "coq" ] -build: [ [ "dune" "build" "-p" package "-j" jobs ] ] +build: [ [ "dune" "build" "-p" name "-j" jobs ] ] diff --git a/interp/declare.ml b/interp/declare.ml index a82e6b35a6..22e6cf9d1c 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -39,7 +39,6 @@ type constant_obj = { cst_decl : global_declaration option; (** [None] when the declaration is a side-effect and has already been defined in the global environment. *) - cst_hyps : Dischargedhypsmap.discharged_hyps; cst_kind : logical_kind; cst_locl : bool; } @@ -94,28 +93,20 @@ let cache_constant ((sp,kn), obj) = Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn)); let cst = Global.lookup_constant kn' in add_section_constant (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps; - Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps; add_constant_kind (Constant.make1 kn) obj.cst_kind -let discharged_hyps kn sechyps = - let (_,dir,_) = KerName.repr kn in - let args = Array.to_list (instance_from_variable_context sechyps) in - List.rev_map (Libnames.make_path dir) args - let discharge_constant ((sp, kn), obj) = let con = Constant.make1 kn in let from = Global.lookup_constant con in let modlist = replacement_context () in let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = section_segment_of_constant con in - let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in let abstract = (named_of_variable_context hyps, subst, uctx) in let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in - Some { obj with cst_hyps = new_hyps; cst_decl = Some new_decl; } + Some { obj with cst_decl = Some new_decl; } (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant cst = { cst_decl = None; - cst_hyps = []; cst_kind = cst.cst_kind; cst_locl = cst.cst_locl; } @@ -142,7 +133,6 @@ let update_tables c = let register_side_effect (c, role) = let o = inConstant { cst_decl = None; - cst_hyps = [] ; cst_kind = IsProof Theorem; cst_locl = false; } in @@ -194,7 +184,6 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e let () = List.iter register_side_effect export in let cst = { cst_decl = Some decl; - cst_hyps = [] ; cst_kind = kind; cst_locl = local; } in @@ -255,7 +244,6 @@ let cache_variable ((sp,_),o) = poly, univs in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); add_section_variable id impl poly ctx; - Dischargedhypsmap.set_discharged_hyps sp []; add_variable_data id (p,opaq,ctx,poly,mk) let discharge_variable (_,o) = match o with @@ -311,15 +299,15 @@ let inductive_names sp kn mie = ([], 0) mie.mind_entry_inds in names -let load_inductive i ((sp,kn),(_,mie)) = +let load_inductive i ((sp,kn),mie) = let names = inductive_names sp kn mie in List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names -let open_inductive i ((sp,kn),(_,mie)) = +let open_inductive i ((sp,kn),mie) = let names = inductive_names sp kn mie in List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names -let cache_inductive ((sp,kn),(dhyps,mie)) = +let cache_inductive ((sp,kn),mie) = let names = inductive_names sp kn mie in List.iter check_exists (List.map fst names); let id = basename sp in @@ -328,17 +316,14 @@ let cache_inductive ((sp,kn),(dhyps,mie)) = assert (MutInd.equal kn' (MutInd.make1 kn)); let mind = Global.lookup_mind kn' in add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps; - Dischargedhypsmap.set_discharged_hyps sp dhyps; List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names -let discharge_inductive ((sp,kn),(dhyps,mie)) = +let discharge_inductive ((sp,kn),mie) = let mind = Global.mind_of_delta_kn kn in let mie = Global.lookup_mind mind in let repl = replacement_context () in let info = section_segment_of_mutual_inductive mind in - let sechyps = info.Lib.abstr_ctx in - Some (discharged_hyps kn sechyps, - Discharge.process_inductive info repl mie) + Some (Discharge.process_inductive info repl mie) let dummy_one_inductive_entry mie = { mind_entry_typename = mie.mind_entry_typename; @@ -349,30 +334,28 @@ let dummy_one_inductive_entry mie = { } (* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_inductive_entry (_,m) = ([],{ +let dummy_inductive_entry m = { mind_entry_params = []; mind_entry_record = None; mind_entry_finite = Declarations.BiFinite; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; mind_entry_universes = Monomorphic_ind_entry Univ.ContextSet.empty; mind_entry_private = None; -}) +} (* reinfer subtyping constraints for inductive after section is dischared. *) -let infer_inductive_subtyping (pth, mind_ent) = +let infer_inductive_subtyping mind_ent = match mind_ent.mind_entry_universes with | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ -> - (pth, mind_ent) + mind_ent | Cumulative_ind_entry cumi -> begin let env = Global.env () in (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *) - (pth, InferCumulativity.infer_inductive env mind_ent) + InferCumulativity.infer_inductive env mind_ent end -type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry - -let inInductive : inductive_obj -> obj = +let inInductive : mutual_inductive_entry -> obj = declare_object {(default_object "INDUCTIVE") with cache_function = cache_inductive; load_function = load_inductive; @@ -426,7 +409,7 @@ let declare_mind mie = let id = match mie.mind_entry_inds with | ind::_ -> ind.mind_entry_typename | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in - let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in + let (sp,kn as oname) = add_leaf id (inInductive mie) in let mind = Global.mind_of_delta_kn kn in let isprim = declare_projections mie.mind_entry_universes mind in declare_mib_implicits mind; diff --git a/kernel/clambda.ml b/kernel/clambda.ml index ff977416df..31dede6f5d 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -661,11 +661,11 @@ let rec lambda_of_constr env c = (* translation of the argument *) let la = lambda_of_constr env a in - let entry = mkInd ind in + let gr = GlobRef.IndRef ind in let la = try Retroknowledge.get_vm_before_match_info env.global_env.retroknowledge - entry la + gr la with Not_found -> la in (* translation of the type *) @@ -723,7 +723,7 @@ and lambda_of_app env f args = (try (* We delay the compilation of arguments to avoid an exponential behavior *) let f = Retroknowledge.get_vm_compiling_info env.global_env.retroknowledge - (mkConstU (kn,u)) in + (GlobRef.ConstRef kn) in let args = lambda_of_args env 0 args in f args with Not_found -> @@ -736,6 +736,7 @@ and lambda_of_app env f args = | Construct (c,_) -> let tag, nparams, arity = Renv.get_construct_info env c in let nargs = Array.length args in + let gr = GlobRef.ConstructRef c in if Int.equal (nparams + arity) nargs then (* fully applied *) (* spiwack: *) (* 1/ tries to compile the constructor in an optimal way, @@ -750,7 +751,7 @@ and lambda_of_app env f args = try Retroknowledge.get_vm_constant_static_info env.global_env.retroknowledge - f args + gr args with NotClosed -> (* 2/ if the arguments are not all closed (this is expectingly (and it is currently the case) the only @@ -771,7 +772,7 @@ and lambda_of_app env f args = let args = lambda_of_args env nparams rargs in Retroknowledge.get_vm_constant_dynamic_info env.global_env.retroknowledge - f args + gr args with Not_found -> (* 3/ if no special behavior is available, then the compiler falls back to the normal behavior *) @@ -784,7 +785,7 @@ and lambda_of_app env f args = (try (Retroknowledge.get_vm_constant_dynamic_info env.global_env.retroknowledge - f) args + gr) args with Not_found -> if nparams <= nargs then (* got all parameters *) makeblock tag 0 arity args diff --git a/kernel/environ.ml b/kernel/environ.ml index e7efa5e2c9..3bfcaa7f52 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -365,8 +365,7 @@ let push_constraints_to_env (_,univs) env = let add_universes strict ctx g = let g = Array.fold_left - (* Be lenient, module typing reintroduces universes and constraints due to includes *) - (fun g v -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g) + (fun g v -> UGraph.add_universe v strict g) g (Univ.Instance.to_array (Univ.UContext.instance ctx)) in UGraph.merge_constraints (Univ.UContext.constraints ctx) g @@ -376,6 +375,7 @@ let push_context ?(strict=false) ctx env = let add_universes_set strict ctx g = let g = Univ.LSet.fold + (* Be lenient, module typing reintroduces universes and constraints due to includes *) (fun v g -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g) (Univ.ContextSet.levels ctx) g in UGraph.merge_constraints (Univ.ContextSet.constraints ctx) g @@ -693,12 +693,12 @@ let register_one env field entry = { env with retroknowledge = Retroknowledge.add_field env.retroknowledge field entry } (* [register env field entry] may register several fields when needed *) -let register env field entry = +let register env field gr = match field with - | KInt31 (grp, Int31Type) -> - let i31c = match kind entry with - | Ind i31t -> mkConstructUi (i31t, 1) - | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type.") - in - register_one (register_one env (KInt31 (grp,Int31Constructor)) i31c) field entry - | field -> register_one env field entry + | KInt31 Int31Type -> + let i31c = match gr with + | GlobRef.IndRef i31t -> GlobRef.ConstructRef (i31t, 1) + | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type.") + in + register_one (register_one env (KInt31 Int31Constructor) i31c) field gr + | field -> register_one env field gr diff --git a/kernel/environ.mli b/kernel/environ.mli index f45b7be821..1343b9029b 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -325,7 +325,7 @@ val retroknowledge : (retroknowledge->'a) -> env -> 'a val registered : env -> field -> bool -val register : env -> field -> Retroknowledge.entry -> env +val register : env -> field -> GlobRef.t -> env (** Native compiler *) val no_link_info : link_info diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index f79e5270a2..7abf8027bd 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -234,8 +234,7 @@ let check_subtyping cumi paramsctxt env_ar inds = let instance_other = Instance.of_array new_levels in let constraints_other = Univ.subst_univs_level_constraints lmap (Univ.UContext.constraints uctx) in let uctx_other = Univ.UContext.make (instance_other, constraints_other) in - let env = Environ.push_context uctx env_ar in - let env = Environ.push_context uctx_other env in + let env = Environ.push_context uctx_other env_ar in let subtyp_constraints = CumulativityInfo.leq_constraints cumi (UContext.instance uctx) instance_other diff --git a/kernel/modops.ml b/kernel/modops.ml index 98a9973117..9435f46c6b 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -267,7 +267,7 @@ let subst_structure subst = subst_structure subst do_delta_codom (* lclrk : retroknowledge_action list, rkaction : retroknowledge action *) let add_retroknowledge = let perform rkaction env = match rkaction with - | Retroknowledge.RKRegister (f, e) when (isConst e || isInd e) -> + | Retroknowledge.RKRegister (f, ((GlobRef.ConstRef _ | GlobRef.IndRef _) as e)) -> Environ.register env f e | _ -> CErrors.anomaly ~label:"Modops.add_retroknowledge" diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 122fe95df4..ab40c643f9 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -373,14 +373,14 @@ let is_lazy env prefix t = | App (f,args) -> begin match kind f with | Construct (c,_) -> - let entry = mkInd (fst c) in - (try - let _ = - Retroknowledge.get_native_before_match_info env.retroknowledge - entry prefix c Llazy; - in + let gr = GlobRef.IndRef (fst c) in + (try + let _ = + Retroknowledge.get_native_before_match_info env.retroknowledge + gr prefix c Llazy; + in false - with Not_found -> true) + with Not_found -> true) | _ -> true end | LetIn _ | Case _ | Proj _ -> true @@ -482,12 +482,12 @@ let rec lambda_of_constr cache env sigma c = in (* translation of the argument *) let la = lambda_of_constr cache env sigma a in - let entry = mkInd ind in + let gr = GlobRef.IndRef ind in let la = - try - Retroknowledge.get_native_before_match_info (env).retroknowledge - entry prefix (ind,1) la - with Not_found -> la + try + Retroknowledge.get_native_before_match_info (env).retroknowledge + gr prefix (ind,1) la + with Not_found -> la in (* translation of the type *) let lt = lambda_of_constr cache env sigma t in @@ -536,7 +536,7 @@ and lambda_of_app cache env sigma f args = let prefix = get_const_prefix env kn in (* We delay the compilation of arguments to avoid an exponential behavior *) let f = Retroknowledge.get_native_compiling_info - (env).retroknowledge (mkConst kn) prefix in + (env).retroknowledge (GlobRef.ConstRef kn) prefix in let args = lambda_of_args cache env sigma 0 args in f args with Not_found -> @@ -561,17 +561,18 @@ and lambda_of_app cache env sigma f args = let expected = nparams + arity in let nargs = Array.length args in let prefix = get_mind_prefix env (fst (fst c)) in + let gr = GlobRef.ConstructRef c in if Int.equal nargs expected then try try Retroknowledge.get_native_constant_static_info (env).retroknowledge - f args + gr args with NotClosed -> assert (Int.equal nparams 0); (* should be fine for int31 *) let args = lambda_of_args cache env sigma nparams args in Retroknowledge.get_native_constant_dynamic_info - (env).retroknowledge f prefix c args + (env).retroknowledge gr prefix c args with Not_found -> let args = lambda_of_args cache env sigma nparams args in makeblock env c u tag args @@ -579,7 +580,7 @@ and lambda_of_app cache env sigma f args = let args = lambda_of_args cache env sigma 0 args in (try Retroknowledge.get_native_constant_dynamic_info - (env).retroknowledge f prefix c args + (env).retroknowledge gr prefix c args with Not_found -> mkLapp (Lconstruct (prefix, (c,u))) args) | _ -> diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index 34f62defb8..e51c25c06b 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -19,12 +19,9 @@ open Names open Constr (* The retroknowledge defines a bijective correspondance between some - [entry]-s (which are, in fact, merely terms) and [field]-s which + [entry]-s (which are, in fact, merely names) and [field]-s which are roles assigned to these entries. *) -(* aliased type for clarity purpose*) -type entry = Constr.t - type int31_field = | Int31Bits | Int31Type @@ -53,8 +50,37 @@ type int31_field = | Int31Lxor type field = - | KInt31 of string*int31_field - + | KInt31 of int31_field + +let int31_field_of_string = + function + | "bits" -> Int31Bits + | "type" -> Int31Type + | "twice" -> Int31Twice + | "twice_plus_one" -> Int31TwicePlusOne + | "phi" -> Int31Phi + | "phi_inv" -> Int31PhiInv + | "plus" -> Int31Plus + | "plusc" -> Int31PlusC + | "pluscarryc" -> Int31PlusCarryC + | "minus" -> Int31Minus + | "minusc" -> Int31MinusC + | "minuscarryc" -> Int31MinusCarryC + | "times" -> Int31Times + | "timesc" -> Int31TimesC + | "div21" -> Int31Div21 + | "div" -> Int31Div + | "diveucl" -> Int31Diveucl + | "addmuldiv" -> Int31AddMulDiv + | "compare" -> Int31Compare + | "head0" -> Int31Head0 + | "tail0" -> Int31Tail0 + | "lor" -> Int31Lor + | "land" -> Int31Land + | "lxor" -> Int31Lxor + | s -> CErrors.user_err Pp.(str "Registering unknown int31 operator " ++ str s) + +let int31_path = DirPath.make [ Id.of_string "int31" ] (* record representing all the flags of the internal state of the kernel *) type flags = {fastcomputation : bool} @@ -68,19 +94,13 @@ type flags = {fastcomputation : bool} module Proactive = Map.Make (struct type t = field let compare = Pervasives.compare end) -type proactive = entry Proactive.t +type proactive = GlobRef.t Proactive.t (* The [reactive] knowledge contains the mapping [entry->field]. Fields are later to be interpreted as a [reactive_info]. *) -module EntryOrd = -struct - type t = entry - let compare = Constr.compare -end - -module Reactive = Map.Make (EntryOrd) +module Reactive = GlobRef.Map type reactive_info = {(*information required by the compiler of the VM *) vm_compiling : @@ -127,7 +147,7 @@ and retroknowledge = {flags : flags; proactive : proactive; reactive : reactive} (* As per now, there is only the possibility of registering things the possibility of unregistering or changing the flag is under study *) type action = - | RKRegister of field*entry + | RKRegister of field * GlobRef.t (*initialisation*) diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 02d961d893..0a2ef5300e 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -13,9 +13,6 @@ open Constr type retroknowledge -(** aliased type for clarity purpose*) -type entry = Constr.t - (** the following types correspond to the different "things" the kernel can learn about.*) type int31_field = @@ -46,14 +43,18 @@ type int31_field = | Int31Lxor type field = - | KInt31 of string*int31_field + | KInt31 of int31_field + +val int31_field_of_string : string -> int31_field + +val int31_path : DirPath.t (** This type represent an atomic action of the retroknowledge. It is stored in the compiled libraries As per now, there is only the possibility of registering things the possibility of unregistering or changing the flag is under study *) type action = - | RKRegister of field*entry + | RKRegister of field * GlobRef.t (** initial value for retroknowledge *) @@ -64,7 +65,7 @@ val initial_retroknowledge : retroknowledge and the continuation cont of the bytecode compilation returns the compilation of id in cont if it has a specific treatment or raises Not_found if id should be compiled as usual *) -val get_vm_compiling_info : retroknowledge -> entry -> +val get_vm_compiling_info : retroknowledge -> GlobRef.t -> Cinstr.lambda array -> Cinstr.lambda (*Given an identifier id (usually Construct _) and its argument array, returns a function that tries an ad-hoc optimisated @@ -73,7 +74,7 @@ val get_vm_compiling_info : retroknowledge -> entry -> raises Not_found if id should be compiled as usual, and expectingly CBytecodes.NotClosed if the term is not a closed constructor pattern (a constant for the compiler) *) -val get_vm_constant_static_info : retroknowledge -> entry -> +val get_vm_constant_static_info : retroknowledge -> GlobRef.t -> constr array -> Cinstr.lambda (*Given an identifier id (usually Construct _ ) @@ -81,45 +82,45 @@ val get_vm_constant_static_info : retroknowledge -> entry -> of id+args+cont when id has a specific treatment (in the case of 31-bit integers, that would be the dynamic compilation into integers) or raises Not_found if id should be compiled as usual *) -val get_vm_constant_dynamic_info : retroknowledge -> entry -> +val get_vm_constant_dynamic_info : retroknowledge -> GlobRef.t -> Cinstr.lambda array -> Cinstr.lambda (** Given a type identifier, this function is used before compiling a match over this type. In the case of 31-bit integers for instance, it is used to add the instruction sequence which would perform a dynamic decompilation in case the argument of the match is not in coq representation *) -val get_vm_before_match_info : retroknowledge -> entry -> Cinstr.lambda +val get_vm_before_match_info : retroknowledge -> GlobRef.t -> Cinstr.lambda -> Cinstr.lambda (** Given a type identifier, this function is used by pretyping/vnorm.ml to recover the elements of that type from their compiled form if it's non standard (it is used (and can be used) only when the compiled form is not a block *) -val get_vm_decompile_constant_info : retroknowledge -> entry -> int -> constr +val get_vm_decompile_constant_info : retroknowledge -> GlobRef.t -> int -> constr -val get_native_compiling_info : retroknowledge -> entry -> Nativeinstr.prefix -> +val get_native_compiling_info : retroknowledge -> GlobRef.t -> Nativeinstr.prefix -> Nativeinstr.lambda array -> Nativeinstr.lambda -val get_native_constant_static_info : retroknowledge -> entry -> +val get_native_constant_static_info : retroknowledge -> GlobRef.t -> constr array -> Nativeinstr.lambda -val get_native_constant_dynamic_info : retroknowledge -> entry -> +val get_native_constant_dynamic_info : retroknowledge -> GlobRef.t -> Nativeinstr.prefix -> constructor -> Nativeinstr.lambda array -> Nativeinstr.lambda -val get_native_before_match_info : retroknowledge -> entry -> +val get_native_before_match_info : retroknowledge -> GlobRef.t -> Nativeinstr.prefix -> constructor -> Nativeinstr.lambda -> Nativeinstr.lambda (** the following functions are solely used in Environ and Safe_typing to implement the functions register and unregister (and mem) of Environ *) -val add_field : retroknowledge -> field -> entry -> retroknowledge +val add_field : retroknowledge -> field -> GlobRef.t -> retroknowledge val mem : retroknowledge -> field -> bool (* val remove : retroknowledge -> field -> retroknowledge *) -val find : retroknowledge -> field -> entry +val find : retroknowledge -> field -> GlobRef.t (** Dispatching type for the above [get_*] functions. *) @@ -161,4 +162,4 @@ val empty_reactive_info : reactive_info (** Hook to be set after the compiler are installed to dispatch fields into the above [get_*] functions. *) -val dispatch_hook : (retroknowledge -> entry -> field -> reactive_info) Hook.t +val dispatch_hook : (retroknowledge -> GlobRef.t -> field -> reactive_info) Hook.t diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 6c87ff570f..9d302c69fb 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -892,8 +892,8 @@ let retroknowledge f senv = Environ.retroknowledge f (env_of_senv senv) [@@@ocaml.warning "+3"] -let register field value by_clause senv = - (* todo : value closed, by_clause safe, by_clause of the proper type*) +let register field value senv = + (* todo : value closed *) (* spiwack : updates the safe_env with the information that the register action has to be performed (again) when the environment is imported *) { senv with @@ -977,39 +977,39 @@ let dispatch = it to the name of the coq definition in the reactive retroknowledge) *) let int31_op n op prim kn = { empty_reactive_info with - vm_compiling = Some (Clambda.compile_prim n op kn); - native_compiling = Some (Nativelambda.compile_prim prim (Univ.out_punivs kn)); + vm_compiling = Some (Clambda.compile_prim n op (kn, Univ.Instance.empty)); (*XXX: FIXME universes? *) + native_compiling = Some (Nativelambda.compile_prim prim kn); } in fun rk value field -> (* subfunction which shortens the (very common) dispatch of operations *) let int31_op_from_const n op prim = - match Constr.kind value with - | Constr.Const kn -> int31_op n op prim kn + match value with + | GlobRef.ConstRef kn -> int31_op n op prim kn | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant.") in let int31_binop_from_const op prim = int31_op_from_const 2 op prim in let int31_unop_from_const op prim = int31_op_from_const 1 op prim in match field with - | KInt31 (grp, Int31Type) -> + | KInt31 Int31Type -> let int31bit = (* invariant : the type of bits is registered, otherwise the function would raise Not_found. The invariant is enforced in safe_typing.ml *) match field with - | KInt31 (grp, Int31Type) -> Retroknowledge.find rk (KInt31 (grp,Int31Bits)) + | KInt31 Int31Type -> Retroknowledge.find rk (KInt31 Int31Bits) | _ -> anomaly ~label:"Environ.register" (Pp.str "add_int31_decompilation_from_type called with an abnormal field.") in let i31bit_type = - match Constr.kind int31bit with - | Constr.Ind (i31bit_type,_) -> i31bit_type + match int31bit with + | GlobRef.IndRef i31bit_type -> i31bit_type | _ -> anomaly ~label:"Environ.register" (Pp.str "Int31Bits should be an inductive type.") in let int31_decompilation = - match Constr.kind value with - | Constr.Ind (i31t,_) -> + match value with + | GlobRef.IndRef i31t -> constr_of_int31 i31t i31bit_type | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type.") @@ -1019,46 +1019,46 @@ fun rk value field -> vm_before_match = Some Clambda.int31_escape_before_match; native_before_match = Some (Nativelambda.before_match_int31 i31bit_type); } - | KInt31 (_, Int31Constructor) -> + | KInt31 Int31Constructor -> { empty_reactive_info with vm_constant_static = Some Clambda.compile_structured_int31; vm_constant_dynamic = Some Clambda.dynamic_int31_compilation; native_constant_static = Some Nativelambda.compile_static_int31; native_constant_dynamic = Some Nativelambda.compile_dynamic_int31; } - | KInt31 (_, Int31Plus) -> int31_binop_from_const Cbytecodes.Kaddint31 + | KInt31 Int31Plus -> int31_binop_from_const Cbytecodes.Kaddint31 CPrimitives.Int31add - | KInt31 (_, Int31PlusC) -> int31_binop_from_const Cbytecodes.Kaddcint31 + | KInt31 Int31PlusC -> int31_binop_from_const Cbytecodes.Kaddcint31 CPrimitives.Int31addc - | KInt31 (_, Int31PlusCarryC) -> int31_binop_from_const Cbytecodes.Kaddcarrycint31 + | KInt31 Int31PlusCarryC -> int31_binop_from_const Cbytecodes.Kaddcarrycint31 CPrimitives.Int31addcarryc - | KInt31 (_, Int31Minus) -> int31_binop_from_const Cbytecodes.Ksubint31 + | KInt31 Int31Minus -> int31_binop_from_const Cbytecodes.Ksubint31 CPrimitives.Int31sub - | KInt31 (_, Int31MinusC) -> int31_binop_from_const Cbytecodes.Ksubcint31 + | KInt31 Int31MinusC -> int31_binop_from_const Cbytecodes.Ksubcint31 CPrimitives.Int31subc - | KInt31 (_, Int31MinusCarryC) -> int31_binop_from_const + | KInt31 Int31MinusCarryC -> int31_binop_from_const Cbytecodes.Ksubcarrycint31 CPrimitives.Int31subcarryc - | KInt31 (_, Int31Times) -> int31_binop_from_const Cbytecodes.Kmulint31 + | KInt31 Int31Times -> int31_binop_from_const Cbytecodes.Kmulint31 CPrimitives.Int31mul - | KInt31 (_, Int31TimesC) -> int31_binop_from_const Cbytecodes.Kmulcint31 + | KInt31 Int31TimesC -> int31_binop_from_const Cbytecodes.Kmulcint31 CPrimitives.Int31mulc - | KInt31 (_, Int31Div21) -> int31_op_from_const 3 Cbytecodes.Kdiv21int31 + | KInt31 Int31Div21 -> int31_op_from_const 3 Cbytecodes.Kdiv21int31 CPrimitives.Int31div21 - | KInt31 (_, Int31Diveucl) -> int31_binop_from_const Cbytecodes.Kdivint31 + | KInt31 Int31Diveucl -> int31_binop_from_const Cbytecodes.Kdivint31 CPrimitives.Int31diveucl - | KInt31 (_, Int31AddMulDiv) -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31 + | KInt31 Int31AddMulDiv -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31 CPrimitives.Int31addmuldiv - | KInt31 (_, Int31Compare) -> int31_binop_from_const Cbytecodes.Kcompareint31 + | KInt31 Int31Compare -> int31_binop_from_const Cbytecodes.Kcompareint31 CPrimitives.Int31compare - | KInt31 (_, Int31Head0) -> int31_unop_from_const Cbytecodes.Khead0int31 + | KInt31 Int31Head0 -> int31_unop_from_const Cbytecodes.Khead0int31 CPrimitives.Int31head0 - | KInt31 (_, Int31Tail0) -> int31_unop_from_const Cbytecodes.Ktail0int31 + | KInt31 Int31Tail0 -> int31_unop_from_const Cbytecodes.Ktail0int31 CPrimitives.Int31tail0 - | KInt31 (_, Int31Lor) -> int31_binop_from_const Cbytecodes.Klorint31 + | KInt31 Int31Lor -> int31_binop_from_const Cbytecodes.Klorint31 CPrimitives.Int31lor - | KInt31 (_, Int31Land) -> int31_binop_from_const Cbytecodes.Klandint31 + | KInt31 Int31Land -> int31_binop_from_const Cbytecodes.Klandint31 CPrimitives.Int31land - | KInt31 (_, Int31Lxor) -> int31_binop_from_const Cbytecodes.Klxorint31 + | KInt31 Int31Lxor -> int31_binop_from_const Cbytecodes.Klxorint31 CPrimitives.Int31lxor | _ -> empty_reactive_info diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 502e2970a1..08b97b718e 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -215,7 +215,7 @@ val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a [@@ocaml.deprecated "Use the projection of Environ.env"] val register : - field -> Retroknowledge.entry -> Constr.constr -> safe_transformer0 + field -> GlobRef.t -> safe_transformer0 val register_inline : Constant.t -> safe_transformer0 diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 43351737e5..f59e07098b 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -256,6 +256,8 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let tyj = infer_type env typ in let proofterm = Future.chain body (fun ((body,uctx),side_eff) -> + (* don't redeclare universes which are declared for the type *) + let uctx = Univ.ContextSet.diff uctx univs in let j, uctx = match trust with | Pure -> let env = push_context_set uctx env in diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml deleted file mode 100644 index abcdb93a27..0000000000 --- a/library/dischargedhypsmap.ml +++ /dev/null @@ -1,21 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \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) *) -(************************************************************************) - -open Libnames - -type discharged_hyps = full_path list - -let discharged_hyps_map = Summary.ref Spmap.empty ~name:"discharged_hypothesis" - -let set_discharged_hyps sp hyps = - discharged_hyps_map := Spmap.add sp hyps !discharged_hyps_map - -let get_discharged_hyps sp = - try Spmap.find sp !discharged_hyps_map with Not_found -> [] diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli deleted file mode 100644 index c70677225b..0000000000 --- a/library/dischargedhypsmap.mli +++ /dev/null @@ -1,19 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \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) *) -(************************************************************************) - -open Libnames - -type discharged_hyps = full_path list - -(** Discharged hypothesis. Here we store the discharged hypothesis of each - constant or inductive type declaration. *) - -val set_discharged_hyps : full_path -> discharged_hyps -> unit -val get_discharged_hyps : full_path -> discharged_hyps diff --git a/library/global.ml b/library/global.ml index e833f71142..5872126a12 100644 --- a/library/global.ml +++ b/library/global.ml @@ -271,8 +271,8 @@ let with_global f = push_context_set false ctx; a (* spiwack: register/unregister functions for retroknowledge *) -let register field value by_clause = - globalize0 (Safe_typing.register field value by_clause) +let register field value = + globalize0 (Safe_typing.register field value) let register_inline c = globalize0 (Safe_typing.register_inline c) diff --git a/library/global.mli b/library/global.mli index 2819c187ed..6aeae9fd02 100644 --- a/library/global.mli +++ b/library/global.mli @@ -148,7 +148,7 @@ val universes_of_global : GlobRef.t -> Univ.AUContext.t (** {6 Retroknowledge } *) val register : - Retroknowledge.field -> Constr.constr -> Constr.constr -> unit + Retroknowledge.field -> GlobRef.t -> unit val register_inline : Constant.t -> unit diff --git a/library/goptions.ml b/library/goptions.ml index eafcb8fea6..dcbc46ab72 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -412,7 +412,7 @@ let print_tables () = if depr then msg ++ str " [DEPRECATED]" ++ fnl () else msg ++ fnl () in - str "Synchronous options:" ++ fnl () ++ + str "Options:" ++ fnl () ++ OptionMap.fold (fun key (name, depr, (read,_,_)) p -> p ++ print_option key name (read ()) depr) diff --git a/library/library.mllib b/library/library.mllib index 9cacaba4a7..8f694f4a31 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -11,7 +11,6 @@ Loadpath Library States Kindops -Dischargedhypsmap Goptions Decls Keys diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index bbc0a37c69..fd2d90e9cf 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1469,7 +1469,7 @@ let do_build_inductive (rel_constructors) in let rel_ind i ext_rel_constructors = - (((CAst.make @@ relnames.(i)), None), + ((CAst.make @@ relnames.(i)), rel_params, Some rel_arities.(i), ext_rel_constructors),[] @@ -1499,14 +1499,14 @@ let do_build_inductive let _time2 = System.get_time () in try with_full_print - (Flags.silently (ComInductive.do_mutual_inductive ~template:None rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters)) + (Flags.silently (ComInductive.do_mutual_inductive ~template:None None rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters)) Declarations.Finite with | UserError(s,msg) as e -> let _time3 = System.get_time () in (* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) let repacked_rel_inds = - List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) + List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) rel_inds in let msg = @@ -1521,7 +1521,7 @@ let do_build_inductive let _time3 = System.get_time () in (* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) let repacked_rel_inds = - List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) + List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) rel_inds in let msg = diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 84f13d2131..73490a2dfd 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -94,7 +94,7 @@ let let_evar name typ = in let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Namegen.IntroFresh id) typ in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (Tactics.letin_tac None (Name.Name id) evar None Locusops.nowhere) + (Tactics.pose_tac (Name.Name id) evar) end let hget_evar n = diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 38600695dc..f4555509cc 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -311,78 +311,3 @@ let pr_lpar_id_colon _ _ _ _ = mt () ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY pr_lpar_id_colon | [ local_test_lpar_id_colon(x) ] -> [ () ] END - -(* spiwack: the print functions are incomplete, but I don't know what they are - used for *) -let pr_r_int31_field i31f = - str "int31 " ++ - match i31f with - | Retroknowledge.Int31Bits -> str "bits" - | Retroknowledge.Int31Type -> str "type" - | Retroknowledge.Int31Twice -> str "twice" - | Retroknowledge.Int31TwicePlusOne -> str "twice plus one" - | Retroknowledge.Int31Phi -> str "phi" - | Retroknowledge.Int31PhiInv -> str "phi inv" - | Retroknowledge.Int31Plus -> str "plus" - | Retroknowledge.Int31Times -> str "times" - | Retroknowledge.Int31Constructor -> assert false - | Retroknowledge.Int31PlusC -> str "plusc" - | Retroknowledge.Int31PlusCarryC -> str "pluscarryc" - | Retroknowledge.Int31Minus -> str "minus" - | Retroknowledge.Int31MinusC -> str "minusc" - | Retroknowledge.Int31MinusCarryC -> str "minuscarryc" - | Retroknowledge.Int31TimesC -> str "timesc" - | Retroknowledge.Int31Div21 -> str "div21" - | Retroknowledge.Int31Div -> str "div" - | Retroknowledge.Int31Diveucl -> str "diveucl" - | Retroknowledge.Int31AddMulDiv -> str "addmuldiv" - | Retroknowledge.Int31Compare -> str "compare" - | Retroknowledge.Int31Head0 -> str "head0" - | Retroknowledge.Int31Tail0 -> str "tail0" - | Retroknowledge.Int31Lor -> str "lor" - | Retroknowledge.Int31Land -> str "land" - | Retroknowledge.Int31Lxor -> str "lxor" - -let pr_retroknowledge_field f = - match f with - (* | Retroknowledge.KEq -> str "equality" - | Retroknowledge.KNat natf -> pr_r_nat_field () () () natf - | Retroknowledge.KN nf -> pr_r_n_field () () () nf *) - | Retroknowledge.KInt31 (group, i31f) -> (pr_r_int31_field i31f) ++ - spc () ++ str "in " ++ qs group - -VERNAC ARGUMENT EXTEND retroknowledge_int31 -PRINTED BY pr_r_int31_field -| [ "int31" "bits" ] -> [ Retroknowledge.Int31Bits ] -| [ "int31" "type" ] -> [ Retroknowledge.Int31Type ] -| [ "int31" "twice" ] -> [ Retroknowledge.Int31Twice ] -| [ "int31" "twice" "plus" "one" ] -> [ Retroknowledge.Int31TwicePlusOne ] -| [ "int31" "phi" ] -> [ Retroknowledge.Int31Phi ] -| [ "int31" "phi" "inv" ] -> [ Retroknowledge.Int31PhiInv ] -| [ "int31" "plus" ] -> [ Retroknowledge.Int31Plus ] -| [ "int31" "plusc" ] -> [ Retroknowledge.Int31PlusC ] -| [ "int31" "pluscarryc" ] -> [ Retroknowledge.Int31PlusCarryC ] -| [ "int31" "minus" ] -> [ Retroknowledge.Int31Minus ] -| [ "int31" "minusc" ] -> [ Retroknowledge.Int31MinusC ] -| [ "int31" "minuscarryc" ] -> [ Retroknowledge.Int31MinusCarryC ] -| [ "int31" "times" ] -> [ Retroknowledge.Int31Times ] -| [ "int31" "timesc" ] -> [ Retroknowledge.Int31TimesC ] -| [ "int31" "div21" ] -> [ Retroknowledge.Int31Div21 ] -| [ "int31" "div" ] -> [ Retroknowledge.Int31Div ] -| [ "int31" "diveucl" ] -> [ Retroknowledge.Int31Diveucl ] -| [ "int31" "addmuldiv" ] -> [ Retroknowledge.Int31AddMulDiv ] -| [ "int31" "compare" ] -> [ Retroknowledge.Int31Compare ] -| [ "int31" "head0" ] -> [ Retroknowledge.Int31Head0 ] -| [ "int31" "tail0" ] -> [ Retroknowledge.Int31Tail0 ] -| [ "int31" "lor" ] -> [ Retroknowledge.Int31Lor ] -| [ "int31" "land" ] -> [ Retroknowledge.Int31Land ] -| [ "int31" "lxor" ] -> [ Retroknowledge.Int31Lxor ] -END - -VERNAC ARGUMENT EXTEND retroknowledge_field -PRINTED BY pr_retroknowledge_field -(*| [ "equality" ] -> [ Retroknowledge.KEq ] -| [ retroknowledge_nat(n)] -> [ Retroknowledge.KNat n ] -| [ retroknowledge_binary_n (n)] -> [ Retroknowledge.KN n ]*) -| [ retroknowledge_int31 (i) "in" string(g)] -> [ Retroknowledge.KInt31(g,i) ] -END diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index e477b12cd3..fa70235975 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -72,11 +72,6 @@ val test_lpar_id_colon : unit Pcoq.Entry.t val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type -(** Spiwack: Primitive for retroknowledge registration *) - -val retroknowledge_field : Retroknowledge.field Pcoq.Entry.t -val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type - val wit_in_clause : (lident Locus.clause_expr, lident Locus.clause_expr, diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index dc027c4041..8dad6260ae 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -545,22 +545,6 @@ END (**********************************************************************) -(*spiwack : Vernac commands for retroknowledge *) - -VERNAC COMMAND EXTEND RetroknowledgeRegister CLASSIFIED AS SIDEFF - | [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] -> - [ let env = Global.env () in - let evd = Evd.from_env env in - let tc,_ctx = Constrintern.interp_constr env evd c in - let tb,_ctx(*FIXME*) = Constrintern.interp_constr env evd b in - let tc = EConstr.to_constr evd tc in - let tb = EConstr.to_constr evd tb in - Global.register f tc tb ] -END - - - -(**********************************************************************) (* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as defined by Conor McBride *) TACTIC EXTEND generalize_eqs diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index f4313a8fa3..71da6c7667 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1664,16 +1664,18 @@ and interp_atomic ist tac : unit Proofview.tactic = (* We try to fully-typecheck the term *) let flags = open_constr_use_classes_flags () in let (sigma,c_interp) = interp_open_constr ~flags ist env sigma c in - let let_tac b na c cl eqpat = - let id = Option.default (make IntroAnonymous) eqpat in - let with_eq = if b then None else Some (true,id) in - Tactics.letin_tac with_eq na c None cl - in let na = interp_name ist env sigma na in + let let_tac = + if b then Tactics.pose_tac na c_interp + else + let id = Option.default (make IntroAnonymous) eqpat in + let with_eq = Some (true, id) in + Tactics.letin_tac with_eq na c_interp None Locusops.nowhere + in Tacticals.New.tclWITHHOLES ev (name_atomic ~env (TacLetTac(ev,na,c_interp,clp,b,eqpat)) - (let_tac b na c_interp clp eqpat)) sigma + let_tac) sigma else (* We try to keep the pattern structure as much as possible *) let let_pat_tac b na c cl eqpat = diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index 59fd9b8017..094adfda7a 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -85,6 +85,7 @@ Ltac zify_binop t thm a b:= Ltac zify_op_1 := match goal with + | x := ?t : Z |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x | |- context [ Z.max ?a ?b ] => zify_binop Z.max Z.max_spec a b | H : context [ Z.max ?a ?b ] |- _ => zify_binop Z.max Z.max_spec a b | |- context [ Z.min ?a ?b ] => zify_binop Z.min Z.min_spec a b @@ -114,6 +115,7 @@ Ltac hide_Z_of_nat t := Ltac zify_nat_rel := match goal with (* I: equalities *) + | x := ?t : nat |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x | |- (@eq nat ?a ?b) => apply (Nat2Z.inj a b) (* shortcut *) | H : context [ @eq nat ?a ?b ] |- _ => rewrite <- (Nat2Z.inj_iff a b) in H | |- context [ @eq nat ?a ?b ] => rewrite <- (Nat2Z.inj_iff a b) @@ -223,6 +225,7 @@ Ltac hide_Zpos t := Ltac zify_positive_rel := match goal with (* I: equalities *) + | x := ?t : positive |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x | |- (@eq positive ?a ?b) => apply Pos2Z.inj | H : context [ @eq positive ?a ?b ] |- _ => rewrite <- (Pos2Z.inj_iff a b) in H | |- context [ @eq positive ?a ?b ] => rewrite <- (Pos2Z.inj_iff a b) @@ -348,6 +351,7 @@ Ltac hide_Z_of_N t := Ltac zify_N_rel := match goal with (* I: equalities *) + | x := ?t : N |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x | |- (@eq N ?a ?b) => apply (N2Z.inj a b) (* shortcut *) | H : context [ @eq N ?a ?b ] |- _ => rewrite <- (N2Z.inj_iff a b) in H | |- context [ @eq N ?a ?b ] => rewrite <- (N2Z.inj_iff a b) diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index e367cd32d6..f67cf20e49 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -25,9 +25,7 @@ module RelDecl = Context.Rel.Declaration (** 8. Forward chaining tactics (pose, set, have, suffice, wlog) *) (** Defined identifier *) - -let settac id c = Tactics.letin_tac None (Name id) c None -let posetac id cl = Proofview.V82.of_tactic (settac id cl Locusops.nowhere) +let posetac id cl = Proofview.V82.of_tactic (Tactics.pose_tac (Name id) cl) let ssrposetac (id, (_, t)) gl = let ist, t = diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index 83581f3416..f12f9fac0f 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -14,7 +14,6 @@ open Names open Constr open Termops open Tacmach -open Locusops open Ssrast open Ssrcommon @@ -82,8 +81,7 @@ let pf_clauseids gl gens clseq = let hidden_clseq = function InHyps | InHypsSeq | InAllHyps -> true | _ -> false -let settac id c = Tactics.letin_tac None (Name id) c None -let posetac id cl = Proofview.V82.of_tactic (settac id cl nowhere) +let posetac id cl = Proofview.V82.of_tactic (Tactics.pose_tac (Name id) cl) let hidetacs clseq idhide cl0 = if not (hidden_clseq clseq) then [] else diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 7baa755ab5..81e8bd06f5 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1726,7 +1726,7 @@ let abstract_tycon ?loc env evdref subst tycon extenv t = List.map (fun d -> local_occur_var !evdref (NamedDecl.get_id d) u) (named_context !!extenv) in let filter = Filter.make (rel_filter @ named_filter) in - let candidates = u :: List.map mkRel vl in + let candidates = List.rev (u :: List.map mkRel vl) in let ev = evd_comb1 (Evarutil.new_evar !!extenv ~src ~filter ~candidates) evdref ty in lift k ev in diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 984fa92c0e..6c52dacaa9 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1317,6 +1317,7 @@ let rec solve_unconstrained_evars_with_candidates ts evd = let rec aux = function | [] -> user_err Pp.(str "Unsolvable existential variables.") | a::l -> + (* In case of variables, most recent ones come first *) try let conv_algo = evar_conv_x ts in let evd = check_evar_instance evd evk a conv_algo in @@ -1327,9 +1328,9 @@ let rec solve_unconstrained_evars_with_candidates ts evd = with | IllTypedInstance _ -> aux l | e when Pretype_errors.precatchable_exception e -> aux l in - (* List.rev is there to favor most dependent solutions *) - (* and favor progress when used with the refine tactics *) - let evd = aux (List.rev l) in + (* Expected invariant: most dependent solutions come first *) + (* so as to favor progress when used with the refine tactics *) + let evd = aux l in solve_unconstrained_evars_with_candidates ts evd let solve_unconstrained_impossible_cases env evd = diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 3f5d186d4e..2dd3721980 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -599,11 +599,12 @@ let solve_pattern_eqn env sigma l c = let make_projectable_subst aliases sigma evi args = let sign = evar_filtered_context evi in let evar_aliases = compute_var_aliases sign sigma in - let (_,full_subst,cstr_subst) = - List.fold_right - (fun decl (args,all,cstrs) -> + let (_,full_subst,cstr_subst,_) = + List.fold_right_i + (fun i decl (args,all,cstrs,revmap) -> match decl,args with | LocalAssum (id,c), a::rest -> + let revmap = Id.Map.add id i revmap in let cstrs = let a',args = decompose_app_vect sigma a in match EConstr.kind sigma a' with @@ -611,22 +612,26 @@ let make_projectable_subst aliases sigma evi args = let l = try Constrmap.find (fst cstr) cstrs with Not_found -> [] in Constrmap.add (fst cstr) ((args,id)::l) cstrs | _ -> cstrs in - (rest,Id.Map.add id [a,normalize_alias_opt sigma aliases a,id] all,cstrs) + let all = Int.Map.add i [a,normalize_alias_opt sigma aliases a,id] all in + (rest,all,cstrs,revmap) | LocalDef (id,c,_), a::rest -> + let revmap = Id.Map.add id i revmap in (match EConstr.kind sigma c with | Var id' -> let idc = normalize_alias_var sigma evar_aliases id' in - let sub = try Id.Map.find idc all with Not_found -> [] in + let ic, sub = + try let ic = Id.Map.find idc revmap in ic, Int.Map.find ic all + with Not_found -> i, [] (* e.g. [idc] is a filtered variable: treat [id] as an assumption *) in if List.exists (fun (c,_,_) -> EConstr.eq_constr sigma a c) sub then - (rest,all,cstrs) + (rest,all,cstrs,revmap) else - (rest, - Id.Map.add idc ((a,normalize_alias_opt sigma aliases a,id)::sub) all, - cstrs) + let all = Int.Map.add ic ((a,normalize_alias_opt sigma aliases a,id)::sub) all in + (rest,all,cstrs,revmap) | _ -> - (rest,Id.Map.add id [a,normalize_alias_opt sigma aliases a,id] all,cstrs)) - | _ -> anomaly (Pp.str "Instance does not match its signature.")) - sign (Array.rev_to_list args,Id.Map.empty,Constrmap.empty) in + let all = Int.Map.add i [a,normalize_alias_opt sigma aliases a,id] all in + (rest,all,cstrs,revmap)) + | _ -> anomaly (Pp.str "Instance does not match its signature.")) 0 + sign (Array.rev_to_list args,Int.Map.empty,Constrmap.empty,Id.Map.empty) in (full_subst,cstr_subst) (*------------------------------------* @@ -793,11 +798,11 @@ let rec assoc_up_to_alias sigma aliases y yc = function let rec find_projectable_vars with_evars aliases sigma y subst = let yc = normalize_alias sigma aliases y in - let is_projectable idc idcl subst' = + let is_projectable idc idcl (subst1,subst2 as subst') = (* First test if some [id] aliased to [idc] is bound to [y] in [subst] *) try let id = assoc_up_to_alias sigma aliases y yc idcl in - (id,ProjectVar)::subst' + (id,ProjectVar)::subst1,subst2 with Not_found -> (* Then test if [idc] is (indirectly) bound in [subst] to some evar *) (* projectable on [y] *) @@ -812,14 +817,18 @@ let rec find_projectable_vars with_evars aliases sigma y subst = let subst,_ = make_projectable_subst aliases sigma evi argsv in let l = find_projectable_vars with_evars aliases sigma y subst in match l with - | [id',p] -> (id,ProjectEvar (t,evi,id',p))::subst' + | [id',p] -> (subst1,(id,ProjectEvar (t,evi,id',p))::subst2) | _ -> subst' end | [] -> subst' | _ -> anomaly (Pp.str "More than one non var in aliases class of evar instance.") else subst' in - Id.Map.fold is_projectable subst [] + let subst1,subst2 = Int.Map.fold is_projectable subst ([],[]) in + (* We return the substitution with ProjectVar first (from most + recent to oldest var), followed by ProjectEvar (from most recent + to oldest var too) *) + subst1 @ subst2 (* [filter_solution] checks if one and only one possible projection exists * among a set of solutions to a projection problem *) @@ -842,25 +851,6 @@ let rec find_solution_type evarenv = function | (id,ProjectEvar _)::l -> find_solution_type evarenv l | [] -> assert false -let is_preferred_projection_over sign (id,p) (id',p') = - (* We give priority to projection of variables over instantiation of - an evar considering that the latter is a stronger decision which - may even procude an incorrect (ill-typed) solution *) - match p, p' with - | ProjectEvar _, ProjectVar -> false - | ProjectVar, ProjectEvar _ -> true - | _, _ -> - List.index Id.equal id sign < List.index Id.equal id' sign - -let choose_projection evi sols = - let sign = List.map get_id (evar_filtered_context evi) in - match sols with - | y::l -> - List.fold_right (fun (id,p as x) (id',_ as y) -> - if is_preferred_projection_over sign x y then x else y) - l y - | _ -> assert false - (* In case the solution to a projection problem requires the instantiation of * subsidiary evars, [do_projection_effects] performs them; it * also try to instantiate the type of those subsidiary evars if their @@ -1447,12 +1437,8 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = let c, p = match sols with | [] -> raise Not_found | [id,p] -> (mkVar id, p) - | _ -> - if choose then - let (id,p) = choose_projection evi sols in - (mkVar id, p) - else - raise (NotUniqueInType sols) + | (id,p)::_ -> + if choose then (mkVar id, p) else raise (NotUniqueInType sols) in let ty = lazy (Retyping.get_type_of env !evdref (of_alias t)) in let evd = do_projection_effects (evar_define conv_algo ~choose) env ty !evdref p in @@ -1556,7 +1542,8 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = let t = map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1) imitate envk t in - t::l + (* Less dependent solutions come last *) + l@[t] with e when CErrors.noncritical e -> l in (match candidates with | [x] -> x diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 246acfc92e..20185363e6 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -123,7 +123,7 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs = try if const then let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(0)) params in - Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (mkInd ind) tag, ctyp + Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (GlobRef.IndRef ind) tag, ctyp else raise Not_found with Not_found -> diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 82c732c59f..c30c4f0932 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -79,7 +79,7 @@ let construct_of_constr const env tag typ = (* spiwack : here be a branch for specific decompilation handled by retroknowledge *) try if const then - ((Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (mkIndU indu) tag), + ((Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (GlobRef.IndRef ind) tag), typ) (*spiwack: this may need to be changed in case there are parameters in the type which may cause a constant value to have an arity. (type_constructor seems to be all about parameters actually) diff --git a/printing/printer.ml b/printing/printer.ml index 804999986c..67d71332b0 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -947,8 +947,8 @@ let pr_assumptionset env sigma s = let mp,_,lab = Constant.repr3 kn in str (ModPath.to_string mp) ++ str "." ++ Label.print lab in - let safe_pr_ltype typ = - try str " : " ++ pr_ltype typ + let safe_pr_ltype env sigma typ = + try str " : " ++ pr_ltype_env env sigma typ with e when CErrors.noncritical e -> mt () in let safe_pr_ltype_relctx (rctx, typ) = @@ -959,7 +959,7 @@ let pr_assumptionset env sigma s = let pr_axiom env ax typ = match ax with | Constant kn -> - safe_pr_constant env kn ++ safe_pr_ltype typ + safe_pr_constant env kn ++ safe_pr_ltype env sigma typ | Positive m -> hov 2 (MutInd.print m ++ spc () ++ strbrk"is positive.") | Guarded kn -> @@ -969,7 +969,7 @@ let pr_assumptionset env sigma s = let (v, a, o, tr) = accu in match t with | Variable id -> - let var = pr_id id ++ str " : " ++ pr_ltype typ in + let var = pr_id id ++ str " : " ++ pr_ltype_env env sigma typ in (var :: v, a, o, tr) | Axiom (axiom, []) -> let ax = pr_axiom env axiom typ in @@ -983,10 +983,10 @@ let pr_assumptionset env sigma s = l in (v, ax :: a, o, tr) | Opaque kn -> - let opq = safe_pr_constant env kn ++ safe_pr_ltype typ in + let opq = safe_pr_constant env kn ++ safe_pr_ltype env sigma typ in (v, a, opq :: o, tr) | Transparent kn -> - let tran = safe_pr_constant env kn ++ safe_pr_ltype typ in + let tran = safe_pr_constant env kn ++ safe_pr_ltype env sigma typ in (v, a, o, tran :: tr) in let (vars, axioms, opaque, trans) = diff --git a/printing/printer.mli b/printing/printer.mli index 47be8b7eaa..518c5b930b 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -220,13 +220,14 @@ val pr_ne_evar_set : Pp.t -> Pp.t -> evar_map -> Evar.Set.t -> Pp.t val pr_prim_rule : prim_rule -> Pp.t +[@@ocaml.deprecated "[pr_prim_rule] is scheduled to be removed along with the legacy proof engine"] val print_and_diff : Proof.t option -> Proof.t option -> unit (** Backwards compatibility *) val prterm : constr -> Pp.t (** = pr_lconstr *) - +[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] (** Declarations for the "Print Assumption" command *) type axiom = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d536204ec3..95d545b046 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2690,6 +2690,34 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty = let (sigma, x) = new_evar newenv sigma ~principal:true ~store ccl in (sigma, mkNamedLetIn id c t x) +let pose_tac na c = + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let hyps = named_context_val env in + let concl = Proofview.Goal.concl gl in + let t = typ_of env sigma c in + let (sigma, t) = Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma t in + let id = match na with + | Name id -> + let () = if mem_named_context_val id hyps then + user_err (str "Variable " ++ Id.print id ++ str " is already declared.") + in + id + | Anonymous -> + let id = id_of_name_using_hdchar env sigma t Anonymous in + next_ident_away_in_goal id (ids_of_named_context_val hyps) + in + Proofview.Unsafe.tclEVARS sigma <*> + Refine.refine ~typecheck:false begin fun sigma -> + let nhyps = EConstr.push_named_context_val (NamedDecl.LocalDef (id, c, t)) hyps in + let (sigma, ev) = Evarutil.new_pure_evar nhyps sigma concl in + let inst = Array.map_of_list (fun d -> mkVar (get_id d)) (named_context env) in + let body = mkEvar (ev, Array.append [|mkRel 1|] inst) in + (sigma, mkLetIn (Name id, c, t, body)) + end + end + let letin_tac with_eq id c ty occs = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 57f20d2ff2..c088e404b0 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -390,6 +390,8 @@ val cut : types -> unit Proofview.tactic (** {6 Tactics for adding local definitions. } *) +val pose_tac : Name.t -> constr -> unit Proofview.tactic + val letin_tac : (bool * intro_pattern_naming) option -> Name.t -> constr -> types option -> clause -> unit Proofview.tactic diff --git a/test-suite/bugs/2428.v b/test-suite/bugs/closed/2428.v index a4f587a58d..b398a76d91 100644 --- a/test-suite/bugs/2428.v +++ b/test-suite/bugs/closed/2428.v @@ -5,6 +5,6 @@ Definition myFact := forall x, P x. Hint Extern 1 (P _) => progress (unfold myFact in *). Lemma test : (True -> myFact) -> P 3. -Proof. +Proof. intros. debug eauto. Qed. diff --git a/test-suite/bugs/closed/2670.v b/test-suite/bugs/closed/2670.v index c401420e94..791889b24b 100644 --- a/test-suite/bugs/closed/2670.v +++ b/test-suite/bugs/closed/2670.v @@ -15,6 +15,14 @@ Proof. refine (match e return _ with refl_equal => _ end). reflexivity. Undo 2. + (** Check insensitivity to alphabetic order *) + refine (match e as a in _ = b return _ with refl_equal => _ end). + reflexivity. + Undo 2. + (** Check insensitivity to alphabetic order *) + refine (match e as z in _ = y return _ with refl_equal => _ end). + reflexivity. + Undo 2. (* Next line similarly has a dependent and a non dependent solution *) refine (match e with refl_equal => _ end). reflexivity. diff --git a/test-suite/bugs/4623.v b/test-suite/bugs/closed/4623.v index 7ecfd98b67..7ecfd98b67 100644 --- a/test-suite/bugs/4623.v +++ b/test-suite/bugs/closed/4623.v diff --git a/test-suite/bugs/4624.v b/test-suite/bugs/closed/4624.v index f5ce981cd0..f5ce981cd0 100644 --- a/test-suite/bugs/4624.v +++ b/test-suite/bugs/closed/4624.v diff --git a/test-suite/bugs/7333.v b/test-suite/bugs/closed/7333.v index fba5b9029d..fba5b9029d 100644 --- a/test-suite/bugs/7333.v +++ b/test-suite/bugs/closed/7333.v diff --git a/test-suite/bugs/closed/7754.v b/test-suite/bugs/closed/7754.v new file mode 100644 index 0000000000..229df93773 --- /dev/null +++ b/test-suite/bugs/closed/7754.v @@ -0,0 +1,21 @@ + +Set Universe Polymorphism. + +Module OK. + + Inductive one@{i j} : Type@{i} := + with two : Type@{j} := . + Check one@{Set Type} : Set. + Fail Check two@{Set Type} : Set. + +End OK. + +Module Bad. + + Fail Inductive one := + with two@{i +} : Type@{i} := . + + Fail Inductive one@{i +} := + with two@{i +} := . + +End Bad. diff --git a/test-suite/misc/poly-capture-global-univs.sh b/test-suite/misc/poly-capture-global-univs.sh new file mode 100755 index 0000000000..e066ac039b --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs.sh @@ -0,0 +1,19 @@ +#!/usr/bin/env bash + +set -e + +export COQBIN=$BIN +export PATH=$COQBIN:$PATH + +cd misc/poly-capture-global-univs/ + +coq_makefile -f _CoqProject -o Makefile + +make clean + +make src/evil_plugin.cmxs + +if make; then + >&2 echo 'Should have failed!' + exit 1 +fi diff --git a/test-suite/misc/poly-capture-global-univs/.gitignore b/test-suite/misc/poly-capture-global-univs/.gitignore new file mode 100644 index 0000000000..f5a6d22b8e --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/.gitignore @@ -0,0 +1 @@ +/Makefile* diff --git a/test-suite/misc/poly-capture-global-univs/_CoqProject b/test-suite/misc/poly-capture-global-univs/_CoqProject new file mode 100644 index 0000000000..70ec246062 --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/_CoqProject @@ -0,0 +1,9 @@ +-Q theories Evil +-I src + +src/evil.ml4 +src/evilImpl.ml +src/evilImpl.mli +src/evil_plugin.mlpack +theories/evil.v + diff --git a/test-suite/misc/poly-capture-global-univs/src/evil.ml4 b/test-suite/misc/poly-capture-global-univs/src/evil.ml4 new file mode 100644 index 0000000000..565e979aaa --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/src/evil.ml4 @@ -0,0 +1,9 @@ + +open Stdarg +open EvilImpl + +DECLARE PLUGIN "evil_plugin" + +VERNAC COMMAND FUNCTIONAL EXTEND VernacEvil CLASSIFIED AS SIDEFF +| [ "Evil" ident(x) ident(y) ] -> [ fun ~atts ~st -> evil x y; st ] +END diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml new file mode 100644 index 0000000000..6d8ce7c5d7 --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml @@ -0,0 +1,22 @@ +open Names + +let evil t f = + let open Univ in + let open Entries in + let open Decl_kinds in + let open Constr in + let k = IsDefinition Definition in + let u = Level.var 0 in + let tu = mkType (Universe.make u) in + let te = Declare.definition_entry + ~univs:(Monomorphic_const_entry (ContextSet.singleton u)) tu + in + let tc = Declare.declare_constant t (DefinitionEntry te, k) in + let tc = mkConst tc in + + let fe = Declare.definition_entry + ~univs:(Polymorphic_const_entry (UContext.make (Instance.of_array [|u|],Constraint.empty))) + ~types:(Term.mkArrow tc tu) + (mkLambda (Name.Name (Id.of_string "x"), tc, mkRel 1)) + in + ignore (Declare.declare_constant f (DefinitionEntry fe, k)) diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.mli b/test-suite/misc/poly-capture-global-univs/src/evilImpl.mli new file mode 100644 index 0000000000..97c7e3dadd --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.mli @@ -0,0 +1,2 @@ + +val evil : Names.Id.t -> Names.Id.t -> unit diff --git a/test-suite/misc/poly-capture-global-univs/src/evil_plugin.mlpack b/test-suite/misc/poly-capture-global-univs/src/evil_plugin.mlpack new file mode 100644 index 0000000000..0093328a40 --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/src/evil_plugin.mlpack @@ -0,0 +1,2 @@ +EvilImpl +Evil diff --git a/test-suite/misc/poly-capture-global-univs/theories/evil.v b/test-suite/misc/poly-capture-global-univs/theories/evil.v new file mode 100644 index 0000000000..7fd98c2773 --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/theories/evil.v @@ -0,0 +1,13 @@ + +Declare ML Module "evil_plugin". + +Evil T f. (* <- if this doesn't fail then the rest goes through *) + +Definition g : Type -> Set := f. + +Require Import Hurkens. + +Lemma absurd : False. +Proof. + exact (TypeNeqSmallType.paradox (g Type) eq_refl). +Qed. diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index b60b1ee863..94b86fc222 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -125,13 +125,15 @@ s : nat fun _ : nat => 9 : nat -> nat -fun (x : nat) (p : x = x) => match p with - | ONE => ONE - end = p +fun (x : nat) (p : x = x) => +match p in (_ = n) return (n = n) with +| ONE => ONE +end = p : forall x : nat, x = x -> Prop -fun (x : nat) (p : x = x) => match p with - | 1 => 1 - end = p +fun (x : nat) (p : x = x) => +match p in (_ = n) return (n = n) with +| 1 => 1 +end = p : forall x : nat, x = x -> Prop bar 0 : nat diff --git a/test-suite/success/ROmega4.v b/test-suite/success/ROmega4.v index 58ae5b8fb8..a724592749 100644 --- a/test-suite/success/ROmega4.v +++ b/test-suite/success/ROmega4.v @@ -3,12 +3,12 @@ See also #148 for the corresponding improvement in Omega. *) -Require Import ZArith ROmega. +Require Import ZArith Lia. Open Scope Z. Goal let x := 3 in x = 3. intros. -romega. +lia. Qed. (** Example seen in #4132 @@ -22,5 +22,5 @@ Lemma foo (H : - zxy' <= zxy) (H' : zxy' <= x') : - b <= zxy. Proof. -romega. +lia. Qed. diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index b287b5facf..e1df9ba84a 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -559,3 +559,26 @@ split. - (* clear b:True *) match goal with H:_ |- _ => clear H end. (* use a:0=0 *) match goal with H:_ |- _ => exact H end. Qed. + +(* Test choice of most dependent solution *) +Goal forall n, n = 0 -> exists p, p = n /\ p = 0. +intros. eexists ?[p]. split. rewrite H. +reflexivity. (* Compatibility tells [?p:=n] rather than [?p:=0] *) +exact H. (* this checks that the goal is [n=0], not [0=0] *) +Qed. + +(* Check insensitivity to alphabetic order of names*) +(* In both cases, the last name is conventionally chosen *) +(* Before 8.9, the name coming first in alphabetic order *) +(* was chosen. *) +Goal forall m n, m = n -> n = 0 -> exists p, p = n /\ p = 0. +intros. eexists ?[p]. split. rewrite H. +reflexivity. +exact H0. +Qed. + +Goal forall n m, n = m -> m = 0 -> exists p, p = m /\ p = 0. +intros. eexists ?[p]. split. rewrite H. +reflexivity. +exact H0. +Qed. diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index 77ab624ca5..ca7d3ec074 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -45,8 +45,8 @@ Inductive int31 : Type := I31 : digits31 int31. (* spiwack: Registration of the type of integers, so that the matchs in the functions below perform dynamic decompilation (otherwise some segfault occur when they are applied to one non-closed term and one closed term). *) -Register digits as int31 bits in "coq_int31" by True. -Register int31 as int31 type in "coq_int31" by True. +Register digits as int31.bits. +Register int31 as int31.type. Declare Scope int31_scope. Declare ML Module "int31_syntax_plugin". @@ -345,21 +345,21 @@ Definition lor31 n m := phi_inv (Z.lor (phi n) (phi m)). Definition land31 n m := phi_inv (Z.land (phi n) (phi m)). Definition lxor31 n m := phi_inv (Z.lxor (phi n) (phi m)). -Register add31 as int31 plus in "coq_int31" by True. -Register add31c as int31 plusc in "coq_int31" by True. -Register add31carryc as int31 pluscarryc in "coq_int31" by True. -Register sub31 as int31 minus in "coq_int31" by True. -Register sub31c as int31 minusc in "coq_int31" by True. -Register sub31carryc as int31 minuscarryc in "coq_int31" by True. -Register mul31 as int31 times in "coq_int31" by True. -Register mul31c as int31 timesc in "coq_int31" by True. -Register div3121 as int31 div21 in "coq_int31" by True. -Register div31 as int31 diveucl in "coq_int31" by True. -Register compare31 as int31 compare in "coq_int31" by True. -Register addmuldiv31 as int31 addmuldiv in "coq_int31" by True. -Register lor31 as int31 lor in "coq_int31" by True. -Register land31 as int31 land in "coq_int31" by True. -Register lxor31 as int31 lxor in "coq_int31" by True. +Register add31 as int31.plus. +Register add31c as int31.plusc. +Register add31carryc as int31.pluscarryc. +Register sub31 as int31.minus. +Register sub31c as int31.minusc. +Register sub31carryc as int31.minuscarryc. +Register mul31 as int31.times. +Register mul31c as int31.timesc. +Register div3121 as int31.div21. +Register div31 as int31.diveucl. +Register compare31 as int31.compare. +Register addmuldiv31 as int31.addmuldiv. +Register lor31 as int31.lor. +Register land31 as int31.land. +Register lxor31 as int31.lxor. Definition lnot31 n := lxor31 Tn n. Definition ldiff31 n m := land31 n (lnot31 m). @@ -485,5 +485,5 @@ Definition tail031 (i:int31) := end) i On. -Register head031 as int31 head0 in "coq_int31" by True. -Register tail031 as int31 tail0 in "coq_int31" by True. +Register head031 as int31.head0. +Register tail031 as int31.tail0. diff --git a/tools/coqdoc/dune b/tools/coqdoc/dune new file mode 100644 index 0000000000..8e05c7d97e --- /dev/null +++ b/tools/coqdoc/dune @@ -0,0 +1,6 @@ +(executable + (name main) + (public_name coqdoc) + (libraries str coq.config)) + +(ocamllex cpretty) diff --git a/tools/dune b/tools/dune index 2ba0e3fe8a..05a620fb07 100644 --- a/tools/dune +++ b/tools/dune @@ -10,6 +10,10 @@ (modules coq_makefile) (libraries coq.lib)) +(install + (section lib) + (files (CoqMakefile.in as tools/CoqMakefile.in))) + (executable (name coqdep) (public_name coqdep) @@ -19,6 +23,14 @@ (ocamllex coqdep_lexer) (executable + (name coqwc) + (public_name coqwc) + (modules coqwc) + (libraries)) + +(ocamllex coqwc) + +(executable (name coq_tex) (public_name coq_tex) (modules coq_tex) diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index fb9d21c429..7b28895814 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -67,7 +67,6 @@ let push_types env idl tl = type structured_one_inductive_expr = { ind_name : Id.t; - ind_univs : universe_decl_expr option; ind_arity : constr_expr; ind_lc : (Id.t * constr_expr) list } @@ -348,13 +347,12 @@ let restrict_inductive_universes sigma ctx_params arities constructors = let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in Evd.restrict_universe_context sigma uvars -let interp_mutual_inductive_gen env0 ~template (uparamsl,paramsl,indl) notations cum poly prv finite = +let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations cum poly prv finite = check_all_names_different indl; List.iter check_param paramsl; if not (List.is_empty uparamsl) && not (List.is_empty notations) then user_err (str "Inductives with uniform parameters may not have attached notations."); - let pl = (List.hd indl).ind_univs in - let sigma, decl = interp_univ_decl_opt env0 pl in + let sigma, udecl = interp_univ_decl_opt env0 udecl in let sigma, (uimpls, ((env_uparams, ctx_uparams), useruimpls)) = interp_context_evars env0 sigma uparamsl in let sigma, (impls, ((env_params, ctx_params), userimpls)) = @@ -424,7 +422,7 @@ let interp_mutual_inductive_gen env0 ~template (uparamsl,paramsl,indl) notations let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in let arityconcl = List.map (Option.map (EConstr.ESorts.kind sigma)) arityconcl in let sigma = restrict_inductive_universes sigma ctx_params arities constructors in - let uctx = Evd.check_univ_decl ~poly sigma decl in + let uctx = Evd.check_univ_decl ~poly sigma udecl in List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr c)) arities; Context.Rel.iter (fun c -> check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr c)) ctx_params; List.iter (fun (_,ctyps,_) -> @@ -478,8 +476,8 @@ let interp_mutual_inductive_gen env0 ~template (uparamsl,paramsl,indl) notations InferCumulativity.infer_inductive env_ar mind_ent else mind_ent), Evd.universe_binders sigma, impls -let interp_mutual_inductive ~template (paramsl,indl) notations cum poly prv finite = - interp_mutual_inductive_gen (Global.env()) ~template ([],paramsl,indl) notations cum poly prv finite +let interp_mutual_inductive ~template udecl (paramsl,indl) notations cum poly prv finite = + interp_mutual_inductive_gen (Global.env()) ~template udecl ([],paramsl,indl) notations cum poly prv finite (* Very syntactical equality *) let eq_local_binders bl1 bl2 = @@ -500,8 +498,8 @@ let extract_params indl = params let extract_inductive indl = - List.map (fun (({CAst.v=indname},pl),_,ar,lc) -> { - ind_name = indname; ind_univs = pl; + List.map (fun ({CAst.v=indname},_,ar,lc) -> { + ind_name = indname; ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (Glob_term.GType [])) ar; ind_lc = List.map (fun (_,({CAst.v=id},t)) -> (id,t)) lc }) indl @@ -567,11 +565,11 @@ type uniform_inductive_flag = | UniformParameters | NonUniformParameters -let do_mutual_inductive ~template indl cum poly prv ~uniform finite = +let do_mutual_inductive ~template udecl indl cum poly prv ~uniform finite = let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in (* Interpret the types *) let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in - let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template indl ntns cum poly prv finite in + let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns cum poly prv finite in (* Declare the mutual inductive block with its associated schemes *) ignore (declare_mutual_inductive_with_eliminations mie pl impls); (* Declare the possible notations of inductive types *) diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 8a2c9b8719..f23085a538 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -24,7 +24,8 @@ type uniform_inductive_flag = | NonUniformParameters val do_mutual_inductive : - template:bool option -> (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag -> + template:bool option -> universe_decl_expr option -> + (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag -> polymorphic -> private_flag -> uniform:uniform_inductive_flag -> Declarations.recursivity_kind -> unit @@ -54,7 +55,6 @@ val should_auto_template : unit -> bool type structured_one_inductive_expr = { ind_name : Id.t; - ind_univs : universe_decl_expr option; ind_arity : constr_expr; ind_lc : (Id.t * constr_expr) list } @@ -69,6 +69,7 @@ val extract_mutual_inductive_declaration_components : (** Typing mutual inductive definitions *) val interp_mutual_inductive : - template:bool option -> structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag -> + template:bool option -> universe_decl_expr option -> structured_inductive_expr -> + decl_notation list -> cumulative_inductive_flag -> polymorphic -> private_flag -> Declarations.recursivity_kind -> mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 44c0159d1b..650b28ea67 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -212,8 +212,10 @@ GRAMMAR EXTEND Gram | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> { VernacScheme l } | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; l = LIST1 identref SEP "," -> { VernacCombinedScheme (id, l) } - | IDENT "Register"; IDENT "Inline"; id = identref -> - { VernacRegister(id, RegisterInline) } + | IDENT "Register"; g = global; "as"; quid = qualid -> + { VernacRegister(g, RegisterRetroknowledge quid) } + | IDENT "Register"; IDENT "Inline"; g = global -> + { VernacRegister(g, RegisterInline) } | IDENT "Universe"; l = LIST1 identref -> { VernacUniverse l } | IDENT "Universes"; l = LIST1 identref -> { VernacUniverse l } | IDENT "Constraint"; l = LIST1 univ_constraint SEP "," -> { VernacConstraint l } diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 63e9e4fe49..e15e57a003 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1161,7 +1161,11 @@ open Pputils | VernacRegister (id, RegisterInline) -> return ( hov 2 - (keyword "Register Inline" ++ spc() ++ pr_lident id) + (keyword "Register Inline" ++ spc() ++ pr_qualid id) + ) + | VernacRegister (id, RegisterRetroknowledge n) -> + return ( + hov 2 (keyword "Register" ++ spc () ++ pr_qualid id ++ spc () ++ keyword "as" ++ pr_qualid n) ) | VernacComments l -> return ( diff --git a/vernac/record.ml b/vernac/record.ml index d36586d062..724b6e62fe 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -487,10 +487,11 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari let cst = Declare.declare_constant id (DefinitionEntry class_entry, IsDefinition Definition) in - let cstu = (cst, match univs with - | Polymorphic_const_entry univs -> Univ.UContext.instance univs - | Monomorphic_const_entry _ -> Univ.Instance.empty) + let inst, univs = match univs with + | Polymorphic_const_entry uctx -> Univ.UContext.instance uctx, univs + | Monomorphic_const_entry _ -> Univ.Instance.empty, Monomorphic_const_entry Univ.ContextSet.empty in + let cstu = (cst, inst) in let inst_type = appvectc (mkConstU cstu) (Termops.rel_vect 0 (List.length params)) in let proj_type = @@ -627,7 +628,7 @@ let check_unique_names records = | Vernacexpr.DefExpr ({CAst.v=Name id},_,_) -> id::acc | _ -> acc in let allnames = - List.fold_left (fun acc (_, id, _, _, cfs, _, _) -> + List.fold_left (fun acc (_, id, _, cfs, _, _) -> id.CAst.v :: (List.fold_left extract_name acc cfs)) [] records in match List.duplicates Id.equal allnames with @@ -636,19 +637,19 @@ let check_unique_names records = let check_priorities kind records = let isnot_class = match kind with Class false -> false | _ -> true in - let has_priority (_, _, _, _, cfs, _, _) = + let has_priority (_, _, _, cfs, _, _) = List.exists (fun ((_, pri), _) -> not (Option.is_empty pri)) cfs in if isnot_class && List.exists has_priority records then user_err Pp.(str "Priorities only allowed for type class substructures") let extract_record_data records = - let map (is_coe, id, _, _, cfs, idbuild, s) = + let map (is_coe, id, _, cfs, idbuild, s) = let fs = List.map (fun (((_, f), _), _) -> f) cfs in id.CAst.v, s, List.map snd cfs, fs in let data = List.map map records in - let pss = List.map (fun (_, _, _, ps, _, _, _) -> ps) records in + let pss = List.map (fun (_, _, ps, _, _, _) -> ps) records in let ps = match pss with | [] -> CErrors.anomaly (str "Empty record block") | ps :: rem -> @@ -660,30 +661,28 @@ let extract_record_data records = in ps in - (** FIXME: Same issue as #7754 *) - let _, _, pl, _, _, _, _ = List.hd records in - pl, ps, data + ps, data (* [fs] corresponds to fields and [ps] to parameters; [coers] is a list telling if the corresponding fields must me declared as coercions or subinstances. *) -let definition_structure kind ~template cum poly finite records = +let definition_structure udecl kind ~template cum poly finite records = let () = check_unique_names records in let () = check_priorities kind records in - let pl, ps, data = extract_record_data records in - let pl, univs, auto_template, params, implpars, data = + let ps, data = extract_record_data records in + let ubinders, univs, auto_template, params, implpars, data = States.with_state_protection (fun () -> - typecheck_params_and_fields finite (kind = Class true) poly pl ps data) () in + typecheck_params_and_fields finite (kind = Class true) poly udecl ps data) () in let template = template, auto_template in match kind with | Class def -> - let (_, id, _, _, cfs, idbuild, _), (arity, implfs, fields) = match records, data with + let (_, id, _, cfs, idbuild, _), (arity, implfs, fields) = match records, data with | [r], [d] -> r, d | _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled") in let priorities = List.map (fun ((_, id), _) -> {hint_priority = id; hint_pattern = None}) cfs in let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in - declare_class finite def cum pl univs id.CAst.v idbuild + declare_class finite def cum ubinders univs id.CAst.v idbuild implpars params arity template implfs fields coers priorities | _ -> let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in @@ -698,11 +697,11 @@ let definition_structure kind ~template cum poly finite records = | Monomorphic_const_entry univs -> Monomorphic_ind_entry univs in - let map (arity, implfs, fields) (is_coe, id, _, _, cfs, idbuild, _) = + let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) = let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in let coe = List.map (fun coe -> not (Option.is_empty coe)) coers in id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe in let data = List.map2 map data records in - let inds = declare_structure finite pl univs implpars params template data in + let inds = declare_structure finite ubinders univs implpars params template data in List.map (fun ind -> IndRef ind) inds diff --git a/vernac/record.mli b/vernac/record.mli index 055a17895a..953d5ec3b6 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -26,12 +26,11 @@ val declare_projections : (Name.t * bool) list * Constant.t option list val definition_structure : - inductive_kind -> template:bool option -> + universe_decl_expr option -> inductive_kind -> template:bool option -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic -> Declarations.recursivity_kind -> (coercion_flag * Names.lident * - universe_decl_expr option * local_binder_expr list * (local_decl_expr with_instance with_priority with_notation) list * Id.t * constr_expr option) list -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e6b3721134..015d5fabef 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -555,9 +555,9 @@ let should_treat_as_uniform () = then ComInductive.UniformParameters else ComInductive.NonUniformParameters -let vernac_record ~template cum k poly finite records = +let vernac_record ~template udecl cum k poly finite records = let is_cumulative = should_treat_as_cumulative cum poly in - let map ((coe, (id, pl)), binders, sort, nameopt, cfs) = + let map ((coe, id), binders, sort, nameopt, cfs) = let const = match nameopt with | None -> add_prefix "Build_" id.v | Some lid -> @@ -574,10 +574,22 @@ let vernac_record ~template cum k poly finite records = in List.iter iter cfs in - coe, id, pl, binders, cfs, const, sort + coe, id, binders, cfs, const, sort in let records = List.map map records in - ignore(Record.definition_structure ~template k is_cumulative poly finite records) + ignore(Record.definition_structure ~template udecl k is_cumulative poly finite records) + +let extract_inductive_udecl (indl:(inductive_expr * decl_notation list) list) = + match indl with + | [] -> assert false + | (((coe,(id,udecl)),b,c,k,d),e) :: rest -> + let rest = List.map (fun (((coe,(id,udecl)),b,c,k,d),e) -> + if Option.has_some udecl + then user_err ~hdr:"inductive udecl" Pp.(strbrk "Universe binders must be on the first inductive of the block.") + else (((coe,id),b,c,k,d),e)) + rest + in + udecl, (((coe,id),b,c,k,d),e) :: rest (** When [poly] is true the type is declared polymorphic. When [lo] is true, then the type is declared private (as per the [Private] keyword). [finite] @@ -585,8 +597,9 @@ let vernac_record ~template cum k poly finite records = neither. *) let vernac_inductive ~atts cum lo finite indl = let open Pp in + let udecl, indl = extract_inductive_udecl indl in if Dumpglob.dump () then - List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) -> + List.iter (fun (((coe,lid), _, _, _, cstrs), _) -> match cstrs with | Constructors cstrs -> Dumpglob.dump_definition lid false "ind"; @@ -594,6 +607,7 @@ let vernac_inductive ~atts cum lo finite indl = Dumpglob.dump_definition lid false "constr") cstrs | _ -> () (* dumping is done by vernac_record (called below) *) ) indl; + let is_record = function | ((_ , _ , _ , _, RecordDecl _), _) -> true | _ -> false @@ -613,7 +627,7 @@ let vernac_inductive ~atts cum lo finite indl = let (coe, (lid, ce)) = l in let coe' = if coe then Some true else None in let f = (((coe', AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce)), None), []) in - vernac_record ~template cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]] + vernac_record ~template udecl cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]] else if List.for_all is_record indl then (** Mutual record case *) let check_kind ((_, _, _, kind, _), _) = match kind with @@ -636,7 +650,7 @@ let vernac_inductive ~atts cum lo finite indl = let ((_, _, _, kind, _), _) = List.hd indl in let kind = match kind with Class _ -> Class false | _ -> kind in let recordl = List.map unpack indl in - vernac_record ~template cum kind atts.polymorphic finite recordl + vernac_record ~template udecl cum kind atts.polymorphic finite recordl else if List.for_all is_constructor indl then (** Mutual inductive case *) let check_kind ((_, _, _, kind, _), _) = match kind with @@ -662,7 +676,7 @@ let vernac_inductive ~atts cum lo finite indl = let indl = List.map unpack indl in let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in let uniform = should_treat_as_uniform () in - ComInductive.do_mutual_inductive ~template indl is_cumulative atts.polymorphic lo ~uniform finite + ComInductive.do_mutual_inductive ~template udecl indl is_cumulative atts.polymorphic lo ~uniform finite else user_err (str "Mixed record-inductive definitions are not allowed") (* @@ -1950,14 +1964,23 @@ let vernac_locate = function | LocateOther (s, qid) -> print_located_other s qid | LocateFile f -> locate_file f -let vernac_register id r = +let vernac_register qid r = + let gr = Smartlocate.global_with_alias qid in if Proof_global.there_are_pending_proofs () then user_err Pp.(str "Cannot register a primitive while in proof editing mode."); - let kn = Constrintern.global_reference id.v in - if not (isConstRef kn) then - user_err Pp.(str "Register inline: a constant is expected"); match r with - | RegisterInline -> Global.register_inline (destConstRef kn) + | RegisterInline -> + if not (isConstRef gr) then + user_err Pp.(str "Register inline: a constant is expected"); + Global.register_inline (destConstRef gr) + | RegisterRetroknowledge n -> + let path, id = Libnames.repr_qualid n in + if DirPath.equal path Retroknowledge.int31_path + then + let f = Retroknowledge.(KInt31 (int31_field_of_string (Id.to_string id))) in + Global.register f gr + else + user_err Pp.(str "Register in unknown namespace: " ++ str (DirPath.to_string path)) (********************) (* Proof management *) diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 11b2a7d802..0c0204a728 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -202,7 +202,7 @@ type inductive_expr = constructor_list_or_record_decl_expr type one_inductive_expr = - ident_decl * local_binder_expr list * constr_expr option * constructor_expr list + lident * local_binder_expr list * constr_expr option * constructor_expr list type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr and typeclass_context = typeclass_constraint list @@ -278,6 +278,7 @@ type extend_name = It will be extended with primitive inductive types and operators *) type register_kind = | RegisterInline + | RegisterRetroknowledge of qualid type bullet = Proof_bullet.t [@@ocaml.deprecated "Alias type, please use [Proof_bullet.t]"] @@ -438,7 +439,7 @@ type nonrec vernac_expr = | VernacPrint of printable | VernacSearch of searchable * Goal_select.t option * search_restriction | VernacLocate of locatable - | VernacRegister of lident * register_kind + | VernacRegister of qualid * register_kind | VernacComments of comment list (* Proof management *) |