diff options
68 files changed, 657 insertions, 445 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 5aa0fee16f..5e6c380f4b 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -18,7 +18,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2019-03-14-V14" + CACHEKEY: "bionic_coq-V2020-03-19-V93" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" diff --git a/INSTALL.md b/INSTALL.md index a55e1e9ac2..0c98a611a5 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -7,7 +7,7 @@ Build Requirements To compile Coq yourself, you need: - [OCaml](https://ocaml.org/) (version >= 4.05.0) - (This version of Coq has been tested up to OCaml 4.09.0) + (This version of Coq has been tested up to OCaml 4.09.1) - The [num](https://github.com/ocaml/num) library; note that it is included in the OCaml distribution for OCaml versions < 4.06.0 @@ -45,7 +45,7 @@ CoqIDE with: Opam (https://opam.ocaml.org/) is recommended to install OCaml and the corresponding packages. - $ opam switch create coq 4.09.0+flambda + $ opam switch create coq 4.09.1+flambda $ eval $(opam env) $ opam install num ocamlfind lablgtk3-sourceview3 diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 98e17e8fe8..aae2c3cb42 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -72,7 +72,7 @@ jobs: opam list displayName: 'Install OCaml dependencies' env: - COMPILER: "4.09.0" + COMPILER: "4.09.1" FINDLIB_VER: ".1.8.1" OPAMYES: "true" diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh index ee6c62673b..7b3e2703b8 100755 --- a/dev/ci/azure-opam.sh +++ b/dev/ci/azure-opam.sh @@ -2,7 +2,7 @@ set -e -x -OPAM_VARIANT=ocaml-variants.4.09.0+mingw64c +OPAM_VARIANT=ocaml-variants.4.09.1+mingw64c wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz tar -xf opam64.tar.xz diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 979b5917d4..e14f634073 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2019-03-14-V14" +# CACHEKEY: "bionic_coq-V2020-03-19-V93" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -18,7 +18,7 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ texlive-science tipa # More dependencies of the sphinx doc -RUN pip3 install sphinx==1.7.8 sphinx_rtd_theme==0.2.5b2 \ +RUN pip3 install sphinx==1.8.0 sphinx_rtd_theme==0.2.5b2 \ antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0 # We need to install OPAM 2.0 manually for now. @@ -56,7 +56,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ opam install $BASE_OPAM # EDGE switch -ENV COMPILER_EDGE="4.09.0" \ +ENV COMPILER_EDGE="4.09.1" \ BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.12" # EDGE+flambda switch, we install CI_OPAM as to be able to use diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all index 49e338d0a5..556493ffad 100644 --- a/dev/dune-workspace.all +++ b/dev/dune-workspace.all @@ -3,5 +3,5 @@ ; Add custom flags here. Default developer profile is `dev` (context (opam (switch 4.05.0))) (context (opam (switch 4.05.0+32bit))) -(context (opam (switch 4.09.0))) -(context (opam (switch 4.09.0+flambda))) +(context (opam (switch 4.09.1))) +(context (opam (switch 4.09.1+flambda))) diff --git a/dev/top_printers.ml b/dev/top_printers.ml index ebe704b88a..96dbf9142b 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -82,7 +82,7 @@ let ppsconstr x = ppconstr (Mod_subst.force_constr x) let ppconstr_univ x = Constrextern.with_universes ppconstr x let ppglob_constr = (fun x -> pp(pr_lglob_constr_env (Global.env()) x)) let pppattern = (fun x -> pp(envpp pr_constr_pattern_env x)) -let pptype = (fun x -> try pp(envpp pr_ltype_env x) with e -> pp (str (Printexc.to_string e))) +let pptype = (fun x -> try pp(envpp (fun env evm t -> pr_ltype_env env evm t) x) with e -> pp (str (Printexc.to_string e))) let ppfconstr c = ppconstr (CClosure.term_of_fconstr c) let ppbigint n = pp (str (Bigint.to_string n));; diff --git a/doc/README.md b/doc/README.md index 7fa6f5cf3d..e749bcf5d1 100644 --- a/doc/README.md +++ b/doc/README.md @@ -30,7 +30,7 @@ To produce the complete documentation in HTML, you will need Coq dependencies listed in [`INSTALL.md`](../INSTALL.md). Additionally, the Sphinx-based reference manual requires Python 3, and the following Python packages: - - sphinx >= 1.7.8 + - sphinx >= 1.8.0 - sphinx_rtd_theme >= 0.2.5b2 - beautifulsoup4 >= 4.0.6 - antlr4-python3-runtime >= 4.7.1 diff --git a/doc/changelog/04-tactics/11760-firstorder-leaf.rst b/doc/changelog/04-tactics/11760-firstorder-leaf.rst new file mode 100644 index 0000000000..e6e4b827e5 --- /dev/null +++ b/doc/changelog/04-tactics/11760-firstorder-leaf.rst @@ -0,0 +1,9 @@ +- **Changed:** + The default tactic used by :g:`firstorder` is + :g:`auto with core` instead of :g:`auto with *`; + see :ref:`decisionprocedures` for details; + old behavior can be reset by using the `-compat 8.12` command-line flag; + to ease the migration of legacy code, the default solver can be set to `debug auto with *` + with `Set Firstorder Solver debug auto with *` + (`#11760 <https://github.com/coq/coq/pull/11760>`_, + by Vincent Laporte). diff --git a/doc/changelog/07-commands-and-options/11795-print_implicit_args.rst b/doc/changelog/07-commands-and-options/11795-print_implicit_args.rst new file mode 100644 index 0000000000..5b0cdb5914 --- /dev/null +++ b/doc/changelog/07-commands-and-options/11795-print_implicit_args.rst @@ -0,0 +1,5 @@ +- **Added:** + Several commands (`Search`, `About`, ...) now print the implicit arguments + in brackets when printing types. + (`#11795 <https://github.com/coq/coq/pull/11795>`_, + by SimonBoulier). diff --git a/doc/changelog/11-infrastructure-and-dependencies/11860-ci+ocaml_to_4091.rst b/doc/changelog/11-infrastructure-and-dependencies/11860-ci+ocaml_to_4091.rst new file mode 100644 index 0000000000..94e2c34828 --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/11860-ci+ocaml_to_4091.rst @@ -0,0 +1,4 @@ +- **Added:** + Bump official OCaml support to 4.09.1 + (`#11860 <https://github.com/coq/coq/pull/11860>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index d909f98956..41b726b069 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -1,7 +1,7 @@ .. _extraction: -Extraction of programs in |OCaml| and Haskell -============================================= +Program extraction +================== :Authors: Jean-Christophe Filliâtre and Pierre Letouzey diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index db8c09d88f..0e8660cb0e 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -1,10 +1,5 @@ -.. _miscellaneousextensions: - -Miscellaneous extensions -======================== - Program derivation ------------------- +================== |Coq| comes with an extension called ``Derive``, which supports program derivation. Typically in the style of Bird and Meertens or derivations diff --git a/doc/sphinx/appendix/history-and-changes/index.rst b/doc/sphinx/appendix/history-and-changes/index.rst new file mode 100644 index 0000000000..50ffec8e3f --- /dev/null +++ b/doc/sphinx/appendix/history-and-changes/index.rst @@ -0,0 +1,21 @@ +.. _history-and-changes: + +========================== +History and recent changes +========================== + +This chapter is divided in two parts. The first one is about the +:ref:`early history of Coq <history>` and is presented in +chronological order. The second one provides :ref:`release notes +about recent versions of Coq <changes>` and is presented in reverse +chronological order. When updating your copy of Coq to a new version +(especially a new major version), it is strongly recommended that you +read the corresponding release notes. They may contain advice that +will help you understand the differences with the previous version and +upgrade your projects. + +.. toctree:: + :maxdepth: 1 + + ../../history + ../../changes diff --git a/doc/sphinx/appendix/indexes/index.rst b/doc/sphinx/appendix/indexes/index.rst new file mode 100644 index 0000000000..a5032ff822 --- /dev/null +++ b/doc/sphinx/appendix/indexes/index.rst @@ -0,0 +1,24 @@ +:orphan: + +.. _indexes: + +======== +Indexes +======== + +We provide various specialized indexes that are helpful to quickly +find what you are looking for. + +.. toctree:: + + ../../genindex + ../../coq-cmdindex + ../../coq-tacindex + ../../coq-optindex + ../../coq-exnindex + +For reference, here are direct links to the documentation of: + +- :ref:`flags, options and tables <flags-options-tables>`; +- controlling the display of warning messages with the :opt:`Warnings` + option. diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 6d9979a704..afe22d24e5 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -1,3 +1,5 @@ +.. _changes: + -------------- Recent changes -------------- diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 98272810f6..3d77d07061 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -46,7 +46,7 @@ with open("refman-preamble.rst") as s: # -- General configuration ------------------------------------------------ # If your documentation needs a minimal Sphinx version, state it here. -needs_sphinx = '1.7.8' +needs_sphinx = '1.8.0' # Add any Sphinx extension module names here, as strings. They can be # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom diff --git a/doc/sphinx/genindex.rst b/doc/sphinx/genindex.rst index 29f792b3aa..e3a27fd7c4 100644 --- a/doc/sphinx/genindex.rst +++ b/doc/sphinx/genindex.rst @@ -2,6 +2,6 @@ .. hack to get index in TOC ------ -Index ------ +------------- +General index +------------- diff --git a/doc/sphinx/history.rst b/doc/sphinx/history.rst index c4a48d6985..153dc1f368 100644 --- a/doc/sphinx/history.rst +++ b/doc/sphinx/history.rst @@ -1,3 +1,5 @@ +.. _history: + -------------------- Early history of Coq -------------------- diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst index 0a20d1c47b..6069ed42fe 100644 --- a/doc/sphinx/index.html.rst +++ b/doc/sphinx/index.html.rst @@ -8,84 +8,37 @@ Contents -------- .. toctree:: - :caption: Indexes - - genindex - coq-cmdindex - coq-tacindex - coq-optindex - coq-exnindex - -.. No entries yet - * :index:`thmindex` - -.. toctree:: - :caption: Preamble self - history - changes .. toctree:: - :caption: The language + :caption: Specification language - language/gallina-specification-language - language/gallina-extensions - language/coq-library - language/cic - language/module-system + language/core/index + language/extensions/index .. toctree:: - :caption: The proof engine + :caption: Proofs - proof-engine/vernacular-commands - proof-engine/proof-handling - proof-engine/tactics - proof-engine/ltac - proof-engine/ltac2 - proof-engine/detailed-tactic-examples - proof-engine/ssreflect-proof-language + proofs/writing-proofs/index + proofs/automatic-tactics/index + proofs/creating-tactics/index .. toctree:: - :caption: User extensions + :caption: Using Coq - user-extensions/syntax-extensions - user-extensions/proof-schemes + using/libraries/index + using/tools/index .. toctree:: - :caption: Practical tools + :caption: Appendix - practical-tools/coq-commands - practical-tools/utilities - practical-tools/coqide - -.. toctree:: - :caption: Addendum - - 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 - addendum/sprop + appendix/history-and-changes/index + appendix/indexes/index + zebibliography -.. toctree:: - :caption: Reference +.. No entries yet + * :index:`thmindex` - zebibliography .. include:: license.rst - -.. [#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). diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst index 5562736997..62d9525194 100644 --- a/doc/sphinx/index.latex.rst +++ b/doc/sphinx/index.latex.rst @@ -10,81 +10,39 @@ Introduction .. include:: license.rst -.. [#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:: history.rst - -.. include:: changes.rst - ------------- -The language ------------- +---------------------- +Specification language +---------------------- .. toctree:: - language/gallina-specification-language - language/gallina-extensions - language/coq-library - language/cic - language/module-system + language/core/index + language/extensions/index ----------------- -The proof engine ----------------- +------ +Proofs +------ .. toctree:: - proof-engine/vernacular-commands - proof-engine/proof-handling - proof-engine/tactics - proof-engine/ltac - proof-engine/ltac2 - proof-engine/detailed-tactic-examples - proof-engine/ssreflect-proof-language + proofs/writing-proofs/index + proofs/automatic-tactics/index + proofs/creating-tactics/index ---------------- -User extensions ---------------- +--------- +Using Coq +--------- .. toctree:: - user-extensions/syntax-extensions - user-extensions/proof-schemes - ---------------- -Practical tools ---------------- - -.. toctree:: - - practical-tools/coq-commands - practical-tools/utilities - practical-tools/coqide + using/libraries/index + using/tools/index -------- -Addendum +Appendix -------- .. 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 - addendum/sprop - -.. toctree:: + appendix/history-and-changes/index zebibliography diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index 1424b4f3e1..b059fb4069 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -1,107 +1,68 @@ -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 -https://coq.inria.fr/documentation and -https://github.com/coq/coq/wiki#coq-tutorials - -The |Coq| system is designed to develop mathematical proofs, and -especially to write formal specifications, programs and to verify that -programs are correct with respect to their specifications. It provides a -specification language named |Gallina|. Terms of |Gallina| can represent -programs as well as properties of these programs and proofs of these -properties. Using the so-called *Curry-Howard isomorphism*, programs, -properties and proofs are formalized in the same language called -*Calculus of Inductive Constructions*, that is a -:math:`\lambda`-calculus with a rich type system. All logical judgments -in |Coq| are typing judgments. The very heart of the |Coq| system is the -type checking algorithm that checks the correctness of proofs, in other -words that checks that a program complies to its specification. |Coq| also -provides an interactive proof assistant to build proofs using specific -programs called *tactics*. - -All services of the |Coq| proof assistant are accessible by interpretation -of a command language called *the vernacular*. - -Coq has an interactive mode in which commands are interpreted as the -user types them in from the keyboard and a compiled mode where commands -are processed from a file. - -- In interactive mode, users can develop their theories and proofs step by - step, and query the system for available theorems and definitions. The - interactive mode is generally run with the help of an IDE, such - as CoqIDE, documented in :ref:`coqintegrateddevelopmentenvironment`, - Emacs with Proof-General :cite:`Asp00` [#PG]_, - or jsCoq to run Coq in your browser (see https://github.com/ejgallego/jscoq). - The `coqtop` read-eval-print-loop can also be used directly, for debugging - purposes. - -- 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 - representation of its input. The compiled mode is run with the `coqc` - command. - -.. seealso:: :ref:`thecoqcommands`. - -How to read this book ---------------------- - -This is a Reference Manual, so it is not intended for continuous reading. -We recommend using the various indexes to quickly locate the documentation -you are looking for. There is a global index, and a number of specific indexes -for tactics, vernacular commands, and error messages and warnings. -Nonetheless, the manual has some structure that is explained below. - -- The first part describes the specification language, |Gallina|. - Chapters :ref:`gallinaspecificationlanguage` and :ref:`extensionsofgallina` describe the concrete - syntax as well as the meaning of programs, theorems and proofs in the - Calculus of Inductive Constructions. Chapter :ref:`thecoqlibrary` describes the - standard library of |Coq|. Chapter :ref:`calculusofinductiveconstructions` is a mathematical description - of the formalism. Chapter :ref:`themodulesystem` describes the module - system. - -- The second part describes the proof engine. It is divided into several - chapters. Chapter :ref:`vernacularcommands` presents all commands (we - call them *vernacular commands*) that are not directly related to - interactive proving: requests to the environment, complete or partial - evaluation, loading and compiling files. How to start and stop - proofs, do multiple proofs in parallel is explained in - Chapter :ref:`proofhandling`. In Chapter :ref:`tactics`, all commands that - realize one or more steps of the proof are presented: we call them - *tactics*. The legacy language to combine these tactics into complex proof - strategies is given in Chapter :ref:`ltac`. The currently experimental - language that will eventually replace Ltac is presented in - Chapter :ref:`ltac2`. Examples of tactics - are described in Chapter :ref:`detailedexamplesoftactics`. - Finally, the |SSR| proof language is presented in - Chapter :ref:`thessreflectprooflanguage`. - -- The third part describes how to extend the syntax of |Coq| in - Chapter :ref:`syntaxextensionsandinterpretationscopes` and how to define - new induction principles in Chapter :ref:`proofschemes`. - -- In the fourth part more practical tools are documented. First in - Chapter :ref:`thecoqcommands`, the usage of `coqc` (batch mode) and - `coqtop` (interactive mode) with their options is described. Then, - in Chapter :ref:`utilities`, various utilities that come with the - |Coq| distribution are presented. Finally, Chapter :ref:`coqintegrateddevelopmentenvironment` - describes CoqIDE. - -- The fifth part documents a number of advanced features, including coercions, - canonical structures, typeclasses, program extraction, and specialized - solvers and tactics. See the table of contents for a complete list. - -List of additional documentation --------------------------------- - -This manual does not contain all the documentation the user may need -about |Coq|. Various informations can be found in the following documents: - -Installation - A text file `INSTALL` that comes with the sources explains how to - install |Coq|. - -The |Coq| standard library - A commented version of sources of the |Coq| standard library - (including only the specifications, the proofs are removed) is - available at https://coq.inria.fr/stdlib/. +This is the reference manual of |Coq|. Coq is an interactive theorem +prover. It lets you formalize mathematical concepts and then helps +you interactively generate machine-checked proofs of theorems. +Machine checking gives users much more confidence that the proofs are +correct compared to human-generated and -checked proofs. Coq has been +used in a number of flagship verification projects, including the +`CompCert verified C compiler <http://compcert.inria.fr/>`_, and has +served to verify the proof of the `four color theorem +<https://github.com/math-comp/fourcolor>`_ (among many other +mathematical formalizations). + +Users generate proofs by entering a series of tactics that constitute +steps in the proof. There are many built-in tactics, some of which +are elementary, while others implement complex decision procedures +(such as :tacn:`lia`, a decision procedure for linear integer +arithmetic). :ref:`Ltac <ltac>` and its planned replacement, +:ref:`Ltac2 <ltac2>`, provide languages to define new tactics by +combining existing tactics with looping and conditional constructs. +These permit automation of large parts of proofs and sometimes entire +proofs. Furthermore, users can add novel tactics or functionality by +creating Coq plugins using OCaml. + +The Coq kernel, a small part of Coq, does the final verification that +the tactic-generated proof is valid. Usually the tactic-generated +proof is indeed correct, but delegating proof verification to the +kernel means that even if a tactic is buggy, it won't be able to +introduce an incorrect proof into the system. + +Finally, Coq also supports extraction of verified programs to +programming languages such as OCaml and Haskell. This provides a way +of executing Coq code efficiently and can be used to create verified +software libraries. + +To learn Coq, beginners are advised to first start with a tutorial / +book. Several such tutorials / books are listed at +https://coq.inria.fr/documentation. + +This manual is organized in three main parts, plus an appendix: + +- **The first part presents the specification language of Coq**, that + allows to define programs and state mathematical theorems. + :ref:`core-language` presents the language that the kernel of Coq + understands. :ref:`extensions` presents the richer language, with + notations, implicits, etc. that a user can use and which is + translated down to the language of the kernel by means of an + "elaboration process". + +- **The second part presents the interactive proof mode**, the central + feature of Coq. :ref:`writing-proofs` introduces this interactive + proof mode and the available proof languages. + :ref:`automatic-tactics` presents some more advanced tactics, while + :ref:`writing-tactics` is about the languages that allow a user to + combine tactics together and develop new ones. + +- **The third part shows how to use Coq in practice.** + :ref:`libraries` presents some of the essential reusable blocks from + the ecosystem and some particularly important extensions such as the + program extraction mechanism. :ref:`tools` documents important + tools that a user needs to build a Coq project. + +- In the appendix, :ref:`history-and-changes` presents the history of + Coq and changes in recent releases. This is an important reference + if you upgrade the version of Coq that you use. The various + :ref:`indexes <indexes>` are very useful to **quickly browse the + manual and find what you are looking for.** They are often the main + entry point to the manual. + +The full table of contents is presented below: diff --git a/doc/sphinx/language/core/index.rst b/doc/sphinx/language/core/index.rst new file mode 100644 index 0000000000..07dcfff444 --- /dev/null +++ b/doc/sphinx/language/core/index.rst @@ -0,0 +1,37 @@ +.. _core-language: + +============= +Core language +============= + +At the heart of the Coq proof assistant is the Coq kernel. While +users have access to a language with many convenient features such as +notations, implicit arguments, etc. (that are presented in the +:ref:`next chapter <extensions>`), such complex terms get translated +down to a core language (the Calculus of Inductive Constructions) that +the kernel understands, and which we present here. Furthermore, while +users can build proofs interactively using tactics (see Chapter +:ref:`writing-proofs`), the role of these tactics is to incrementally +build a "proof term" which the kernel will verify. More precisely, a +proof term is a term of the Calculus of Inductive Constructions whose +type corresponds to a theorem statement. The kernel is a type checker +which verifies that terms have their expected type. + +This separation between the kernel on the one hand and the elaboration +engine and tactics on the other hand follows what is known as the "de +Bruijn criterion" (keeping a small and well delimited trusted code +base within a proof assistant which can be much more complex). This +separation makes it possible to reduce the trust in the whole system +to trusting a smaller, critical component: the kernel. In particular, +users may rely on external plugins that provide advanced and complex +tactics without fear of these tactics being buggy, because the kernel +will have to check their output. + +.. toctree:: + :maxdepth: 1 + + ../gallina-specification-language + ../cic + ../../addendum/universe-polymorphism + ../../addendum/sprop + ../module-system diff --git a/doc/sphinx/language/extensions/index.rst b/doc/sphinx/language/extensions/index.rst new file mode 100644 index 0000000000..f22927d627 --- /dev/null +++ b/doc/sphinx/language/extensions/index.rst @@ -0,0 +1,26 @@ +.. _extensions: + +=================== +Language extensions +=================== + +Elaboration extends the language accepted by the Coq kernel to make it +easier to use. For example, this lets the user omit most type +annotations because they can be inferred, call functions with implicit +arguments which will be inferred as well, extend the syntax with +notations, factorize branches when pattern-matching, etc. In this +chapter, we present these language extensions and we give some +explanations on how this language is translated down to the core +language presented in the :ref:`previous chapter <core-language>`. + +.. toctree:: + :maxdepth: 1 + + ../gallina-extensions + ../../addendum/extended-pattern-matching + ../../user-extensions/syntax-extensions + ../../addendum/implicit-coercions + ../../addendum/type-classes + ../../addendum/canonical-structures + ../../addendum/program + ../../proof-engine/vernacular-commands diff --git a/doc/sphinx/license.rst b/doc/sphinx/license.rst index 55c6d988f0..35837f8407 100644 --- a/doc/sphinx/license.rst +++ b/doc/sphinx/license.rst @@ -1,7 +1,7 @@ -License -------- +.. note:: **License** -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. + 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/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index be185e885b..d498c1ee2c 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -4286,7 +4286,7 @@ some incompatibilities. :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. + :g:`auto with core`, it can be reset locally or globally using this option. .. cmd:: Print Firstorder Solver diff --git a/doc/sphinx/proofs/automatic-tactics/index.rst b/doc/sphinx/proofs/automatic-tactics/index.rst new file mode 100644 index 0000000000..a219770c69 --- /dev/null +++ b/doc/sphinx/proofs/automatic-tactics/index.rst @@ -0,0 +1,20 @@ +.. _automatic-tactics: + +===================================================== +Built-in decision procedures and programmable tactics +===================================================== + +Some tactics are largely automated and are able to solve complex +goals. This chapter presents both some decision procedures that can +be used to solve some specific categories of goals, and some +programmable tactics, that the user can instrument to handle some +complex goals in new domains. + +.. toctree:: + :maxdepth: 1 + + ../../addendum/omega + ../../addendum/micromega + ../../addendum/ring + ../../addendum/nsatz + ../../addendum/generalized-rewriting diff --git a/doc/sphinx/proofs/creating-tactics/index.rst b/doc/sphinx/proofs/creating-tactics/index.rst new file mode 100644 index 0000000000..1af1b0b726 --- /dev/null +++ b/doc/sphinx/proofs/creating-tactics/index.rst @@ -0,0 +1,34 @@ +.. _writing-tactics: + +==================== +Creating new tactics +==================== + +The languages presented in this chapter allow one to build complex +tactics by combining existing ones with constructs such as +conditionals and looping. While :ref:`Ltac <ltac>` was initially +thought of as a language for doing some basic combinations, it has +been used successfully to build highly complex tactics as well, but +this has also highlighted its limits and fragility. The experimental +language :ref:`Ltac2 <ltac2>` is a typed and more principled variant +which is more adapted to building complex tactics. + +There are other solutions beyond these two tactic languages to write +new tactics: + +- `Mtac2 <https://github.com/Mtac2/Mtac2>`_ is an external plugin + which provides another typed tactic language. While Ltac2 belongs + to the ML language family, Mtac2 reuses the language of Coq itself + as the language to build Coq tactics. + +- The most traditional way of building new complex tactics is to write + a Coq plugin in OCaml. Beware that this also requires much more + effort and commitment. A tutorial for writing Coq plugins is + available in the Coq repository in `doc/plugin_tutorial + <https://github.com/coq/coq/tree/master/doc/plugin_tutorial>`_. + +.. toctree:: + :maxdepth: 1 + + ../../proof-engine/ltac + ../../proof-engine/ltac2 diff --git a/doc/sphinx/proofs/writing-proofs/index.rst b/doc/sphinx/proofs/writing-proofs/index.rst new file mode 100644 index 0000000000..a279a5957f --- /dev/null +++ b/doc/sphinx/proofs/writing-proofs/index.rst @@ -0,0 +1,34 @@ +.. _writing-proofs: + +============== +Writing proofs +============== + +Coq is an interactive theorem prover, or proof assistant, which means +that proofs can be constructed interactively through a dialog between +the user and the assistant. The building blocks for this dialog are +tactics which the user will use to represent steps in the proof of a +theorem. + +Incomplete proofs have one or more open (unproven) sub-goals. Each +goal has its own context (a set of assumptions that can be used to +prove the goal). Tactics can transform goals and contexts. +Internally, the incomplete proof is represented as a partial proof +term, with holes for the unproven sub-goals. + +When a proof is complete, the user leaves the proof mode and defers +the verification of the resulting proof term to the :ref:`kernel +<core-language>`. + +This chapter is divided in several parts, describing the basic ideas +of the proof mode (during which tactics can be used), and several +flavors of tactics, including the SSReflect proof language. + +.. toctree:: + :maxdepth: 1 + + ../../proof-engine/proof-handling + ../../proof-engine/tactics + ../../proof-engine/ssreflect-proof-language + ../../proof-engine/detailed-tactic-examples + ../../user-extensions/proof-schemes diff --git a/doc/sphinx/using/libraries/index.rst b/doc/sphinx/using/libraries/index.rst new file mode 100644 index 0000000000..d0848e6c3f --- /dev/null +++ b/doc/sphinx/using/libraries/index.rst @@ -0,0 +1,24 @@ +.. _libraries: + +===================== +Libraries and plugins +===================== + +Coq is distributed with a standard library and a set of internal +plugins (most of which provide tactics that have already been +presented in :ref:`writing-proofs`). This chapter presents this +standard library and some of these internal plugins which provide +features that are not tactics. + +In addition, Coq has a rich ecosystem of external libraries and +plugins. These libraries and plugins can be browsed online through +the `Coq Package Index <https://coq.inria.fr/opam/www/>`_ and +installed with the `opam package manager +<https://coq.inria.fr/opam-using.html>`_. + +.. toctree:: + :maxdepth: 1 + + ../../language/coq-library + ../../addendum/extraction + ../../addendum/miscellaneous-extensions diff --git a/doc/sphinx/using/tools/index.rst b/doc/sphinx/using/tools/index.rst new file mode 100644 index 0000000000..4381c4d63d --- /dev/null +++ b/doc/sphinx/using/tools/index.rst @@ -0,0 +1,20 @@ +.. _tools: + +================================ +Command-line and graphical tools +================================ + +This chapter presents the command-line tools that users will need to +build their Coq project, the documentation of the CoqIDE standalone +user interface and the documentation of the parallel proof processing +feature that is supported by CoqIDE and several other user interfaces. +A list of available user interfaces to interact with Coq is available +on the `Coq website <https://coq.inria.fr/user-interfaces.html>`_. + +.. toctree:: + :maxdepth: 1 + + ../../practical-tools/coq-commands + ../../practical-tools/utilities + ../../practical-tools/coqide + ../../addendum/parallel-proof-processing diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index b92c94fe2c..84f32e187b 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -34,7 +34,6 @@ from sphinx.util.logging import getLogger, get_node_location from sphinx.directives import ObjectDescription from sphinx.domains import Domain, ObjType, Index from sphinx.domains.std import token_xrefs -from sphinx.ext import mathbase from . import coqdoc from .repl import ansicolors @@ -74,8 +73,7 @@ def make_target(objtype, targetid): return "coq:{}.{}".format(objtype, targetid) def make_math_node(latex, docname, nowrap): - node = mathbase.displaymath() - node['latex'] = latex + node = nodes.math_block(latex, latex) node['label'] = None # Otherwise equations are numbered node['nowrap'] = nowrap node['docname'] = docname @@ -493,9 +491,7 @@ class ProductionObject(CoqObject): pass def _target_id(self, name): - # Use `name[1]` instead of ``nodes.make_id(name[1])`` to work around - # https://github.com/sphinx-doc/sphinx/issues/4983 - return 'grammar-token-{}'.format(name[1]) + return 'grammar-token-{}'.format(nodes.make_id(name[1])) def _record_name(self, name, targetid): env = self.state.document.settings.env diff --git a/ide/default_bindings_src.ml b/ide/default_bindings_src.ml index 85a635a50f..a69a7c2aba 100644 --- a/ide/default_bindings_src.ml +++ b/ide/default_bindings_src.ml @@ -545,7 +545,7 @@ let bindings_set_1 = [ ["\\Hopf"; "\\quaternions" ], "ℍ", [letter]; ["\\planckh" ], "ℎ", [letter]; ["\\hslash"; "\\plankv" ], "ℏ", [letter]; - ["\\hbar"; "\\planck" ], "ℏ︀", [letter]; + ["\\hbar"; "\\planck" ], "ℏ", [letter]; ["\\Iscr"; "\\imagline" ], "ℐ", [letter]; ["\\Im"; "\\Ifr"; "\\image"; "\\imagpart" ], "ℑ", [letter]; ["\\Lscr"; "\\lagran"; "\\Laplacetrf" ], "ℒ", [letter]; @@ -1108,7 +1108,7 @@ let bindings_set_1 = [ ["\\isins" ], "⋴", [set]; ["\\isindot" ], "⋵", [set]; ["\\notinvc" ], "⋶", [set]; - ["\\notindot" ], "⋶︀", [set]; + ["\\notindot" ], "⋶", [set]; ["\\notinvb" ], "⋷", [set]; ["\\isinE" ], "⋹", [set]; ["\\nisd" ], "⋺", [set]; @@ -1192,40 +1192,40 @@ let bindings_set_1 = [ (* }}} *) (* {{{ Missing font *) - ["\\NegativeThickSpace" ], " ︀", [miscellanea]; - ["\\NegativeThinSpace" ], " ︀", [miscellanea]; - ["\\NegativeVeryThinSpace" ], " ︀", [miscellanea]; - ["\\NegativeMediumSpace" ], " ︀", [miscellanea]; - ["\\slarr"; "\\ShortLeftArrow" ], "←︀", [miscellanea]; - ["\\srarr"; "\\ShortRightArrow" ], "→︀", [miscellanea]; - ["\\empty"; "\\emptyset" ], "∅︀", [miscellanea]; - ["\\ssetmn"; "\\smallsetminus" ], "∖︀", [miscellanea]; - ["\\smid"; "\\shortmid" ], "∣︀", [miscellanea]; - ["\\nsmid"; "\\nshortmid" ], "∤︀", [miscellanea]; - ["\\spar"; "\\parsl"; "\\shortparallel" ], "∥︀", [miscellanea]; - ["\\nparsl" ], "∥︀⃥", [miscellanea]; - ["\\nspar"; "\\nshortparallel" ], "∦︀", [miscellanea]; - ["\\caps" ], "∩︀", [miscellanea]; - ["\\cups" ], "∪︀", [miscellanea]; - ["\\thksim"; "\\thicksim" ], "∼︀", [miscellanea]; - ["\\thkap"; "\\thickapprox" ], "≈︀", [miscellanea]; - ["\\nedot" ], "≠︀", [miscellanea]; + ["\\NegativeThickSpace" ], " ", [miscellanea]; + ["\\NegativeThinSpace" ], " ", [miscellanea]; + ["\\NegativeVeryThinSpace" ], " ", [miscellanea]; + ["\\NegativeMediumSpace" ], " ", [miscellanea]; + ["\\slarr"; "\\ShortLeftArrow" ], "←", [miscellanea]; + ["\\srarr"; "\\ShortRightArrow" ], "→", [miscellanea]; + ["\\empty"; "\\emptyset" ], "∅", [miscellanea]; + ["\\ssetmn"; "\\smallsetminus" ], "∖", [miscellanea]; + ["\\smid"; "\\shortmid" ], "∣", [miscellanea]; + ["\\nsmid"; "\\nshortmid" ], "∤", [miscellanea]; + ["\\spar"; "\\parsl"; "\\shortparallel" ], "∥", [miscellanea]; + ["\\nparsl" ], "∥⃥", [miscellanea]; + ["\\nspar"; "\\nshortparallel" ], "∦", [miscellanea]; + ["\\caps" ], "∩", [miscellanea]; + ["\\cups" ], "∪", [miscellanea]; + ["\\thksim"; "\\thicksim" ], "∼", [miscellanea]; + ["\\thkap"; "\\thickapprox" ], "≈", [miscellanea]; + ["\\nedot" ], "≠", [miscellanea]; ["\\bnequiv" ], "≡⃥", [miscellanea]; - ["\\lvnE"; "\\lvertneqq" ], "≨︀", [miscellanea]; - ["\\gvnE"; "\\gvertneqq" ], "≩︀", [miscellanea]; - ["\\nLtv"; "\\NotLessLess" ], "≪̸︀", [miscellanea]; - ["\\nGtv"; "\\NotGreaterGreater" ], "≫̸︀", [miscellanea]; + ["\\lvnE"; "\\lvertneqq" ], "≨", [miscellanea]; + ["\\gvnE"; "\\gvertneqq" ], "≩", [miscellanea]; + ["\\nLtv"; "\\NotLessLess" ], "≪̸", [miscellanea]; + ["\\nGtv"; "\\NotGreaterGreater" ], "≫̸", [miscellanea]; ["\\nle"; "\\NotLessEqual" ], "≰⃥", [miscellanea]; ["\\nge"; "\\NotGreaterEqual" ], "≱⃥", [miscellanea]; - ["\\vsubnE"; "\\vsubne"; "\\varsubsetneq"; "\\varsubsetneqq" ], "⊊︀", [miscellanea]; - ["\\vsupne"; "\\vsupnE"; "\\varsupsetneq"; "\\varsupsetneqq" ], "⊋︀", [miscellanea]; - ["\\sqcaps" ], "⊓︀", [miscellanea]; - ["\\sqcups" ], "⊔︀", [miscellanea]; + ["\\vsubnE"; "\\vsubne"; "\\varsubsetneq"; "\\varsubsetneqq" ], "⊊", [miscellanea]; + ["\\vsupne"; "\\vsupnE"; "\\varsupsetneq"; "\\varsupsetneqq" ], "⊋", [miscellanea]; + ["\\sqcaps" ], "⊓", [miscellanea]; + ["\\sqcups" ], "⊔", [miscellanea]; ["\\prurel" ], "⊰", [miscellanea]; - ["\\lesg" ], "⋚︀", [miscellanea]; - ["\\gesl" ], "⋛︀", [miscellanea]; - ["\\ShortUpArrow" ], "⌃︀", [miscellanea]; - ["\\ShortDownArrow" ], "⌄︀", [miscellanea]; + ["\\lesg" ], "⋚", [miscellanea]; + ["\\gesl" ], "⋛", [miscellanea]; + ["\\ShortUpArrow" ], "⌃", [miscellanea]; + ["\\ShortDownArrow" ], "⌄", [miscellanea]; ["\\target" ], "⌖", [miscellanea]; ["\\cylcty" ], "⌭", [miscellanea]; ["\\profalar" ], "⌮", [miscellanea]; @@ -1248,7 +1248,7 @@ let bindings_set_1 = [ ["\\ltrPar" ], "⦖", [miscellanea]; ["\\vzigzag" ], "⦚", [miscellanea]; ["\\angrtvbd" ], "⦝", [miscellanea]; - ["\\angrtvb" ], "⦝︀", [miscellanea]; + ["\\angrtvb" ], "⦝", [miscellanea]; ["\\ange" ], "⦤", [miscellanea]; ["\\range" ], "⦥", [miscellanea]; ["\\dwangle" ], "⦦", [miscellanea]; @@ -1367,9 +1367,9 @@ let bindings_set_1 = [ ["\\smt" ], "⪪", [miscellanea]; ["\\lat" ], "⪫", [miscellanea]; ["\\smte" ], "⪬", [miscellanea]; - ["\\smtes" ], "⪬︀", [miscellanea]; + ["\\smtes" ], "⪬", [miscellanea]; ["\\late" ], "⪭", [miscellanea]; - ["\\lates" ], "⪭︀", [miscellanea]; + ["\\lates" ], "⪭", [miscellanea]; ["\\Sc" ], "⪼", [miscellanea]; ["\\subdot" ], "⪽", [miscellanea]; ["\\supdot" ], "⪾", [miscellanea]; diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 631408c032..a16825b5c9 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -926,7 +926,7 @@ let extern_ref vars ref us = let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None) -let rec extern inctx scopes vars r = +let rec extern inctx ?impargs scopes vars r = match remove_one_coercion inctx (flatten_application r) with | Some (nargs,inctx,r') -> (try extern_notations scopes vars (Some nargs) r @@ -990,10 +990,10 @@ let rec extern inctx scopes vars r = | GLetIn (na,b,t,c) -> CLetIn (make ?loc na,sub_extern false scopes vars b, Option.map (extern_typ scopes vars) t, - extern inctx scopes (add_vname vars na) c) + extern inctx ?impargs scopes (add_vname vars na) c) | GProd (na,bk,t,c) -> - factorize_prod scopes vars na bk t c + factorize_prod ?impargs scopes vars na bk t c | GLambda (na,bk,t,c) -> factorize_lambda inctx scopes vars na bk t c @@ -1092,12 +1092,12 @@ let rec extern inctx scopes vars r = in insert_coercion coercion (CAst.make ?loc c) -and extern_typ (subentry,(_,scopes)) = - extern true (subentry,(Notation.current_type_scope_name (),scopes)) +and extern_typ ?impargs (subentry,(_,scopes)) = + extern true ?impargs (subentry,(Notation.current_type_scope_name (),scopes)) and sub_extern inctx (subentry,(_,scopes)) = extern inctx (subentry,(None,scopes)) -and factorize_prod scopes vars na bk t c = +and factorize_prod ?impargs scopes vars na bk t c = let implicit_type = is_reserved_type na t in let aty = extern_typ scopes vars t in let vars = add_vname vars na in @@ -1117,7 +1117,13 @@ and factorize_prod scopes vars na bk t c = | _ -> CProdN ([binder],b)) | _ -> assert false) | _, _ -> - let c' = extern_typ scopes vars c in + let impargs_hd, impargs_tl = + match impargs with + | Some [hd] -> Some hd, None + | Some (hd::tl) -> Some hd, Some tl + | _ -> None, None in + let bk = Option.default Explicit impargs_hd in + let c' = extern_typ ?impargs:impargs_tl scopes vars c in match na, c'.v with | Name id, CProdN (CLocalAssum(nal,Default bk',ty)::bl,b) when binding_kind_eq bk bk' @@ -1306,8 +1312,8 @@ and extern_notation (custom,scopes as allscopes) vars t rules = let extern_glob_constr vars c = extern false (InConstrEntrySomeLevel,(None,[])) vars c -let extern_glob_type vars c = - extern_typ (InConstrEntrySomeLevel,(None,[])) vars c +let extern_glob_type ?impargs vars c = + extern_typ ?impargs (InConstrEntrySomeLevel,(None,[])) vars c (******************************************************************) (* Main translation function from constr -> constr_expr *) @@ -1320,7 +1326,7 @@ let extern_constr ?lax ?(inctx=false) ?scope env sigma t = let extern_constr_in_scope ?lax ?inctx scope env sigma t = extern_constr ?lax ?inctx ~scope env sigma t -let extern_type ?lax ?(goal_concl_style=false) env sigma t = +let extern_type ?lax ?(goal_concl_style=false) env sigma ?impargs t = (* "goal_concl_style" means do alpha-conversion using the "goal" convention *) (* i.e.: avoid using the names of goal/section/rel variables and the short *) (* names of global definitions of current module when computing names for *) @@ -1330,7 +1336,7 @@ let extern_type ?lax ?(goal_concl_style=false) env sigma t = (* consideration; see namegen.ml for further details *) let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in let r = Detyping.detype Detyping.Later ?lax goal_concl_style avoid env sigma t in - extern_glob_type (vars_of_env env) r + extern_glob_type ?impargs (vars_of_env env) r let extern_sort sigma s = extern_glob_sort (detype_sort sigma s) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index fe64661a66..f85e49d2df 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -25,7 +25,7 @@ open Ltac_pretype val extern_cases_pattern : Id.Set.t -> 'a cases_pattern_g -> cases_pattern_expr val extern_glob_constr : Id.Set.t -> 'a glob_constr_g -> constr_expr -val extern_glob_type : Id.Set.t -> 'a glob_constr_g -> constr_expr +val extern_glob_type : ?impargs:Glob_term.binding_kind list -> Id.Set.t -> 'a glob_constr_g -> constr_expr val extern_constr_pattern : names_context -> Evd.evar_map -> constr_pattern -> constr_expr val extern_closed_glob : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> @@ -42,7 +42,7 @@ val extern_constr : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> val extern_constr_in_scope : ?lax:bool -> ?inctx:bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid -val extern_type : ?lax:bool -> ?goal_concl_style:bool -> env -> Evd.evar_map -> types -> constr_expr +val extern_type : ?lax:bool -> ?goal_concl_style:bool -> env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> types -> constr_expr val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort val extern_rel_context : constr option -> env -> Evd.evar_map -> rel_context -> local_binder_expr list diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index 0133a02ca7..49e4c91182 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/plugins/firstorder/g_ground.mlg @@ -47,7 +47,7 @@ let ()= let default_intuition_tac = - let tac _ _ = Auto.h_auto None [] None in + let tac _ _ = Auto.h_auto None [] (Some []) in let name = { Tacexpr.mltac_plugin = "ground_plugin"; mltac_tactic = "auto_with"; } in let entry = { Tacexpr.mltac_name = name; mltac_index = 0 } in Tacenv.register_ml_tactic name [| tac |]; diff --git a/printing/printer.ml b/printing/printer.ml index 70fdd43908..32dc4bb0f0 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -106,8 +106,8 @@ let pr_letype_env = Proof_diffs.pr_letype_env let pr_type_env ?lax ?goal_concl_style env sigma c = pr_etype_env ?lax ?goal_concl_style env sigma (EConstr.of_constr c) -let pr_ltype_env ?lax ?goal_concl_style env sigma c = - pr_letype_env ?lax ?goal_concl_style env sigma (EConstr.of_constr c) +let pr_ltype_env ?lax ?goal_concl_style env sigma ?impargs c = + pr_letype_env ?lax ?goal_concl_style env sigma ?impargs (EConstr.of_constr c) let pr_ljudge_env env sigma j = (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type) diff --git a/printing/printer.mli b/printing/printer.mli index 8b8157fba4..936426949c 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -45,6 +45,10 @@ val enable_goal_names_printing : bool ref intended to be printed in scope [some_scope_name]. It defaults to [None]. + [~impargs:some_list_of_binding_kind] indicates the implicit arguments + of the external quatification. Only used for printing types (not + terms), and at toplevel (only "l" versions). It defaults to [None]. + [~lax:true] is for debugging purpose. It defaults to [~lax:false]. *) @@ -66,7 +70,7 @@ val pr_leconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env - val pr_econstr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> EConstr.t -> Pp.t val pr_etype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t -val pr_letype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t +val pr_letype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> ?impargs:Glob_term.binding_kind list -> EConstr.types -> Pp.t val pr_open_constr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> open_constr -> Pp.t val pr_open_lconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> open_constr -> Pp.t @@ -97,7 +101,7 @@ val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp [~lax:true] is for debugging purpose. *) -val pr_ltype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t +val pr_ltype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> ?impargs:Glob_term.binding_kind list -> types -> Pp.t val pr_type_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t val pr_closed_glob_n_env : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> closed_glob_constr -> Pp.t diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index da76bc130d..fb91ea7b5c 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -244,9 +244,9 @@ let process_goal sigma g : EConstr.t reified_goal = let hyps = List.map to_tuple hyps in { name; ty; hyps; env; sigma };; -let pr_letype_env ?lax ?goal_concl_style env sigma t = +let pr_letype_env ?lax ?goal_concl_style env sigma ?impargs t = Ppconstr.pr_lconstr_expr env sigma - (Constrextern.extern_type ?lax ?goal_concl_style env sigma t) + (Constrextern.extern_type ?lax ?goal_concl_style env sigma ?impargs t) let pp_of_type env sigma ty = pr_letype_env ~goal_concl_style:true env sigma ty diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli index 59b7beb794..83e721d3d5 100644 --- a/printing/proof_diffs.mli +++ b/printing/proof_diffs.mli @@ -57,7 +57,7 @@ val diff_goal : ?og_s:(Goal.goal sigma) -> Goal.goal -> Evd.evar_map -> Pp.t (** Convert a string to a list of token strings using the lexer *) val tokenize_string : string -> string list -val pr_letype_env : ?lax:bool -> ?goal_concl_style:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Pp.t +val pr_letype_env : ?lax:bool -> ?goal_concl_style:bool -> Environ.env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> EConstr.types -> Pp.t val pr_leconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t val pr_lconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> env -> evar_map -> constr -> Pp.t diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index f889da4e98..8cf0797b17 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -39,7 +39,7 @@ The reduction tactics unfold Nat.sub when the 1st and Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub pf : -forall D1 C1 : Type, +forall {D1 C1 : Type}, (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2 pf is not universe polymorphic @@ -47,7 +47,7 @@ Arguments pf {D1}%foo_scope {C1}%type_scope _ [D2 C2] : simpl never The reduction tactics never unfold pf pf is transparent Expands to: Constant Arguments.pf -fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C +fcomp : forall {A B C : Type}, (B -> C) -> (A -> B) -> A -> C fcomp is not universe polymorphic Arguments fcomp {A B C}%type_scope _ _ _ / @@ -75,7 +75,7 @@ The reduction tactics unfold f when the 3rd, 4th and 5th arguments evaluate to a constructor f is transparent Expands to: Constant Arguments.S1.S2.f -f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat +f : forall [T2 : Type], T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic Arguments f [T2]%type_scope _ _ !_%nat_scope !_ !_%nat_scope @@ -83,7 +83,7 @@ The reduction tactics unfold f when the 4th, 5th and 6th arguments evaluate to a constructor f is transparent Expands to: Constant Arguments.S1.f -f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat +f : forall [T1 T2 : Type], T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic Arguments f [T1 T2]%type_scope _ _ !_%nat_scope !_ !_%nat_scope diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 26ebd8efc3..abc7f0f88e 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -15,7 +15,7 @@ Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x Arguments eq {A}%type_scope Arguments eq_refl {B}%type_scope {y}, [B] _ -eq_refl : forall (A : Type) (x : A), x = x +eq_refl : forall {A : Type} {x : A}, x = x eq_refl is not universe polymorphic Arguments eq_refl {B}%type_scope {y}, [B] _ @@ -24,7 +24,7 @@ Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x Arguments myEq _%type_scope Arguments myrefl {C}%type_scope x : rename -myrefl : forall (B : Type) (x : A), B -> myEq B x x +myrefl : forall {B : Type} (x : A), B -> myEq B x x myrefl is not universe polymorphic Arguments myrefl {C}%type_scope x : rename @@ -38,7 +38,7 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := : forall T : Type, T -> nat -> nat -> nat Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename -myplus : forall T : Type, T -> nat -> nat -> nat +myplus : forall {T : Type}, T -> nat -> nat -> nat myplus is not universe polymorphic Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename @@ -53,7 +53,7 @@ Inductive myEq (A B : Type) (x : A) : A -> Prop := Arguments myEq (_ _)%type_scope Arguments myrefl A%type_scope {C}%type_scope x : rename -myrefl : forall (A B : Type) (x : A), B -> myEq A B x x +myrefl : forall (A : Type) {B : Type} (x : A), B -> myEq A B x x myrefl is not universe polymorphic Arguments myrefl A%type_scope {C}%type_scope x : rename @@ -69,7 +69,7 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := : forall T : Type, T -> nat -> nat -> nat Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename -myplus : forall T : Type, T -> nat -> nat -> nat +myplus : forall {T : Type}, T -> nat -> nat -> nat myplus is not universe polymorphic Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename diff --git a/test-suite/output/NoAxiomFromR.v b/test-suite/output/NoAxiomFromR.v index 9cf6879699..7abbe29452 100644 --- a/test-suite/output/NoAxiomFromR.v +++ b/test-suite/output/NoAxiomFromR.v @@ -5,6 +5,6 @@ Inductive TT : Set := Lemma lem4 : forall (n m : nat), S m <= m -> C (S m) <> C n -> False. -Proof. firstorder. Qed. +Proof. firstorder lia. Qed. Print Assumptions lem4. diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index 71d162c314..8fb267e343 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -1,4 +1,4 @@ -existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} +existT : forall [A : Type] (P : A -> Type) (x : A), P x -> {x : A & P x} existT is template universe polymorphic on sigT.u0 sigT.u1 Arguments existT [A]%type_scope _%function_scope @@ -8,19 +8,19 @@ Inductive sigT (A : Type) (P : A -> Type) : Type := Arguments sigT [A]%type_scope _%type_scope Arguments existT [A]%type_scope _%function_scope -existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} +existT : forall [A : Type] (P : A -> Type) (x : A), P x -> {x : A & P x} Argument A is implicit Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x Arguments eq {A}%type_scope Arguments eq_refl {A}%type_scope {x}, [A] _ -eq_refl : forall (A : Type) (x : A), x = x +eq_refl : forall {A : Type} {x : A}, x = x eq_refl is not universe polymorphic Arguments eq_refl {A}%type_scope {x}, [A] _ Expands to: Constructor Coq.Init.Logic.eq_refl -eq_refl : forall (A : Type) (x : A), x = x +eq_refl : forall {A : Type} {x : A}, x = x When applied to no arguments: Arguments A, x are implicit and maximally inserted @@ -65,14 +65,14 @@ bar : foo bar is not universe polymorphic Expanded type for implicit arguments -bar : forall x : nat, x = 0 +bar : forall {x : nat}, x = 0 Arguments bar {x} Expands to: Constant PrintInfos.bar *** [ bar : foo ] Expanded type for implicit arguments -bar : forall x : nat, x = 0 +bar : forall {x : nat}, x = 0 Arguments bar {x} Module Coq.Init.Peano diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index ffba1d35cc..9d8e830d64 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -18,6 +18,7 @@ le_sind: P n -> (forall m : nat, n <= m -> P m -> P (S m)) -> forall n0 : nat, n <= n0 -> P n0 +(use "About" for full details on implicit arguments) false: bool true: bool eq_true: bool -> Prop @@ -37,7 +38,7 @@ Nat.leb: nat -> nat -> bool Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b eq_true_ind_r: - forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true + forall (P : bool -> Prop) [b : bool], P b -> eq_true b -> P true eq_true_rec: forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b @@ -49,9 +50,9 @@ bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b eq_true_ind: forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b eq_true_rec_r: - forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true + forall (P : bool -> Set) [b : bool], P b -> eq_true b -> P true eq_true_rect_r: - forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true + forall (P : bool -> Type) [b : bool], P b -> eq_true b -> P true bool_sind: forall P : bool -> SProp, P true -> P false -> forall b : bool, P b Byte.to_bits: @@ -62,13 +63,13 @@ Byte.of_bits: Byte.byte andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true andb_true_intro: - forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true + forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true BoolSpec_sind: - forall (P Q : Prop) (P0 : bool -> SProp), + forall [P Q : Prop] (P0 : bool -> SProp), (P -> P0 true) -> (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b BoolSpec_ind: - forall (P Q : Prop) (P0 : bool -> Prop), + forall [P Q : Prop] (P0 : bool -> Prop), (P -> P0 true) -> (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b Byte.to_bits_of_bits: @@ -76,9 +77,10 @@ Byte.to_bits_of_bits: b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))), Byte.to_bits (Byte.of_bits b) = b bool_choice: - forall (S : Set) (R1 R2 : S -> Prop), + forall [S : Set] [R1 R2 : S -> Prop], (forall x : S, {R1 x} + {R2 x}) -> {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x} +(use "About" for full details on implicit arguments) mult_n_O: forall n : nat, 0 = n * 0 plus_O_n: forall n : nat, 0 + n = n plus_n_O: forall n : nat, n = n + 0 @@ -104,25 +106,35 @@ f_equal2_mult: f_equal2_nat: forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat), x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2 +(use "About" for full details on implicit arguments) andb_true_intro: - forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true + forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true bool_choice: - forall (S : Set) (R1 R2 : S -> Prop), + forall [S : Set] [R1 R2 : S -> Prop], (forall x : S, {R1 x} + {R2 x}) -> {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x} +(use "About" for full details on implicit arguments) andb_true_intro: - forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true + forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true +(use "About" for full details on implicit arguments) andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true +(use "About" for full details on implicit arguments) h: n <> newdef n h': newdef n <> n +(use "About" for full details on implicit arguments) h: n <> newdef n h': newdef n <> n +(use "About" for full details on implicit arguments) h: n <> newdef n +(use "About" for full details on implicit arguments) h: n <> newdef n +(use "About" for full details on implicit arguments) h: n <> newdef n h': newdef n <> n +(use "About" for full details on implicit arguments) +(use "About" for full details on implicit arguments) The command has indeed failed with message: No such goal. The command has indeed failed with message: @@ -131,9 +143,14 @@ The command has indeed failed with message: Query commands only support the single numbered goal selector. h: P n h': ~ P n +(use "About" for full details on implicit arguments) h: P n h': ~ P n +(use "About" for full details on implicit arguments) h: P n h': ~ P n +(use "About" for full details on implicit arguments) h: P n +(use "About" for full details on implicit arguments) h: P n +(use "About" for full details on implicit arguments) diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out index 7038eac22c..5627e4bd3c 100644 --- a/test-suite/output/SearchHead.out +++ b/test-suite/output/SearchHead.out @@ -4,6 +4,7 @@ le_S: forall n m : nat, n <= m -> n <= S m le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m le_n_S: forall n m : nat, n <= m -> S n <= S m le_S_n: forall n m : nat, S n <= S m -> n <= m +(use "About" for full details on implicit arguments) false: bool true: bool negb: bool -> bool @@ -17,6 +18,7 @@ Nat.leb: nat -> nat -> bool Nat.ltb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool Nat.eqb: nat -> nat -> bool +(use "About" for full details on implicit arguments) mult_n_O: forall n : nat, 0 = n * 0 plus_O_n: forall n : nat, 0 + n = n plus_n_O: forall n : nat, n = n + 0 @@ -35,5 +37,8 @@ f_equal2_plus: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 f_equal2_mult: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2 +(use "About" for full details on implicit arguments) h: newdef n +(use "About" for full details on implicit arguments) h: P n +(use "About" for full details on implicit arguments) diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index 4cd0ffb1dc..36fc1a5914 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -11,6 +11,7 @@ Nat.leb: nat -> nat -> bool Nat.ltb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool Nat.eqb: nat -> nat -> bool +(use "About" for full details on implicit arguments) Nat.two: nat Nat.one: nat Nat.zero: nat @@ -44,8 +45,10 @@ Nat.tail_addmul: nat -> nat -> nat -> nat Nat.of_uint_acc: Decimal.uint -> nat -> nat Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat Nat.log2_iter: nat -> nat -> nat -> nat -> nat -length: forall A : Type, list A -> nat +length: forall [A : Type], list A -> nat Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat +(use "About" for full details on implicit arguments) +(use "About" for full details on implicit arguments) Nat.div2: nat -> nat Nat.sqrt: nat -> nat Nat.log2: nat -> nat @@ -74,18 +77,29 @@ Nat.of_uint_acc: Decimal.uint -> nat -> nat Nat.log2_iter: nat -> nat -> nat -> nat -> nat Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat +(use "About" for full details on implicit arguments) mult_n_Sm: forall n m : nat, n * m + n = n * S m +(use "About" for full details on implicit arguments) iff_refl: forall A : Prop, A <-> A le_n: forall n : nat, n <= n -identity_refl: forall (A : Type) (a : A), identity a a -eq_refl: forall (A : Type) (x : A), x = x +identity_refl: forall [A : Type] (a : A), identity a a +eq_refl: forall {A : Type} {x : A}, x = x Nat.divmod: nat -> nat -> nat -> nat -> nat * nat -conj: forall A B : Prop, A -> B -> A /\ B -pair: forall A B : Type, A -> B -> A * B +(use "About" for full details on implicit arguments) +conj: forall [A B : Prop], A -> B -> A /\ B +pair: forall {A B : Type}, A -> B -> A * B Nat.divmod: nat -> nat -> nat -> nat -> nat * nat +(use "About" for full details on implicit arguments) +(use "About" for full details on implicit arguments) h: n <> newdef n +(use "About" for full details on implicit arguments) h: n <> newdef n +(use "About" for full details on implicit arguments) h: P n +(use "About" for full details on implicit arguments) h': ~ P n +(use "About" for full details on implicit arguments) h: P n +(use "About" for full details on implicit arguments) h: P n +(use "About" for full details on implicit arguments) diff --git a/test-suite/output/SearchRewrite.out b/test-suite/output/SearchRewrite.out index 5edea5dff6..3c0880b20c 100644 --- a/test-suite/output/SearchRewrite.out +++ b/test-suite/output/SearchRewrite.out @@ -1,5 +1,10 @@ plus_n_O: forall n : nat, n = n + 0 +(use "About" for full details on implicit arguments) plus_O_n: forall n : nat, 0 + n = n +(use "About" for full details on implicit arguments) h: n = newdef n +(use "About" for full details on implicit arguments) h: n = newdef n +(use "About" for full details on implicit arguments) h: n = newdef n +(use "About" for full details on implicit arguments) diff --git a/test-suite/output/clear.out b/test-suite/output/clear.out new file mode 100644 index 0000000000..42e3abf26f --- /dev/null +++ b/test-suite/output/clear.out @@ -0,0 +1,5 @@ +1 subgoal + + z := 0 : nat + ============================ + True diff --git a/test-suite/output/clear.v b/test-suite/output/clear.v new file mode 100644 index 0000000000..d584cf752e --- /dev/null +++ b/test-suite/output/clear.v @@ -0,0 +1,8 @@ +Module Wish11692. + +(* Support for let-in in clear dependent *) + +Goal forall x : Prop, let z := 0 in let z' : (fun _ => True) x := I in let y := x in y -> True. +Proof. intros x z z' y H. clear dependent x. Show. exact I. Qed. + +End Wish11692. diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index c247bc11dc..598bd8b9c5 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -638,7 +638,7 @@ Instance PartialOrder_proper_type `(PartialOrder A eqA R) : Proper (eqA==>eqA==>iffT) R. Proof. intros. -apply proper_sym_arrow_iffT_2; auto with *. +apply proper_sym_arrow_iffT_2. 1-2: auto with crelations. intros x x' Hx y y' Hy Hr. transitivity x. - generalize (partial_order_equivalence x x'); compute; intuition. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 5adb927357..43adb0b69f 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -640,7 +640,7 @@ Instance PartialOrder_proper `(PartialOrder A eqA R) : Proper (eqA==>eqA==>iff) R. Proof. intros. -apply proper_sym_impl_iff_2; auto with *. +apply proper_sym_impl_iff_2. 1-2: auto with relations. intros x x' Hx y y' Hy Hr. transitivity x. - generalize (partial_order_equivalence x x'); compute; intuition. diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v index 418f7a8767..7d0382ec43 100644 --- a/theories/Classes/Morphisms_Prop.v +++ b/theories/Classes/Morphisms_Prop.v @@ -75,7 +75,7 @@ Instance Acc_pt_morphism {A:Type}(E R : A->A->Prop) `(Equivalence _ E) `(Proper _ (E==>E==>iff) R) : Proper (E==>iff) (Acc R). Proof. - apply proper_sym_impl_iff; auto with *. + apply proper_sym_impl_iff. auto with relations. intros x y EQ WF. apply Acc_intro; intros z Hz. rewrite <- EQ in Hz. now apply Acc_inv with x. Qed. diff --git a/theories/Compat/Coq812.v b/theories/Compat/Coq812.v index d628456c78..ee4bac3542 100644 --- a/theories/Compat/Coq812.v +++ b/theories/Compat/Coq812.v @@ -9,3 +9,4 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.12 *) +Set Firstorder Solver auto with *. diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 8cdc6e54c5..82055c4752 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -1335,7 +1335,7 @@ Proof. apply Hl; auto. constructor. apply Hr; eauto. - apply InA_InfA with (eqA:=eqke); auto with *. intros (y',e') H6. + apply InA_InfA with (eqA:=eqke). auto with typeclass_instances. intros (y',e') H6. destruct (elements_aux_mapsto r acc y' e'); intuition. red; simpl; eauto. red; simpl; eauto with ordered_type. diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 1eb6a3f372..2001201ec3 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -760,7 +760,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). Instance eqke_equiv : Equivalence eqke. Proof. unfold eq_key_elt; split; repeat red; firstorder. - eauto with *. + eauto. congruence. Qed. @@ -910,9 +910,9 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). assert (Hstep' : forall k e a m' m'', InA eqke (k,e) l -> ~In k m' -> Add k e m' m'' -> P m' a -> P m'' (F (k,e) a)). intros k e a m' m'' H ? ? ?; eapply Hstep; eauto. - revert H; unfold l; rewrite InA_rev, elements_mapsto_iff; auto with *. + revert H; unfold l; rewrite InA_rev, elements_mapsto_iff. auto. assert (Hdup : NoDupA eqk l). - unfold l. apply NoDupA_rev; try red; unfold eq_key ; eauto with *. + unfold l. apply NoDupA_rev; try red; unfold eq_key. auto with typeclass_instances. apply elements_3w. assert (Hsame : forall k, find k m = findA (eqb k) l). intros k. unfold l. rewrite elements_o, findA_rev; auto. @@ -993,7 +993,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). rewrite 2 fold_spec_right. set (l:=rev (elements m)). assert (Rstep' : forall k e a b, InA eqke (k,e) l -> R a b -> R (f k e a) (g k e b)) by - (intros; apply Rstep; auto; rewrite elements_mapsto_iff, <- InA_rev; auto with *). + (intros; apply Rstep; auto; rewrite elements_mapsto_iff, <- InA_rev; assumption). clearbody l; clear Rstep m. induction l; simpl; auto. apply Rstep'; auto. @@ -1107,17 +1107,20 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). Proof. intros. rewrite 2 fold_spec_right. - assert (NoDupA eqk (rev (elements m1))) by (auto with *). - assert (NoDupA eqk (rev (elements m2))) by (auto with *). - apply fold_right_equivlistA_restr with (R:=complement eqk)(eqA:=eqke); - auto with *. + assert (NoDupA eqk (rev (elements m1))) by auto with map typeclass_instances. + assert (NoDupA eqk (rev (elements m2))) by auto with map typeclass_instances. + apply fold_right_equivlistA_restr with (R:=complement eqk)(eqA:=eqke). + auto with typeclass_instances. + auto. + 2: auto with crelations. + 4, 5: auto with map. intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; simpl in *; apply Comp; auto. unfold complement, eq_key, eq_key_elt; repeat red. intuition eauto. intros (k,e) (k',e'); unfold eq_key, uncurry; simpl; auto. rewrite <- NoDupA_altdef; auto. intros (k,e). - rewrite 2 InA_rev, <- 2 elements_mapsto_iff, 2 find_mapsto_iff, H; - auto with *. + rewrite 2 InA_rev, <- 2 elements_mapsto_iff, 2 find_mapsto_iff, H. + auto with crelations. Qed. Lemma fold_Equal2 : forall m1 m2 i j, Equal m1 m2 -> eqA i j -> @@ -1125,10 +1128,13 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). Proof. intros. rewrite 2 fold_spec_right. - assert (NoDupA eqk (rev (elements m1))) by (auto with * ). - assert (NoDupA eqk (rev (elements m2))) by (auto with * ). - apply fold_right_equivlistA_restr2 with (R:=complement eqk)(eqA:=eqke) - ; auto with *. + assert (NoDupA eqk (rev (elements m1))) by auto with map typeclass_instances. + assert (NoDupA eqk (rev (elements m2))) by auto with map typeclass_instances. + apply fold_right_equivlistA_restr2 with (R:=complement eqk)(eqA:=eqke). + auto with typeclass_instances. + 1, 10: auto. + 2: auto with crelations. + 4, 5: auto with map. - intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; simpl in *; apply Comp; auto. - unfold complement, eq_key, eq_key_elt; repeat red. intuition eauto. - intros (k,e) (k',e') z z' h h'; unfold eq_key, uncurry;simpl; auto. @@ -1136,8 +1142,8 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). auto. - rewrite <- NoDupA_altdef; auto. - intros (k,e). - rewrite 2 InA_rev, <- 2 elements_mapsto_iff, 2 find_mapsto_iff, H; - auto with *. + rewrite 2 InA_rev, <- 2 elements_mapsto_iff, 2 find_mapsto_iff, H. + auto with crelations. Qed. @@ -1149,18 +1155,22 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). set (f':=uncurry f). change (f k e (fold_right f' i (rev (elements m1)))) with (f' (k,e) (fold_right f' i (rev (elements m1)))). - assert (NoDupA eqk (rev (elements m1))) by (auto with *). - assert (NoDupA eqk (rev (elements m2))) by (auto with *). + assert (NoDupA eqk (rev (elements m1))) by auto with map typeclass_instances. + assert (NoDupA eqk (rev (elements m2))) by auto with map typeclass_instances. apply fold_right_add_restr with - (R:=complement eqk)(eqA:=eqke)(eqB:=eqA); auto with *. + (R:=complement eqk)(eqA:=eqke)(eqB:=eqA). + auto with typeclass_instances. + auto. + 2: auto with crelations. + 4, 5: auto with map. intros (k1,e1) (k2,e2) (Hk,He) a a' Ha; unfold f'; simpl in *. apply Comp; auto. unfold complement, eq_key_elt, eq_key; repeat red; intuition eauto. unfold f'; intros (k1,e1) (k2,e2); unfold eq_key, uncurry; simpl; auto. rewrite <- NoDupA_altdef; auto. - rewrite InA_rev, <- elements_mapsto_iff by (auto with *). firstorder. + rewrite InA_rev, <- elements_mapsto_iff. firstorder. intros (a,b). rewrite InA_cons, 2 InA_rev, <- 2 elements_mapsto_iff, - 2 find_mapsto_iff by (auto with *). + 2 find_mapsto_iff. unfold eq_key_elt; simpl. rewrite H0. rewrite add_o. @@ -1791,7 +1801,7 @@ Module OrdProperties (M:S). Lemma sort_equivlistA_eqlistA : forall l l' : list (key*elt), sort ltk l -> sort ltk l' -> equivlistA eqke l l' -> eqlistA eqke l l'. Proof. - apply SortA_equivlistA_eqlistA; eauto with *. + apply SortA_equivlistA_eqlistA; auto with typeclass_instances. Qed. Ltac clean_eauto := unfold O.eqke, O.ltk; simpl; intuition; eauto. @@ -1842,7 +1852,9 @@ Module OrdProperties (M:S). elements m = elements_lt p m ++ elements_ge p m. Proof. unfold elements_lt, elements_ge, leb; intros. - apply filter_split with (eqA:=eqk) (ltA:=ltk); eauto with *. + apply filter_split with (eqA:=eqk) (ltA:=ltk). + 1-3: auto with typeclass_instances. + 2: auto with map. intros; destruct x; destruct y; destruct p. rewrite gtb_1 in H; unfold O.ltk in H; simpl in *. assert (~ltk (t1,e0) (k,e1)). @@ -1856,14 +1868,14 @@ Module OrdProperties (M:S). (elements_lt (x,e) m ++ (x,e):: elements_ge (x,e) m). Proof. intros; unfold elements_lt, elements_ge. - apply sort_equivlistA_eqlistA; auto with *. - apply (@SortA_app _ eqke); auto with *. - apply (@filter_sort _ eqke); auto with *; clean_eauto. + apply sort_equivlistA_eqlistA. auto with map. + apply (@SortA_app _ eqke). auto with typeclass_instances. + apply (@filter_sort _ eqke). 1-3: auto with typeclass_instances. auto with map. constructor; auto with map. - apply (@filter_sort _ eqke); auto with *; clean_eauto. - rewrite (@InfA_alt _ eqke); auto with *; try (clean_eauto; fail). + apply (@filter_sort _ eqke). 1-3: auto with typeclass_instances. auto with map. + rewrite (@InfA_alt _ eqke). 2-4: auto with typeclass_instances. intros. - rewrite filter_InA in H1; auto with *; destruct H1. + rewrite filter_InA in H1 by auto with map. destruct H1. rewrite leb_1 in H2. destruct y; unfold O.ltk in *; simpl in *. rewrite <- elements_mapsto_iff in H1. @@ -1871,22 +1883,22 @@ Module OrdProperties (M:S). contradict H. exists e0; apply MapsTo_1 with t0; auto with ordered_type. ME.order. - apply (@filter_sort _ eqke); auto with *; clean_eauto. + apply (@filter_sort _ eqke). 1-3: auto with typeclass_instances. auto with map. intros. - rewrite filter_InA in H1; auto with *; destruct H1. + rewrite filter_InA in H1 by auto with map. destruct H1. rewrite gtb_1 in H3. destruct y; destruct x0; unfold O.ltk in *; simpl in *. inversion_clear H2. red in H4; simpl in *; destruct H4. ME.order. - rewrite filter_InA in H4; auto with *; destruct H4. + rewrite filter_InA in H4 by auto with map. destruct H4. rewrite leb_1 in H4. unfold O.ltk in *; simpl in *; ME.order. red; intros a; destruct a. rewrite InA_app_iff, InA_cons, 2 filter_InA, <-2 elements_mapsto_iff, leb_1, gtb_1, find_mapsto_iff, (H0 t0), <- find_mapsto_iff, - add_mapsto_iff by (auto with *). + add_mapsto_iff by auto with map. unfold O.eqke, O.ltk; simpl. destruct (E.compare t0 x); intuition; try fold (~E.eq x t0); auto with ordered_type. - elim H; exists e0; apply MapsTo_1 with t0; auto. @@ -1898,8 +1910,8 @@ Module OrdProperties (M:S). eqlistA eqke (elements m') (elements m ++ (x,e)::nil). Proof. intros. - apply sort_equivlistA_eqlistA; auto with *. - apply (@SortA_app _ eqke); auto with *. + apply sort_equivlistA_eqlistA. auto with map. + apply (@SortA_app _ eqke). auto with typeclass_instances. auto with map. auto. intros. inversion_clear H2. destruct x0; destruct y. @@ -1911,7 +1923,7 @@ Module OrdProperties (M:S). red; intros a; destruct a. rewrite InA_app_iff, InA_cons, InA_nil, <- 2 elements_mapsto_iff, find_mapsto_iff, (H0 t0), <- find_mapsto_iff, - add_mapsto_iff by (auto with *). + add_mapsto_iff. unfold O.eqke; simpl. intuition. destruct (E.eq_dec x t0) as [Heq|Hneq]; auto. exfalso. @@ -1926,9 +1938,9 @@ Module OrdProperties (M:S). eqlistA eqke (elements m') ((x,e)::elements m). Proof. intros. - apply sort_equivlistA_eqlistA; auto with *. + apply sort_equivlistA_eqlistA. auto with map. change (sort ltk (((x,e)::nil) ++ elements m)). - apply (@SortA_app _ eqke); auto with *. + apply (@SortA_app _ eqke). auto with typeclass_instances. auto. auto with map. intros. inversion_clear H1. destruct y; destruct x0. @@ -1940,7 +1952,7 @@ Module OrdProperties (M:S). red; intros a; destruct a. rewrite InA_cons, <- 2 elements_mapsto_iff, find_mapsto_iff, (H0 t0), <- find_mapsto_iff, - add_mapsto_iff by (auto with *). + add_mapsto_iff. unfold O.eqke; simpl. intuition. destruct (E.eq_dec x t0) as [Heq|Hneq]; auto. exfalso. @@ -1954,7 +1966,7 @@ Module OrdProperties (M:S). Equal m m' -> eqlistA eqke (elements m) (elements m'). Proof. intros. - apply sort_equivlistA_eqlistA; auto with *. + apply sort_equivlistA_eqlistA. 1-2: auto with map. red; intros. destruct x; do 2 rewrite <- elements_mapsto_iff. do 2 rewrite find_mapsto_iff; rewrite H; split; auto. @@ -2056,7 +2068,7 @@ Module OrdProperties (M:S). inversion_clear H1 as [? ? H2|? ? H2]. red in H2; destruct H2; simpl in *; ME.order. inversion_clear H4. rename H1 into H3. - rewrite (@InfA_alt _ eqke) in H3; eauto with *. + rewrite (@InfA_alt _ eqke) in H3 by auto with typeclass_instances. apply (H3 (y,x0)); auto. Qed. diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index e9cb0a6aa7..c3c6c96997 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -679,7 +679,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. simpl; auto. destruct o; simpl; intros. (* Some *) - apply (SortA_app (eqA:=eq_key_elt)); auto with *. + apply (SortA_app (eqA:=eq_key_elt)). 1-2: auto with typeclass_instances. constructor; auto. apply In_InfA; intros. destruct y0. @@ -698,7 +698,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. eapply xelements_bits_lt_1; eauto. eapply xelements_bits_lt_2; eauto. (* None *) - apply (SortA_app (eqA:=eq_key_elt)); auto with *. + apply (SortA_app (eqA:=eq_key_elt)). auto with typeclass_instances. 1-2: auto. intros x0 y0. do 2 rewrite InA_alt. intros (y1,(Hy1,H)) (y2,(Hy2,H0)). diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v index d267991c3c..73021a84a3 100644 --- a/theories/FSets/FSetBridge.v +++ b/theories/FSets/FSetBridge.v @@ -772,7 +772,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. generalize C; unfold compat_bool, Proper, respectful; intros; apply (f_equal negb); auto. simpl; unfold Equal; intuition. - apply filter_3; firstorder. + apply filter_3; firstorder with bool. elim (H2 a); intros. assert (In a s). eapply filter_1; eauto. diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v index 4edeaee72e..bff999042b 100644 --- a/theories/FSets/FSetCompat.v +++ b/theories/FSets/FSetCompat.v @@ -381,22 +381,22 @@ Module Update_Sets Instance lt_strorder : StrictOrder lt. Proof. split. - intros x Hx. apply (M.lt_not_eq Hx); auto with *. + intros x Hx. apply (M.lt_not_eq Hx). auto with crelations. exact M.lt_trans. Qed. Instance lt_compat : Proper (eq==>eq==>iff) lt. Proof. - apply proper_sym_impl_iff_2; auto with *. + apply proper_sym_impl_iff_2. 1-2: auto with crelations. intros s s' Hs u u' Hu H. assert (H0 : lt s' u). destruct (M.compare s' u) as [H'|H'|H']; auto. - elim (M.lt_not_eq H). transitivity s'; auto with *. + elim (M.lt_not_eq H). transitivity s'; auto. elim (M.lt_not_eq (M.lt_trans H H')); auto. destruct (M.compare s' u') as [H'|H'|H']; auto. elim (M.lt_not_eq H). - transitivity u'; auto with *. transitivity s'; auto with *. - elim (M.lt_not_eq (M.lt_trans H' H0)); auto with *. + transitivity u'. 2: auto with crelations. transitivity s'; auto. + elim (M.lt_not_eq (M.lt_trans H' H0)); auto with crelations. Qed. Definition compare s s' := diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v index 1542660ab7..ac08351ad9 100644 --- a/theories/FSets/FSetEqProperties.v +++ b/theories/FSets/FSetEqProperties.v @@ -924,7 +924,7 @@ transitivity (f x (fold f s0 i)). apply fold_add with (eqA:=eqA); auto with set. transitivity (g x (fold f s0 i)); auto with set. transitivity (g x (fold g s0 i)); auto with set. -apply gc; auto with *. +apply gc; auto with set. symmetry; apply fold_add with (eqA:=eqA); auto. do 2 rewrite fold_empty; reflexivity. Qed. diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index 88d12fc387..98b445580b 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -365,7 +365,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). assert (Pstep' : forall x a s' s'', InA x l -> ~In x s' -> Add x s' s'' -> P s' a -> P s'' (f x a)). intros; eapply Pstep; eauto. - rewrite elements_iff, <- InA_rev; auto with *. + rewrite elements_iff, <- InA_rev; auto. assert (Hdup : NoDup l) by (unfold l; eauto using elements_3w, NoDupA_rev with *). assert (Hsame : forall x, In x s <-> InA x l) by @@ -435,7 +435,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). intros A B R f g i j s Rempty Rstep. rewrite 2 fold_spec_right. set (l:=rev (elements s)). assert (Rstep' : forall x a b, InA x l -> R a b -> R (f x a) (g x b)) by - (intros; apply Rstep; auto; rewrite elements_iff, <- InA_rev; auto with *). + (intros; apply Rstep; auto; rewrite elements_iff, <- InA_rev; auto). clearbody l; clear Rstep s. induction l; simpl; auto. Qed. @@ -487,7 +487,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). fold f s i = fold_right f i l. Proof. intros; exists (rev (elements s)); split. - apply NoDupA_rev; auto with *. + apply NoDupA_rev. auto with typeclass_instances. auto with set. split; intros. rewrite elements_iff; do 2 rewrite InA_alt. split; destruct 1; generalize (In_rev (elements s) x0); exists x0; intuition. @@ -521,7 +521,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). intros; destruct (fold_0 s i f) as (l,(Hl, (Hl1, Hl2))); destruct (fold_0 s' i f) as (l',(Hl', (Hl'1, Hl'2))). rewrite Hl2; rewrite Hl'2; clear Hl2 Hl'2. - apply fold_right_add with (eqA:=E.eq)(eqB:=eqA); auto with *. + apply fold_right_add with (eqA:=E.eq)(eqB:=eqA). auto with typeclass_instances. 1-5: auto. rewrite <- Hl1; auto. intros a; rewrite InA_cons; rewrite <- Hl1; rewrite <- Hl'1; rewrite (H2 a); intuition. @@ -550,7 +550,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). intros. apply fold_rel with (R:=fun u v => eqA u (f x v)); intros. reflexivity. - transitivity (f x0 (f x b)); auto. apply Comp; auto with *. + transitivity (f x0 (f x b)); auto. apply Comp; auto. Qed. (** ** Fold is a morphism *) @@ -559,7 +559,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). eqA (fold f s i) (fold f s i'). Proof. intros. apply fold_rel with (R:=eqA); auto. - intros; apply Comp; auto with *. + intros; apply Comp; auto. Qed. Lemma fold_equal : @@ -914,7 +914,7 @@ Module OrdProperties (M:S). Lemma sort_equivlistA_eqlistA : forall l l' : list elt, sort E.lt l -> sort E.lt l' -> equivlistA E.eq l l' -> eqlistA E.eq l l'. Proof. - apply SortA_equivlistA_eqlistA; eauto with *. + apply SortA_equivlistA_eqlistA; auto with typeclass_instances. Qed. Definition gtb x y := match E.compare x y with GT _ => true | _ => false end. @@ -958,7 +958,7 @@ Module OrdProperties (M:S). elements s = elements_lt x s ++ elements_ge x s. Proof. unfold elements_lt, elements_ge, leb; intros. - eapply (@filter_split _ E.eq _ E.lt); auto with *. + eapply (@filter_split _ E.eq _ E.lt). 1-2: auto with typeclass_instances. 2: auto with set. intros. rewrite gtb_1 in H. assert (~E.lt y x). @@ -972,32 +972,32 @@ Module OrdProperties (M:S). Proof. intros; unfold elements_ge, elements_lt. apply sort_equivlistA_eqlistA; auto with set. - apply (@SortA_app _ E.eq); auto with *. - apply (@filter_sort _ E.eq); auto with *. + apply (@SortA_app _ E.eq). auto with typeclass_instances. + apply (@filter_sort _ E.eq). 1-3: auto with typeclass_instances. auto with set. constructor; auto. - apply (@filter_sort _ E.eq); auto with *. - rewrite ME.Inf_alt by (apply (@filter_sort _ E.eq); eauto with *). + apply (@filter_sort _ E.eq). 1-3: auto with typeclass_instances. auto with set. + rewrite ME.Inf_alt by (apply (@filter_sort _ E.eq); auto with set typeclass_instances). intros. - rewrite filter_InA in H1; auto with *; destruct H1. + rewrite filter_InA in H1 by auto with fset. destruct H1. rewrite leb_1 in H2. rewrite <- elements_iff in H1. assert (~E.eq x y). contradict H; rewrite H; auto. ME.order. intros. - rewrite filter_InA in H1; auto with *; destruct H1. + rewrite filter_InA in H1 by auto with fset. destruct H1. rewrite gtb_1 in H3. inversion_clear H2. ME.order. - rewrite filter_InA in H4; auto with *; destruct H4. + rewrite filter_InA in H4 by auto with fset. destruct H4. rewrite leb_1 in H4. ME.order. red; intros a. rewrite InA_app_iff, InA_cons, !filter_InA, <-elements_iff, - leb_1, gtb_1, (H0 a) by auto with *. + leb_1, gtb_1, (H0 a) by auto with fset. intuition. destruct (E.compare a x); intuition. - fold (~E.lt a x); auto with *. + fold (~E.lt a x); auto with ordered_type set. Qed. Definition Above x s := forall y, In y s -> E.lt y x. @@ -1008,15 +1008,15 @@ Module OrdProperties (M:S). eqlistA E.eq (elements s') (elements s ++ x::nil). Proof. intros. - apply sort_equivlistA_eqlistA; auto with *. - apply (@SortA_app _ E.eq); auto with *. + apply sort_equivlistA_eqlistA. auto with set. + apply (@SortA_app _ E.eq). auto with typeclass_instances. auto with set. auto. intros. inversion_clear H2. rewrite <- elements_iff in H1. apply ME.lt_eq with x; auto with ordered_type. inversion H3. red; intros a. - rewrite InA_app_iff, InA_cons, InA_nil by auto with *. + rewrite InA_app_iff, InA_cons, InA_nil. do 2 rewrite <- elements_iff; rewrite (H0 a); intuition. Qed. @@ -1025,9 +1025,9 @@ Module OrdProperties (M:S). eqlistA E.eq (elements s') (x::elements s). Proof. intros. - apply sort_equivlistA_eqlistA; auto with *. + apply sort_equivlistA_eqlistA. auto with set. change (sort E.lt ((x::nil) ++ elements s)). - apply (@SortA_app _ E.eq); auto with *. + apply (@SortA_app _ E.eq). auto with typeclass_instances. auto. auto with set. intros. inversion_clear H1. rewrite <- elements_iff in H2. diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 6aa1198c08..a4347bbe62 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -233,6 +233,7 @@ Tactic Notation "clear" "dependent" hyp(h) := clear h || match goal with | H : context [ h ] |- _ => depclear H; depclear h + | H := context [ h ] |- _ => depclear H; depclear h end || fail "hypothesis to clear is used in the conclusion (maybe indirectly)" in depclear h. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 6a1554d102..f050f11170 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -1413,13 +1413,16 @@ End Fold_Right_Recursor. Lemma existsb_exists : forall l, existsb l = true <-> exists x, In x l /\ f x = true. Proof. - induction l; simpl; intuition. - inversion H. - firstorder. - destruct (orb_prop _ _ H1); firstorder. - firstorder. - subst. - rewrite H2; auto. + induction l as [ | a m IH ]; split; simpl. + - easy. + - intros [x [[]]]. + - rewrite orb_true_iff; intros [ H | H ]. + + exists a; auto. + + rewrite IH in H; destruct H as [ x [ Hxm Hfx ] ]. + exists x; auto. + - intros [ x [ [ Hax | Hxm ] Hfx ] ]. + + now rewrite Hax, Hfx. + + destruct IH as [ _ -> ]; eauto with bool. Qed. Lemma existsb_nth : forall l n d, n < length l -> @@ -2747,7 +2750,7 @@ Section Exists_Forall. Proof. split. - induction 1; firstorder; subst; auto. - - induction l; firstorder. + - induction l; firstorder auto with datatypes. Qed. Lemma Forall_nth l : diff --git a/theories/MSets/MSetPositive.v b/theories/MSets/MSetPositive.v index a15b533d3d..4f2f4256e2 100644 --- a/theories/MSets/MSetPositive.v +++ b/theories/MSets/MSetPositive.v @@ -771,7 +771,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. Proof. unfold Exists, In. intro f. induction s as [|l IHl o r IHr]; intros i; simpl. - firstorder. + firstorder with bool. rewrite <- 2orb_lazy_alt, 2orb_true_iff, <- andb_lazy_alt, andb_true_iff. rewrite IHl, IHr. clear IHl IHr. split. diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index 6af9572fff..7c5b43096a 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -60,7 +60,7 @@ Ltac zcongruence := repeat red; intros; zify; congruence. Instance eq_equiv : Equivalence eq. Proof. - split. 1-2: firstorder. + split. 1-2: firstorder auto with crelations. intros x y z; apply eq_trans. Qed. diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v index 6e8d9e4571..fe9794de8a 100644 --- a/theories/Structures/EqualitiesFacts.v +++ b/theories/Structures/EqualitiesFacts.v @@ -74,7 +74,7 @@ Module KeyDecidableType(D:DecidableType). Lemma InA_eqk_eqke {elt} p (m:list (key*elt)) : InA eqk p m -> exists q, eqk p q /\ InA eqke q m. Proof. - induction 1; firstorder. + induction 1; firstorder auto with crelations. Qed. Lemma InA_eqk {elt} p q (m:list (key*elt)) : diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 52457d15dc..a7170c8e18 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -83,6 +83,8 @@ let print_ref reduce ref udecl = let ctx,ccl = Reductionops.splay_prod_assum env sigma typ in EConstr.it_mkProd_or_LetIn ccl ctx else typ in + let impargs = select_stronger_impargs (implicits_of_global ref) in + let impargs = List.map binding_kind_of_status impargs in let variance = let open GlobRef in match ref with | VarRef _ | ConstRef _ -> None | IndRef (ind,_) | ConstructRef ((ind,_),_) -> @@ -95,7 +97,7 @@ let print_ref reduce ref udecl = else mt () in let priv = None in (* We deliberately don't print private univs in About. *) - hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ + hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma ~impargs typ ++ Printer.pr_abstract_universe_ctx sigma ?variance univs ?priv) (********************************) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e2fdae37fb..b5ecd62dad 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1778,12 +1778,15 @@ let vernac_search ~pstate ~atts s gopt r = let pp = if !search_output_name_only then pr else begin - let pc = pr_lconstr_env env Evd.(from_env env) c in + let open Impargs in + let impargs = select_stronger_impargs (implicits_of_global ref) in + let impargs = List.map binding_kind_of_status impargs in + let pc = pr_ltype_env env Evd.(from_env env) ~impargs c in hov 2 (pr ++ str":" ++ spc () ++ pc) end in Feedback.msg_notice pp in - match s with + (match s with | SearchPattern c -> (Search.search_pattern ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search | SearchRewrite c -> @@ -1796,7 +1799,8 @@ let vernac_search ~pstate ~atts s gopt r = Search.prioritize_search) pr_search | Search sl -> (Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> - Search.prioritize_search) pr_search + Search.prioritize_search) pr_search); + Feedback.msg_notice (str "(use \"About\" for full details on implicit arguments)") let vernac_locate ~pstate = let open Constrexpr in function | LocateAny {v=AN qid} -> Prettyp.print_located_qualid qid |