diff options
133 files changed, 645 insertions, 867 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index a7c0846e35..63d6ccc240 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -1,14 +1,11 @@ -# This file describes the maintainers for the main components. See -# `dev/doc/MERGING.md`. +# This file associates maintainer teams to each component. +# See CONTRIBUTING.md ########## Contributing process ########## /.github/ @coq/contributing-process-maintainers /CONTRIBUTING.md @coq/contributing-process-maintainers -/dev/doc/shield-icon.png @coq/contributing-process-maintainers - -/dev/doc/release-process.md @coq/contributing-process-maintainers ########## Build system ########## @@ -53,6 +50,19 @@ # Trick to avoid getting review requests # each time someone modifies the changelog +/dev/doc/build-system*.txt @coq/legacy-build-maintainers +/dev/doc/build-system.dune.md @coq/build-maintainers +/dev/doc/critical-bugs @coq/kernel-maintainers +/dev/doc/econstr.md @coq/engine-maintainers +/dev/doc/proof-engine.md @coq/engine-maintainers +/dev/doc/release-process.md @coq/contributing-process-maintainers +/dev/doc/shield-icon.png @coq/contributing-process-maintainers +/dev/doc/SProp.md @coq/universes-maintainers +/dev/doc/style.txt @coq/contributing-process-maintainers +/dev/doc/unification.txt @coq/pretyper-maintainers +/dev/doc/universes.md @coq/universes-maintainers +/dev/doc/xml-protocol @coq/stm-maintainers + /man/ @coq/doc-maintainers /doc/plugin_tutorial/ @coq/plugin-tutorial-maintainers diff --git a/Makefile.ci b/Makefile.ci index f14203fa4a..c2a3cd7e14 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -45,6 +45,7 @@ CI_TARGETS= \ ci-stdlib2 \ ci-tlc \ ci-unimath \ + ci-unicoq \ ci-verdi-raft \ ci-vst @@ -64,6 +65,8 @@ ci-math-classes: ci-bignums ci-corn: ci-math-classes +ci-mtac2: ci-unicoq + ci-fiat-crypto: ci-coqprime ci-rewriter ci-simple-io: ci-ext-lib diff --git a/Makefile.common b/Makefile.common index 32bf19e99c..780ba717ee 100644 --- a/Makefile.common +++ b/Makefile.common @@ -42,17 +42,17 @@ COQTIME_FILE_MAKER:=tools/TimeFileMaker.py COQMAKE_BOTH_TIME_FILES:=tools/make-both-time-files.py COQMAKE_BOTH_SINGLE_TIMING_FILES:=tools/make-both-single-timing-files.py VOTOUR:=bin/votour +OCAMLLIBDEP:=bin/ocamllibdep$(EXE) +OCAMLLIBDEPBYTE:=bin/ocamllibdep.byte$(EXE) # these get installed! TOOLS:=$(COQDEP) $(COQMAKEFILE) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\ - $(COQWORKMGR) $(COQPP) $(VOTOUR) + $(COQWORKMGR) $(COQPP) $(VOTOUR) $(OCAMLLIBDEP) TOOLS_HELPERS:=tools/CoqMakefile.in $(COQMAKE_ONE_TIME_FILE) $(COQTIME_FILE_MAKER)\ $(COQMAKE_BOTH_TIME_FILES) $(COQMAKE_BOTH_SINGLE_TIMING_FILES) COQDEPBOOT:=bin/coqdep_boot$(EXE) COQDEPBOOTBYTE:=bin/coqdep_boot.byte$(EXE) -OCAMLLIBDEP:=bin/ocamllibdep$(EXE) -OCAMLLIBDEPBYTE:=bin/ocamllibdep.byte$(EXE) FAKEIDE:=bin/fake_ide$(EXE) FAKEIDEBYTE:=bin/fake_ide.byte$(EXE) diff --git a/default.nix b/default.nix index 174e199014..ae6a8d06e5 100644 --- a/default.nix +++ b/default.nix @@ -77,7 +77,7 @@ stdenv.mkDerivation rec { !elem (baseNameOf path) [".git" "result" "bin" "_build" "_build_ci" "nix"]) ./.; preConfigure = '' - patchShebangs dev/tools/ + patchShebangs dev/tools/ doc/stdlib ''; prefixKey = "-prefix "; diff --git a/dev/ci/ci-mtac2.sh b/dev/ci/ci-mtac2.sh index 7075d4d7f6..e08dcf07ab 100755 --- a/dev/ci/ci-mtac2.sh +++ b/dev/ci/ci-mtac2.sh @@ -3,10 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download unicoq - -( cd "${CI_BUILD_DIR}/unicoq" && coq_makefile -f Make -o Makefile && make && make install ) - git_download mtac2 ( cd "${CI_BUILD_DIR}/mtac2" && coq_makefile -f _CoqProject -o Makefile && make ) diff --git a/dev/ci/ci-unicoq.sh b/dev/ci/ci-unicoq.sh new file mode 100755 index 0000000000..36acb115e9 --- /dev/null +++ b/dev/ci/ci-unicoq.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download unicoq + +( cd "${CI_BUILD_DIR}/unicoq" && coq_makefile -f Make -o Makefile && make && make install ) diff --git a/dev/ci/user-overlays/11417-ppedrot-rm-kind-of-type.sh b/dev/ci/user-overlays/11417-ppedrot-rm-kind-of-type.sh new file mode 100644 index 0000000000..5fb29e1826 --- /dev/null +++ b/dev/ci/user-overlays/11417-ppedrot-rm-kind-of-type.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "11417" ] || [ "$CI_BRANCH" = "rm-kind-of-type" ]; then + + elpi_CI_REF=rm-kind-of-type + elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi + +fi diff --git a/dev/ci/user-overlays/11521-SkySkimmer-no-optname.sh b/dev/ci/user-overlays/11521-SkySkimmer-no-optname.sh new file mode 100644 index 0000000000..f2a431978d --- /dev/null +++ b/dev/ci/user-overlays/11521-SkySkimmer-no-optname.sh @@ -0,0 +1,15 @@ +if [ "$CI_PULL_REQUEST" = "11521" ] || [ "$CI_BRANCH" = "no-optname" ]; then + + coqhammer_CI_REF=no-optname + coqhammer_CI_GITURL=https://github.com/SkySkimmer/coqhammer + + equations_CI_REF=no-optname + equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + + unicoq_CI_REF=no-optname + unicoq_CI_GITURL=https://github.com/SkySkimmer/unicoq + + paramcoq_CI_REF=no-optname + paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq + +fi diff --git a/dev/ci/user-overlays/11557-SkySkimmer-template-directify.sh b/dev/ci/user-overlays/11557-SkySkimmer-template-directify.sh new file mode 100644 index 0000000000..913b39c30c --- /dev/null +++ b/dev/ci/user-overlays/11557-SkySkimmer-template-directify.sh @@ -0,0 +1,12 @@ +if [ "$CI_PULL_REQUEST" = "11557" ] || [ "$CI_BRANCH" = "template-directify" ]; then + + equations_CI_REF=template-directify + equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + + paramcoq_CI_REF=template-directify + paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq + + elpi_CI_REF=template-directify + elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi + +fi diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index ba68501e04..58c2fcc68a 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -127,11 +127,11 @@ in time. - [ ] Send an e-mail on Coqdev announcing that the tag has been put so that package managers can start preparing package updates (including a `coq-bignums` compatible version). -- [ ] Ping **@erikmd** to update the Docker images in `coqorg/coq` - (requires `coq-bignums` in `extra-dev` for a beta / in `released` - for a final release). +- [ ] When opening the corresponding PR for `coq` in the opam repository ([`coq/opam-coq-archive`](https://github.com/coq/opam-coq-archive) or [`ocaml/opam-repository`](https://github.com/ocaml/opam-repository)), + the package managers can Cc `@erikmd` to request that he prepare the necessary configuration for the Docker release in [`coqorg/coq`](https://hub.docker.com/r/coqorg/coq) + (namely, he'll need to make sure a `coq-bignums` opam package is available in [`extra-dev`](https://github.com/coq/opam-coq-archive/tree/master/extra-dev), respectively [`released`](https://github.com/coq/opam-coq-archive/tree/master/released), so the Docker image gathering `coq` and `coq-bignums` can be built). - [ ] Draft a release on GitHub. -- [ ] Get **@maximedenes** to sign the Windows and MacOS packages and +- [ ] Get `@maximedenes` to sign the Windows and MacOS packages and upload them on GitHub. - [ ] Prepare a page of news on the website with the link to the GitHub release (see [coq/www#63](https://github.com/coq/www/pull/63)). @@ -139,8 +139,6 @@ in time. *TODO: setup some continuous deployment for this.* - [ ] Merge the website update, publish the release and send announcement e-mails. -- [ ] Ping **@Zimmi48** to publish a new version on Zenodo. - *TODO: automate this.* - [ ] Close the milestone ## At the final release time ## @@ -160,7 +158,10 @@ in time. Repeat the generic process documented above for all releases. +Ping `@Zimmi48` to: + - [ ] Switch the default version of the reference manual on the website. +- [ ] Publish a new version on Zenodo. ## At the patch-level release time ## diff --git a/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst b/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst new file mode 100644 index 0000000000..32526babdb --- /dev/null +++ b/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst @@ -0,0 +1,8 @@ +- **Added:** + :cmd:`Arguments <Arguments (implicits)>` now supports setting + implicit an anonymous argument, as e.g. in :g:`Arguments id {A} {_}`. + (`#11098 <https://github.com/coq/coq/pull/11098>`_, + by Hugo Herbelin, fixes `#4696 + <https://github.com/coq/coq/pull/4696>`_, `#5173 + <https://github.com/coq/coq/pull/5173>`_, `#9098 + <https://github.com/coq/coq/pull/9098>`_.). diff --git a/doc/changelog/03-notations/11113-remove-compat.rst b/doc/changelog/03-notations/11113-remove-compat.rst index 8c71d70cda..3bcdd3dd6f 100644 --- a/doc/changelog/03-notations/11113-remove-compat.rst +++ b/doc/changelog/03-notations/11113-remove-compat.rst @@ -1,4 +1,4 @@ -- Removed deprecated ``compat`` modifier of :cmd:`Notation` +- **Removed:** deprecated ``compat`` modifier of :cmd:`Notation` and :cmd:`Infix` commands (`#11113 <https://github.com/coq/coq/pull/11113>`_, by Théo Zimmermann, with help from Jason Gross). diff --git a/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst b/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst index 8551cf3aac..f377b53ae2 100644 --- a/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst +++ b/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst @@ -1,2 +1,3 @@ -- The printing algorithm now interleave search for notations and removal of coercions +- **Changed:** + The printing algorithm now interleaves search for notations and removal of coercions (`#11172 <https://github.com/coq/coq/pull/11172>`_, by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/10760-more-rapply.rst b/doc/changelog/04-tactics/10760-more-rapply.rst index 2815f8af8a..eeae2ec519 100644 --- a/doc/changelog/04-tactics/10760-more-rapply.rst +++ b/doc/changelog/04-tactics/10760-more-rapply.rst @@ -1,4 +1,5 @@ -- The tactic :tacn:`rapply` in :g:`Coq.Program.Tactics` now handles +- **Changed:** + The tactic :tacn:`rapply` in :g:`Coq.Program.Tactics` now handles arbitrary numbers of underscores and takes in a :g:`uconstr`. In rare cases where users were relying on :tacn:`rapply` inserting exactly 15 underscores and no more, due to the lemma having a diff --git a/doc/changelog/07-commands-and-options/11162-local-cs.rst b/doc/changelog/07-commands-and-options/11162-local-cs.rst index 5a69a107cd..638222fbe1 100644 --- a/doc/changelog/07-commands-and-options/11162-local-cs.rst +++ b/doc/changelog/07-commands-and-options/11162-local-cs.rst @@ -1 +1,3 @@ -- Handle the ``#[local]`` attribute in :g:`Canonical Structure` declarations (`#11162 <https://github.com/coq/coq/pull/11162>`_, by Enrico Tassi). +- **Added:** Handle the ``#[local]`` attribute in :g:`Canonical + Structure` declarations (`#11162 + <https://github.com/coq/coq/pull/11162>`_, by Enrico Tassi). diff --git a/doc/changelog/07-commands-and-options/11164-let-cs.rst b/doc/changelog/07-commands-and-options/11164-let-cs.rst index b9ecd140e7..ec34c075ae 100644 --- a/doc/changelog/07-commands-and-options/11164-let-cs.rst +++ b/doc/changelog/07-commands-and-options/11164-let-cs.rst @@ -1 +1,3 @@ -- A section variable introduces with :g:`Let` can be declared as a :g:`Canonical Structure` (`#11164 <https://github.com/coq/coq/pull/11164>`_, by Enrico Tassi). +- **Added:** A section variable introduces with :g:`Let` can be + declared as a :g:`Canonical Structure` (`#11164 + <https://github.com/coq/coq/pull/11164>`_, by Enrico Tassi). diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index b0197c500c..f706633da9 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -35,6 +35,11 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`, use the Simplex method for solving linear goals. If it is not set, the decision procedures are using Fourier elimination. +.. opt:: Dump Arith + + This option (unset by default) may be set to a file path where + debug info will be written. + .. cmd:: Show Lia Profile This command prints some statistics about the amount of pivoting diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 7b4b652a6a..f0bbaed8f3 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1583,7 +1583,7 @@ An implicit argument is considered trailing when all following arguments are dec implicit. Trailing implicit arguments cannot be declared non maximally inserted, otherwise they would never be inserted. -.. exn:: Argument @ident is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ]. +.. exn:: Argument @name is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ]. For instance: @@ -1713,11 +1713,11 @@ Declaring Implicit Arguments -.. cmd:: Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } +.. cmd:: Arguments @qualid {* {| [ @name ] | { @name } | @name } } :name: Arguments (implicits) This command is used to set implicit arguments *a posteriori*, - where the list of possibly bracketed :token:`ident` is a prefix of the list of + where the list of possibly bracketed :token:`name` is a prefix of the list of arguments of :token:`qualid` where the ones to be declared implicit are surrounded by square brackets and the ones to be declared as maximally inserted implicits are surrounded by curly braces. @@ -1731,20 +1731,20 @@ Declaring Implicit Arguments This command clears implicit arguments. -.. cmdv:: Global Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } +.. cmdv:: Global Arguments @qualid {* {| [ @name ] | { @name } | @name } } This command is used to recompute the implicit arguments of :token:`qualid` after ending of the current section if any, enforcing the implicit arguments known from inside the section to be the ones declared by the command. -.. cmdv:: Local Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } +.. cmdv:: Local Arguments @qualid {* {| [ @name ] | { @name } | @name } } When in a module, tell not to activate the implicit arguments of :token:`qualid` declared by this command to contexts that require the module. -.. cmdv:: {? {| Global | Local } } Arguments @qualid {*, {+ {| [ @ident ] | { @ident } | @ident } } } +.. cmdv:: {? {| Global | Local } } Arguments @qualid {*, {+ {| [ @name ] | { @name } | @name } } } For names of constants, inductive types, constructors, lemmas which can only be applied to a fixed number of diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 09090ce89a..721c7a7a51 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1063,6 +1063,9 @@ Parameterized inductive types | cons3 : A -> list3 -> list3. End list3. + Attributes ``uniform`` and ``nonuniform`` respectively enable and + disable uniform parameters for a single inductive declaration block. + .. seealso:: Section :ref:`inductive-definitions` and the :tacn:`induction` tactic. diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index e5edd08995..3d1fc6d4b9 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -545,7 +545,7 @@ Computing Module dependencies In order to compute module dependencies (to be used by ``make`` or ``dune``), |Coq| provides the ``coqdep`` tool. -``coqdep`` computes inter-module dependencies for |Coq| and |OCaml| +``coqdep`` computes inter-module dependencies for |Coq| programs, and prints the dependencies on the standard output in a format readable by make. When a directory is given as argument, it is recursively looked at. @@ -554,11 +554,6 @@ Dependencies of |Coq| modules are computed by looking at ``Require`` commands (``Require``, ``Require Export``, ``Require Import``), but also at the command ``Declare ML Module``. -Dependencies of |OCaml| modules are computed by looking at -`open` commands and the dot notation *module.value*. However, this is -done approximately and you are advised to use ``ocamldep`` instead for the -|OCaml| module dependencies. - See the man page of ``coqdep`` for more details and options. Both Dune and ``coq_makefile`` use ``coqdep`` to compute the diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 1f9178f4b6..85d86bed62 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -270,7 +270,7 @@ class GallinaObject(PlainObject): :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`. """ subdomain = "thm" - index_suffix = "(thm)" + index_suffix = "(theorem)" annotation = "Theorem" class VernacObject(NotationObject): @@ -283,7 +283,7 @@ class VernacObject(NotationObject): This command is equivalent to :n:`…`. """ subdomain = "cmd" - index_suffix = "(cmd)" + index_suffix = "(command)" annotation = "Command" def _name_from_signature(self, signature): @@ -306,7 +306,7 @@ class VernacVariantObject(VernacObject): This is equivalent to :n:`Axiom @ident : @term`. """ - index_suffix = "(cmdv)" + index_suffix = "(command variant)" annotation = "Variant" def _name_from_signature(self, signature): @@ -322,7 +322,7 @@ class TacticNotationObject(NotationObject): :token:`expr` is evaluated to ``v`` which must be a tactic value. … """ subdomain = "tacn" - index_suffix = "(tacn)" + index_suffix = "(tactic)" annotation = None class TacticNotationVariantObject(TacticNotationObject): @@ -342,7 +342,7 @@ class TacticNotationVariantObject(TacticNotationObject): The number is the failure level. If no level is specified, it defaults to 0. … """ - index_suffix = "(tacnv)" + index_suffix = "(tactic variant)" annotation = "Variant" class OptionObject(NotationObject): @@ -357,7 +357,7 @@ class OptionObject(NotationObject): application of a tactic. """ subdomain = "opt" - index_suffix = "(opt)" + index_suffix = "(option)" annotation = "Option" def _name_from_signature(self, signature): @@ -534,7 +534,7 @@ class ExceptionObject(NotationObject): Raised if :n:`@tactic` does not fully solve the goal. """ subdomain = "exn" - index_suffix = "(err)" + index_suffix = "(error)" annotation = "Error" # Uses “exn” since “err” already is a CSS class added by “writer_aux”. @@ -557,7 +557,7 @@ class WarningObject(NotationObject): valid coercion paths are ignored. """ subdomain = "warn" - index_suffix = "(warn)" + index_suffix = "(warning)" annotation = "Warning" # Generate names automatically diff --git a/doc/tools/coqrst/notations/sphinx.py b/doc/tools/coqrst/notations/sphinx.py index ab18d136b8..5659a64b84 100644 --- a/doc/tools/coqrst/notations/sphinx.py +++ b/doc/tools/coqrst/notations/sphinx.py @@ -80,9 +80,11 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor): while atom != "": if atom[0] == "'": node += nodes.raw("\\textquotesingle{}", "\\textquotesingle{}", format="latex") + node += nodes.raw("'", "'", format="html") atom = atom[1:] elif atom[0] == "`": node += nodes.raw("\\`{}", "\\`{}", format="latex") + node += nodes.raw("`", "`", format="html") atom = atom[1:] else: index_ap = atom.find("'") diff --git a/engine/eConstr.ml b/engine/eConstr.ml index e37a58be61..08e283f524 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -739,6 +739,26 @@ let fresh_global ?loc ?rigid ?names env sigma reference = let is_global = isRefX +(** Kind of type *) + +type kind_of_type = + | SortType of ESorts.t + | CastType of types * t + | ProdType of Name.t Context.binder_annot * t * t + | LetInType of Name.t Context.binder_annot * t * t * t + | AtomicType of t * t array + +let kind_of_type sigma t = match kind sigma t with + | Sort s -> SortType s + | Cast (c,_,t) -> CastType (c, t) + | Prod (na,t,c) -> ProdType (na, t, c) + | LetIn (na,b,t,c) -> LetInType (na, b, t, c) + | App (c,l) -> AtomicType (c, l) + | (Rel _ | Meta _ | Var _ | Evar _ | Const _ + | Proj _ | Case _ | Fix _ | CoFix _ | Ind _) + -> AtomicType (t,[||]) + | (Lambda _ | Construct _ | Int _ | Float _) -> failwith "Not a type" + module Unsafe = struct let to_sorts = ESorts.unsafe_to_sorts diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 181714460d..ead7d88176 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -80,7 +80,14 @@ val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t val to_constr_opt : Evd.evar_map -> t -> Constr.t option (** Same as [to_constr], but returns [None] if some unresolved evars remain *) -val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type +type kind_of_type = + | SortType of ESorts.t + | CastType of types * t + | ProdType of Name.t Context.binder_annot * t * t + | LetInType of Name.t Context.binder_annot * t * t * t + | AtomicType of t * t array + +val kind_of_type : Evd.evar_map -> t -> kind_of_type (** {5 Constructors} *) diff --git a/engine/evd.ml b/engine/evd.ml index 70f58163fd..4bfa7c45e3 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1364,7 +1364,6 @@ module MiniEConstr = struct let kind sigma c = Constr.kind (whd_evar sigma c) let kind_upto = kind - let kind_of_type sigma c = Term.kind_of_type (whd_evar sigma c) let of_kind = Constr.of_kind let of_constr c = c let of_constr_array v = v diff --git a/engine/evd.mli b/engine/evd.mli index 82e1003a65..2c1194a5de 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -711,7 +711,6 @@ module MiniEConstr : sig val kind : evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term val kind_upto : evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term - val kind_of_type : evar_map -> t -> (t, t) Term.kind_of_type val whd_evar : evar_map -> t -> t diff --git a/engine/namegen.ml b/engine/namegen.ml index 56277e8092..bcc8c34a4d 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -216,7 +216,6 @@ let it_mkLambda_or_LetIn_name env sigma b hyps = let get_mangle_names = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"mangle auto-generated names" ~key:["Mangle";"Names"] ~value:false @@ -227,7 +226,6 @@ let set_prefix x = mangle_names_prefix := forget_subscript x let () = Goptions.( declare_string_option { optdepr = false; - optname = "mangled names prefix"; optkey = ["Mangle";"Names";"Prefix"]; optread = (fun () -> Id.to_string !mangle_names_prefix); optwrite = begin fun x -> diff --git a/engine/uState.ml b/engine/uState.ml index 3546ece581..2eaa202246 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -53,7 +53,7 @@ let empty = uctx_weak_constraints = UPairSet.empty; } let elaboration_sprop_cumul = - Goptions.declare_bool_option_and_ref ~depr:false ~name:"SProp cumulativity during elaboration" + Goptions.declare_bool_option_and_ref ~depr:false ~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true let make ~lbound u = diff --git a/engine/univMinim.ml b/engine/univMinim.ml index fc0770cf75..53ff041fa5 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -15,7 +15,6 @@ open UnivSubst let get_set_minimization = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"minimization to Set" ~key:["Universe";"Minimization";"ToSet"] ~value:true diff --git a/ide/idetop.ml b/ide/idetop.ml index 7d92cff365..ae2301a0a7 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -360,7 +360,6 @@ let import_option_value = function let export_option_state s = { Interface.opt_sync = true; Interface.opt_depr = s.Goptions.opt_depr; - Interface.opt_name = s.Goptions.opt_name; Interface.opt_value = export_option_value s.Goptions.opt_value; } diff --git a/ide/protocol/interface.ml b/ide/protocol/interface.ml index 362833743e..be5e305ad3 100644 --- a/ide/protocol/interface.ml +++ b/ide/protocol/interface.ml @@ -71,8 +71,6 @@ type option_state = { (** Whether an option is synchronous *) opt_depr : bool; (** Whether an option is deprecated *) - opt_name : string; - (** A short string that is displayed when using [Test] *) opt_value : option_value; (** The current value of the option *) } diff --git a/ide/protocol/xmlprotocol.ml b/ide/protocol/xmlprotocol.ml index cad65cc5d6..a2c80ea118 100644 --- a/ide/protocol/xmlprotocol.ml +++ b/ide/protocol/xmlprotocol.ml @@ -79,13 +79,11 @@ let of_option_state s = Element ("option_state", [], [ of_bool s.opt_sync; of_bool s.opt_depr; - of_string s.opt_name; of_option_value s.opt_value]) let to_option_state = function - | Element ("option_state", [], [sync; depr; name; value]) -> { + | Element ("option_state", [], [sync; depr; value]) -> { opt_sync = to_bool sync; opt_depr = to_bool depr; - opt_name = to_string name; opt_value = to_option_value value } | x -> raise (Marshal_error("option_state",x)) @@ -429,8 +427,8 @@ end = struct | StringOptValue (Some s) -> s | BoolValue b -> if b then "true" else "false" let pr_option_state (s : option_state) = - Printf.sprintf "sync := %b; depr := %b; name := %s; value := %s\n" - s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value) + Printf.sprintf "sync := %b; depr := %b; value := %s\n" + s.opt_sync s.opt_depr (pr_option_value s.opt_value) let pr_list pr l = "["^String.concat ";" (List.map pr l)^"]" let pr_option pr = function None -> "None" | Some x -> "Some("^pr x^")" let pr_coq_object (o : 'a coq_object) = "FIXME" @@ -513,7 +511,7 @@ end = struct "type which contains a flattened n-tuple. We provide one example.\n"); Printf.printf "%s:\n\n%s\n\n" (print_val_t Option_state) (pr_xml (of_option_state { opt_sync = true; opt_depr = false; - opt_name = "name1"; opt_value = IntValue (Some 37) })); + opt_value = IntValue (Some 37) })); end open ReifType diff --git a/interp/constrextern.ml b/interp/constrextern.ml index c55e17e7a3..c198c4eb9b 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -194,7 +194,6 @@ let without_specific_symbols l = let get_record_print = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"record printing" ~key:["Printing";"Records"] ~value:true diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 2ceea58297..b2c572d290 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1615,7 +1615,6 @@ let is_non_zero_pat c = match c with let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"no parameters in constructors" ~key:["Asymmetric";"Patterns"] ~value:false diff --git a/interp/impargs.ml b/interp/impargs.ml index 9b50d9ca71..78c4b21920 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -83,8 +83,12 @@ let with_implicit_protection f x = type on_trailing_implicit = Error | Info | Silent -let msg_trailing_implicit (fail : on_trailing_implicit) id = - let str1 = "Argument " ^ Names.Id.to_string id ^ " is a trailing implicit, " in + +let msg_trailing_implicit (fail : on_trailing_implicit) na i = + let pos = match na with + | Anonymous -> "number " ^ string_of_int i + | Name id -> Names.Id.to_string id in + let str1 = "Argument " ^ pos ^ " is a trailing implicit, " in match fail with | Error -> user_err (strbrk (str1 ^ "so it can't be declared non maximal. Please use { } instead of [ ].")) @@ -92,12 +96,12 @@ let msg_trailing_implicit (fail : on_trailing_implicit) id = Flags.if_verbose Feedback.msg_info (strbrk (str1 ^ "so it has been declared maximally inserted.")) | Silent -> () -let set_maximality fail id imps b = +let set_maximality fail na i imps b = (* Force maximal insertion on ending implicits (compatibility) *) b || ( let is_set x = match x with None -> false | _ -> true in let b' = List.for_all is_set imps in - if b' then msg_trailing_implicit fail id; + if b' then msg_trailing_implicit fail na i; b') (*s Computation of implicit arguments *) @@ -355,13 +359,13 @@ let positions_of_implicits (_,impls) = (* Manage user-given implicit arguments *) -let rec prepare_implicits f = function +let rec prepare_implicits i f = function | [] -> [] | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit.") | (Name id, Some imp)::imps -> - let imps' = prepare_implicits f imps in - Some (ExplByName id,imp,(set_maximality Silent id imps' f.maximal,true)) :: imps' - | _::imps -> None :: prepare_implicits f imps + let imps' = prepare_implicits (i+1) f imps in + Some (ExplByName id,imp,(set_maximality Silent (Name id) i imps' f.maximal,true)) :: imps' + | _::imps -> None :: prepare_implicits (i+1) f imps let set_manual_implicits silent flags enriching autoimps l = (* Compare with automatic implicits to recover printing data and names *) @@ -370,9 +374,9 @@ let set_manual_implicits silent flags enriching autoimps l = let imps' = merge (k+1) autoimps explimps in begin match autoimp, explimp.CAst.v with | (Name id,_), Some (_,max) -> - Some (ExplByName id, Manual, (set_maximality (if silent then Silent else Error) id imps' max, true)) + Some (ExplByName id, Manual, (set_maximality (if silent then Silent else Error) (Name id) k imps' max, true)) | (Name id,Some exp), None when enriching -> - Some (ExplByName id, exp, (set_maximality (if silent then Silent else Info) id imps' flags.maximal, true)) + Some (ExplByName id, exp, (set_maximality (if silent then Silent else Info) (Name id) k imps' flags.maximal, true)) | (Name _,_), None -> None | (Anonymous,_), Some (Name id,max) -> Some (ExplByName id,Manual,(max,true)) @@ -390,7 +394,7 @@ let set_manual_implicits silent flags enriching autoimps l = let compute_semi_auto_implicits env sigma f t = if not f.auto then [DefaultImpArgs, []] else let l = compute_implicits_flags env sigma f false t in - [DefaultImpArgs, prepare_implicits f l] + [DefaultImpArgs, prepare_implicits 1 f l] (*s Constants. *) @@ -667,22 +671,22 @@ let maybe_declare_manual_implicits local ref ?enriching l = if List.exists (fun x -> x.CAst.v <> None) l then declare_manual_implicits local ref ?enriching l +let explicit_kind i = function + | Name id -> ExplByName id + | Anonymous -> ExplByPos (i,None) let compute_implicit_statuses autoimps l = let rec aux i = function | _ :: autoimps, Explicit :: manualimps -> None :: aux (i+1) (autoimps, manualimps) - | Name id :: autoimps, MaxImplicit :: manualimps -> - Some (ExplByName id, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps) - | Name id :: autoimps, NonMaxImplicit :: manualimps -> + | na :: autoimps, MaxImplicit :: manualimps -> + Some (explicit_kind i na, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps) + | na :: autoimps, NonMaxImplicit :: manualimps -> let imps' = aux (i+1) (autoimps, manualimps) in - let max = set_maximality Error id imps' false in - Some (ExplByName id, Manual, (max, true)) :: imps' - | Anonymous :: _, (NonMaxImplicit | MaxImplicit) :: _ -> - user_err ~hdr:"set_implicits" - (strbrk ("Argument number " ^ string_of_int i ^ " (anonymous in original definition) cannot be declared implicit.")) + let max = set_maximality Error na i imps' false in + Some (explicit_kind i na, Manual, (max, true)) :: imps' | autoimps, [] -> List.map (fun _ -> None) autoimps | [], _::_ -> assert false - in aux 0 (autoimps, l) + in aux 1 (autoimps, l) let set_implicits local ref l = let flags = !implicit_args in diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 3771454db5..b6b8e5265c 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -158,7 +158,7 @@ let ienv_push_var (env, n, ntypes, lra) (x,a,ra) = let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) = let auxntyp = 1 in let specif = (lookup_mind_specif env mi, u) in - let ty = type_of_inductive env specif in + let ty = type_of_inductive specif in let env' = let r = (snd (fst specif)).mind_relevance in let anon = Context.make_annot Anonymous r in diff --git a/kernel/inductive.ml b/kernel/inductive.ml index ca4fea45c5..c6035f78ff 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -143,9 +143,16 @@ let remember_subst u subst = Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst with Not_found -> subst +type param_univs = (unit -> Universe.t) list + +let make_param_univs env argtys = + Array.map_to_list (fun arg () -> + Sorts.univ_of_sort (snd (Reduction.dest_arity env arg))) + argtys + (* Bind expected levels of parameters to actual levels *) (* Propagate the new levels in the signature *) -let make_subst env = +let make_subst = let rec make subst = function | LocalDef _ :: sign, exp, args -> make subst (sign, exp, args) @@ -158,8 +165,8 @@ let make_subst env = (* arity is a global level which, at typing time, will be enforce *) (* to be greater than the level of the argument; this is probably *) (* a useless extra constraint *) - let s = Sorts.univ_of_sort (snd (dest_arity env (Lazy.force a))) in - make (cons_subst u s subst) (sign, exp, args) + let s = a () in + make (cons_subst u s subst) (sign, exp, args) | LocalAssum (_na,_t) :: sign, Some u::exp, [] -> (* No more argument here: we add the remaining universes to the *) (* substitution (when [u] is distinct from all other universes in the *) @@ -178,9 +185,8 @@ let make_subst env = exception SingletonInductiveBecomesProp of Id.t -let instantiate_universes env ctx ar argsorts = - let args = Array.to_list argsorts in - let subst = make_subst env (ctx,ar.template_param_levels,args) in +let instantiate_universes ctx ar args = + let subst = make_subst (ctx,ar.template_param_levels,args) in let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in let ty = (* Singleton type not containing types are interpretable in Prop *) @@ -198,12 +204,19 @@ let relevance_of_inductive env ind = let _, mip = lookup_mind_specif env ind in mip.mind_relevance -let type_of_inductive_gen ?(polyprop=true) env ((_,mip),u) paramtyps = +let check_instance mib u = + if not (match mib.mind_universes with + | Monomorphic _ -> Instance.is_empty u + | Polymorphic uctx -> Instance.length u = AUContext.size uctx) + then CErrors.anomaly Pp.(str "bad instance length on mutind.") + +let type_of_inductive_gen ?(polyprop=true) ((mib,mip),u) paramtyps = + check_instance mib u; match mip.mind_arity with | RegularArity a -> subst_instance_constr u a.mind_user_arity | TemplateArity ar -> let ctx = List.rev mip.mind_arity_ctxt in - let ctx,s = instantiate_universes env ctx ar paramtyps in + let ctx,s = instantiate_universes ctx ar paramtyps in (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e. the situation where a non-Prop singleton inductive becomes Prop when applied to Prop params *) @@ -211,21 +224,21 @@ let type_of_inductive_gen ?(polyprop=true) env ((_,mip),u) paramtyps = then raise (SingletonInductiveBecomesProp mip.mind_typename); Term.mkArity (List.rev ctx,s) -let type_of_inductive env pind = - type_of_inductive_gen env pind [||] +let type_of_inductive pind = + type_of_inductive_gen pind [] -let constrained_type_of_inductive env ((mib,_mip),u as pind) = - let ty = type_of_inductive env pind in +let constrained_type_of_inductive ((mib,_mip),u as pind) = + let ty = type_of_inductive pind in let cst = instantiate_inductive_constraints mib u in (ty, cst) -let constrained_type_of_inductive_knowing_parameters env ((mib,_mip),u as pind) args = - let ty = type_of_inductive_gen env pind args in +let constrained_type_of_inductive_knowing_parameters ((mib,_mip),u as pind) args = + let ty = type_of_inductive_gen pind args in let cst = instantiate_inductive_constraints mib u in (ty, cst) -let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args = - type_of_inductive_gen ~polyprop env mip args +let type_of_inductive_knowing_parameters ?(polyprop=true) mip args = + type_of_inductive_gen ~polyprop mip args (* The max of an array of universes *) @@ -244,6 +257,7 @@ let max_inductive_sort = (* Type of a constructor *) let type_of_constructor (cstr, u) (mib,mip) = + check_instance mib u; let ind = inductive_of_constructor cstr in let specif = mip.mind_user_lc in let i = index_of_constructor cstr in @@ -581,7 +595,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) = let push_ind specif env = let r = specif.mind_relevance in let anon = Context.make_annot Anonymous r in - let decl = LocalAssum (anon, hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) in + let decl = LocalAssum (anon, hnf_prod_applist env (type_of_inductive ((mib,specif),u)) lpar) in push_rel decl env in let env = Array.fold_right push_ind mib.mind_packets env in diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 8c40c318c5..b690fe1157 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -41,16 +41,22 @@ val inductive_paramdecls : mutual_inductive_body puniverses -> Constr.rel_contex val instantiate_inductive_constraints : mutual_inductive_body -> Instance.t -> Constraint.t -val constrained_type_of_inductive : env -> mind_specif puniverses -> types constrained +type param_univs = (unit -> Universe.t) list + +val make_param_univs : Environ.env -> constr array -> param_univs +(** The constr array is the types of the arguments to a template + polymorphic inductive. *) + +val constrained_type_of_inductive : mind_specif puniverses -> types constrained val constrained_type_of_inductive_knowing_parameters : - env -> mind_specif puniverses -> types Lazy.t array -> types constrained + mind_specif puniverses -> param_univs -> types constrained val relevance_of_inductive : env -> inductive -> Sorts.relevance -val type_of_inductive : env -> mind_specif puniverses -> types +val type_of_inductive : mind_specif puniverses -> types val type_of_inductive_knowing_parameters : - env -> ?polyprop:bool -> mind_specif puniverses -> types Lazy.t array -> types + ?polyprop:bool -> mind_specif puniverses -> param_univs -> types val elim_sort : mind_specif -> Sorts.family @@ -117,8 +123,8 @@ exception SingletonInductiveBecomesProp of Id.t val max_inductive_sort : Sorts.t array -> Universe.t -val instantiate_universes : env -> Constr.rel_context -> - template_arity -> constr Lazy.t array -> Constr.rel_context * Sorts.t +val instantiate_universes : Constr.rel_context -> + template_arity -> param_univs -> Constr.rel_context * Sorts.t (** {6 Debug} *) diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 0a654adf7f..11c455de73 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -150,8 +150,8 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 (* nparams done *) (* params_ctxt done because part of the inductive types *) (* Don't check the sort of the type if polymorphic *) - let ty1 = type_of_inductive env ((mib1, p1), inst) in - let ty2 = type_of_inductive env ((mib2, p2), inst) in + let ty1 = type_of_inductive ((mib1, p1), inst) in + let ty2 = type_of_inductive ((mib2, p2), inst) in let cst = check_inductive_type cst p2.mind_typename ty1 ty2 in cst in diff --git a/kernel/term.ml b/kernel/term.ml index 87678b911e..a2586e74f7 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -363,24 +363,3 @@ let rec isArity c = | Cast (c,_,_) -> isArity c | Sort _ -> true | _ -> false - -(** Kind of type *) - -(* Experimental, used in Presburger contrib *) -type ('constr, 'types) kind_of_type = - | SortType of Sorts.t - | CastType of 'types * 'types - | ProdType of Name.t Context.binder_annot * 'types * 'types - | LetInType of Name.t Context.binder_annot * 'constr * 'types * 'types - | AtomicType of 'constr * 'constr array - -let kind_of_type t = match kind t with - | Sort s -> SortType s - | Cast (c,_,t) -> CastType (c, t) - | Prod (na,t,c) -> ProdType (na, t, c) - | LetIn (na,b,t,c) -> LetInType (na, b, t, c) - | App (c,l) -> AtomicType (c, l) - | (Rel _ | Meta _ | Var _ | Evar _ | Const _ - | Proj _ | Case _ | Fix _ | CoFix _ | Ind _) - -> AtomicType (t,[||]) - | (Lambda _ | Construct _ | Int _ | Float _) -> failwith "Not a type" diff --git a/kernel/term.mli b/kernel/term.mli index d2de4177ce..1fef54257a 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -181,17 +181,6 @@ val destArity : types -> arity (** Tell if a term has the form of an arity *) val isArity : types -> bool -(** {5 Kind of type} *) - -type ('constr, 'types) kind_of_type = - | SortType of Sorts.t - | CastType of 'types * 'types - | ProdType of Name.t Context.binder_annot * 'types * 'types - | LetInType of Name.t Context.binder_annot * 'constr * 'types * 'types - | AtomicType of 'constr * 'constr array - -val kind_of_type : types -> (constr, types) kind_of_type - (* Deprecated *) type sorts_family = Sorts.family = InSProp | InProp | InSet | InType [@@ocaml.deprecated "Alias for Sorts.family"] diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 2a35f87db8..80accc1ced 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -372,7 +372,7 @@ let type_of_inductive_knowing_parameters env (ind,u) args = let (mib,_mip) as spec = lookup_mind_specif env ind in check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps; let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters - env (spec,u) args + (spec,u) (Inductive.make_param_univs env args) in check_constraints cst env; t @@ -380,7 +380,7 @@ let type_of_inductive_knowing_parameters env (ind,u) args = let type_of_inductive env (ind,u) = let (mib,mip) = lookup_mind_specif env ind in check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps; - let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in + let t,cst = Inductive.constrained_type_of_inductive ((mib,mip),u) in check_constraints cst env; t @@ -461,8 +461,7 @@ let type_of_global_in_context env r = let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in let univs = Declareops.inductive_polymorphic_context mib in let inst = Univ.make_abstract_instance univs in - let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in - Inductive.type_of_inductive env (specif, inst), univs + Inductive.type_of_inductive (specif, inst), univs | ConstructRef cstr -> let (mib,_ as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) @@ -515,8 +514,7 @@ let rec execute env cstr = let f', ft = match kind f with | Ind ind when Environ.template_polymorphic_pind ind env -> - let args = Array.map (fun t -> lazy t) argst in - f, type_of_inductive_knowing_parameters env ind args + f, type_of_inductive_knowing_parameters env ind argst | _ -> (* No template polymorphism *) execute env f diff --git a/library/goptions.ml b/library/goptions.ml index 6e53bed349..616f6edf72 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -27,7 +27,6 @@ type option_value = (** Summary of an option status *) type option_state = { opt_depr : bool; - opt_name : string; opt_value : option_value; } @@ -190,7 +189,6 @@ module MakeRefTable = type 'a option_sig = { optdepr : bool; - optname : string; optkey : option_name; optread : unit -> 'a; optwrite : 'a -> unit } @@ -229,7 +227,7 @@ let warn_deprecated_option = strbrk " is deprecated") let declare_option cast uncast append ?(preprocess = fun x -> x) - { optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } = + { optdepr=depr; optkey=key; optread=read; optwrite=write } = check_key key; let default = read() in let change = @@ -275,7 +273,7 @@ let declare_option cast uncast append ?(preprocess = fun x -> x) let cread () = cast (read ()) in let cwrite l v = warn (); change l OptSet (uncast v) in let cappend l v = warn (); change l OptAppend (uncast v) in - value_tab := OptionMap.add key (name, depr, (cread,cwrite,cappend)) !value_tab + value_tab := OptionMap.add key (depr, (cread,cwrite,cappend)) !value_tab let declare_int_option = declare_option @@ -298,13 +296,12 @@ let declare_stringopt_option = (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option.")) (fun _ _ -> anomaly (Pp.str "async_option.")) -let declare_bool_option_and_ref ~depr ~name ~key ~(value:bool) = +let declare_bool_option_and_ref ~depr ~key ~(value:bool) = let r_opt = ref value in let optwrite v = r_opt := v in let optread () = !r_opt in let _ = declare_bool_option { optdepr = depr; - optname = name; optkey = key; optread; optwrite } in @@ -323,7 +320,7 @@ let set_option_value ?(locality = OptDefault) check_and_cast key v = let opt = try Some (get_option key) with Not_found -> None in match opt with | None -> warn_unknown_option key - | Some (name, depr, (read,write,append)) -> + | Some (depr, (read,write,append)) -> write locality (check_and_cast v (read ())) let show_value_type = function @@ -373,7 +370,7 @@ let set_string_option_append_value_gen ?(locality = OptDefault) key v = let opt = try Some (get_option key) with Not_found -> None in match opt with | None -> warn_unknown_option key - | Some (name, depr, (read,write,append)) -> + | Some (depr, (read,write,append)) -> append locality (check_string_value v (read ())) let set_int_option_value opt v = set_int_option_value_gen opt v @@ -382,7 +379,7 @@ let set_string_option_value opt v = set_string_option_value_gen opt v (* Printing options/tables *) -let msg_option_value (name,v) = +let msg_option_value v = match v with | BoolValue true -> str "on" | BoolValue false -> str "off" @@ -394,19 +391,18 @@ let msg_option_value (name,v) = (* | IdentValue r -> pr_global_env Id.Set.empty r *) let print_option_value key = - let (name, depr, (read,_,_)) = get_option key in + let (depr, (read,_,_)) = get_option key in let s = read () in match s with | BoolValue b -> - Feedback.msg_notice (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off")) + Feedback.msg_notice (prlist_with_sep spc str key ++ str " is " ++ str (if b then "on" else "off")) | _ -> - Feedback.msg_notice (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s)) + Feedback.msg_notice (str "Current value of " ++ prlist_with_sep spc str key ++ str " is " ++ msg_option_value s) let get_tables () = let tables = !value_tab in - let fold key (name, depr, (read,_,_)) accu = + let fold key (depr, (read,_,_)) accu = let state = { - opt_name = name; opt_depr = depr; opt_value = read (); } in @@ -415,15 +411,15 @@ let get_tables () = OptionMap.fold fold tables OptionMap.empty let print_tables () = - let print_option key name value depr = - let msg = str " " ++ str (nickname key) ++ str ": " ++ msg_option_value (name, value) in + let print_option key value depr = + let msg = str " " ++ str (nickname key) ++ str ": " ++ msg_option_value value in if depr then msg ++ str " [DEPRECATED]" ++ fnl () else msg ++ fnl () in str "Options:" ++ fnl () ++ OptionMap.fold - (fun key (name, depr, (read,_,_)) p -> - p ++ print_option key name (read ()) depr) + (fun key (depr, (read,_,_)) p -> + p ++ print_option key (read ()) depr) !value_tab (mt ()) ++ str "Tables:" ++ fnl () ++ List.fold_right diff --git a/library/goptions.mli b/library/goptions.mli index 29af196654..e3791dffb1 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -111,8 +111,6 @@ end type 'a option_sig = { optdepr : bool; (** whether the option is DEPRECATED *) - optname : string; - (** a short string describing the option *) optkey : option_name; (** the low-level name of this option *) optread : unit -> 'a; @@ -133,7 +131,7 @@ val declare_stringopt_option: ?preprocess:(string option -> string option) -> (** Helper to declare a reference controlled by an option. Read-only as to avoid races. *) -val declare_bool_option_and_ref : depr:bool -> name:string -> key:option_name -> value:bool -> (unit -> bool) +val declare_bool_option_and_ref : depr:bool -> key:option_name -> value:bool -> (unit -> bool) (** {6 Special functions supposed to be used only in vernacentries.ml } *) @@ -181,7 +179,6 @@ val set_option_value : ?locality:option_locality -> (** Summary of an option status *) type option_state = { opt_depr : bool; - opt_name : string; opt_value : option_value; } diff --git a/man/coqdep.1 b/man/coqdep.1 index 4223482c99..0770ce88c8 100644 --- a/man/coqdep.1 +++ b/man/coqdep.1 @@ -12,9 +12,6 @@ coqdep \- Compute inter-module dependencies for Coq and Caml programs .BI \-coqlib \ directory ] [ -.BI \-c -] -[ .BI \-i ] [ @@ -52,10 +49,6 @@ directives and the dot notation .SH OPTIONS .TP -.BI \-c -Prints the dependencies of Caml modules. -(On Caml modules, the behaviour is exactly the same as ocamldep). -.TP .BI \-f \ file Read filenames and options -I, -R and -Q from a _CoqProject FILE. .TP @@ -152,29 +145,8 @@ example% coqdep \-I . *.v .fi .RE .br -.ne 7 -.LP -To get only the Caml dependencies: -.IP -.B -example% coqdep \-c \-I . *.ml -.RS -.sp .5 -.nf -.B D.cmo: D.ml ./A.cmo ./B.cmo ./C.cmo -.B D.cmx: D.ml ./A.cmx ./B.cmx ./C.cmx -.B C.cmo: C.ml -.B C.cmx: C.ml -.B B.cmo: B.ml -.B B.cmx: B.ml -.B A.cmo: A.ml -.B A.cmx: A.ml -.fi -.RE -.br -.ne 7 .SH BUGS Please report any bug to -.B coq\-bugs@pauillac.inria.fr +.B https://github.com/coq/coq/issues diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index fdc70ccaa8..f9078c4bdc 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -33,7 +33,6 @@ let debug x = let () = let gdopt= { optdepr=false; - optname="Congruence Verbose"; optkey=["Congruence";"Verbose"]; optread=(fun ()-> !cc_verbose); optwrite=(fun b -> cc_verbose := b)} diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index a4469b7ec1..9b30ddd958 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -437,7 +437,7 @@ and extract_really_ind env kn mib = Array.mapi (fun i mip -> let (_,u),_ = UnivGen.fresh_inductive_instance env (kn,i) in - let ar = Inductive.type_of_inductive env ((mib,mip),u) in + let ar = Inductive.type_of_inductive ((mib,mip),u) in let ar = EConstr.of_constr ar in let info = (fst (flag_of_type env sg ar) = Info) in let s,v = if info then type_sign_vl env sg ar else [],[] in @@ -526,7 +526,7 @@ and extract_really_ind env kn mib = (* Is this record officially declared with its projections ? *) (* If so, we use this information. *) begin try - let ty = Inductive.type_of_inductive env ((mib,mip0),u) in + let ty = Inductive.type_of_inductive ((mib,mip0),u) in let n = nb_default_params env sg (EConstr.of_constr ty) in let check_proj kn = if Cset.mem kn !projs then add_projection n kn ip in diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 7b64706138..9d07cd7d93 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -503,7 +503,6 @@ let my_bool_option name initval = let access = fun () -> !flag in let () = declare_bool_option {optdepr = false; - optname = "Extraction "^name; optkey = ["Extraction"; name]; optread = access; optwrite = (:=) flag } @@ -575,14 +574,12 @@ let optims () = !opt_flag_ref let () = declare_bool_option {optdepr = false; - optname = "Extraction Optimize"; optkey = ["Extraction"; "Optimize"]; optread = (fun () -> not (Int.equal !int_flag_ref 0)); optwrite = (fun b -> chg_flag (if b then int_flag_init else 0))} let () = declare_int_option { optdepr = false; - optname = "Extraction Flag"; optkey = ["Extraction";"Flag"]; optread = (fun _ -> Some !int_flag_ref); optwrite = (function @@ -596,7 +593,6 @@ let conservative_types () = !conservative_types_ref let () = declare_bool_option {optdepr = false; - optname = "Extraction Conservative Types"; optkey = ["Extraction"; "Conservative"; "Types"]; optread = (fun () -> !conservative_types_ref); optwrite = (fun b -> conservative_types_ref := b) } @@ -608,7 +604,6 @@ let file_comment () = !file_comment_ref let () = declare_string_option {optdepr = false; - optname = "Extraction File Comment"; optkey = ["Extraction"; "File"; "Comment"]; optread = (fun () -> !file_comment_ref); optwrite = (fun s -> file_comment_ref := s) } diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index 9d208e1c86..930801f6fd 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/plugins/firstorder/g_ground.mlg @@ -36,7 +36,6 @@ let ground_depth=ref 3 let ()= let gdopt= { optdepr=false; - optname="Firstorder Depth"; optkey=["Firstorder";"Depth"]; optread=(fun ()->Some !ground_depth); optwrite= diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 84f09c385f..fdbad2ab9e 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1512,12 +1512,12 @@ let do_build_inductive let _time3 = System.get_time () in (* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) let repacked_rel_inds = - List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) + List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c, Vernacexpr.Constructors l),ntn ) rel_inds in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)}) + Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Vernacexpr.Inductive_kw,repacked_rel_inds)}) ++ fnl () ++ msg in @@ -1527,12 +1527,12 @@ let do_build_inductive let _time3 = System.get_time () in (* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) let repacked_rel_inds = - List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) + List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c, Vernacexpr.Constructors l),ntn ) rel_inds in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)}) + Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Vernacexpr.Inductive_kw,repacked_rel_inds)}) ++ fnl () ++ CErrors.print reraise in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index bce09d8fbd..b2ee0f9370 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -320,7 +320,6 @@ open Goptions let functional_induction_rewrite_dependent_proofs_sig = { optdepr = false; - optname = "Functional Induction Rewrite Dependent"; optkey = ["Functional";"Induction";"Rewrite";"Dependent"]; optread = (fun () -> !functional_induction_rewrite_dependent_proofs); optwrite = (fun b -> functional_induction_rewrite_dependent_proofs := b) @@ -332,7 +331,6 @@ let do_rewrite_dependent () = !functional_induction_rewrite_dependent_proofs = t let function_debug_sig = { optdepr = false; - optname = "Function debug"; optkey = ["Function_debug"]; optread = (fun () -> !function_debug); optwrite = (fun b -> function_debug := b) @@ -416,7 +414,6 @@ let is_strict_tcc () = !strict_tcc let strict_tcc_sig = { optdepr = false; - optname = "Raw Function Tcc"; optkey = ["Function_raw_tcc"]; optread = (fun () -> !strict_tcc); optwrite = (fun b -> strict_tcc := b) diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 81a6651745..7ea843ca69 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -368,7 +368,6 @@ let print_info_trace = ref None let () = declare_int_option { optdepr = false; - optname = "print info trace"; optkey = ["Info" ; "Level"]; optread = (fun () -> !print_info_trace); optwrite = fun n -> print_info_trace := n; diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index fe5ebf1172..7529f9fce6 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -450,7 +450,6 @@ let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "Ltac Profiling"; optkey = ["Ltac"; "Profiling"]; optread = get_profiling; optwrite = set_profiling } diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 98aa649b62..6e620b71db 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2082,7 +2082,6 @@ let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "Ltac debug"; optkey = ["Ltac";"Debug"]; optread = (fun () -> get_debug () != Tactic_debug.DebugOff); optwrite = vernac_debug } @@ -2091,7 +2090,6 @@ let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "Ltac Backtrace"; optkey = ["Ltac"; "Backtrace"]; optread = (fun () -> !log_trace); optwrite = (fun b -> log_trace := b) } diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 539536911c..0e9465839a 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -86,7 +86,6 @@ open Goptions let () = declare_bool_option { optdepr = false; - optname = "Ltac batch debug"; optkey = ["Ltac";"Batch";"Debug"]; optread = (fun () -> !batch); optwrite = (fun x -> batch := x) } diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index ba759441e5..92110d7a43 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -68,7 +68,6 @@ open Goptions let () = declare_bool_option { optdepr = false; - optname = "unfolding of not in intuition"; optkey = ["Intuition";"Negation";"Unfolding"]; optread = (fun () -> !negation_unfolding); optwrite = (:=) negation_unfolding } diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index cdadde8621..4b656f8e61 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -55,7 +55,6 @@ let use_csdp_cache = ref true let () = let int_opt l vref = { optdepr = false - ; optname = List.fold_right ( ^ ) l "" ; optkey = l ; optread = (fun () -> Some !vref) ; optwrite = @@ -63,42 +62,36 @@ let () = in let lia_enum_opt = { optdepr = false - ; optname = "Lia Enum" ; optkey = ["Lia"; "Enum"] ; optread = (fun () -> !lia_enum) ; optwrite = (fun x -> lia_enum := x) } in let solver_opt = { optdepr = false - ; optname = "Use the Simplex instead of Fourier elimination" ; optkey = ["Simplex"] ; optread = (fun () -> !Certificate.use_simplex) ; optwrite = (fun x -> Certificate.use_simplex := x) } in let dump_file_opt = { optdepr = false - ; optname = "Generate Coq goals in file from calls to 'lia' 'nia'" ; optkey = ["Dump"; "Arith"] ; optread = (fun () -> !Certificate.dump_file) ; optwrite = (fun x -> Certificate.dump_file := x) } in let lia_cache_opt = { optdepr = false - ; optname = "cache of lia (.lia.cache)" ; optkey = ["Lia"; "Cache"] ; optread = (fun () -> !use_lia_cache) ; optwrite = (fun x -> use_lia_cache := x) } in let nia_cache_opt = { optdepr = false - ; optname = "cache of nia (.nia.cache)" ; optkey = ["Nia"; "Cache"] ; optread = (fun () -> !use_nia_cache) ; optwrite = (fun x -> use_nia_cache := x) } in let nra_cache_opt = { optdepr = false - ; optname = "cache of nra (.nra.cache)" ; optkey = ["Nra"; "Cache"] ; optread = (fun () -> !use_nra_cache) ; optwrite = (fun x -> use_nra_cache := x) } diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 979e5bb8d8..118db01ecb 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -67,7 +67,6 @@ open Goptions let () = declare_bool_option { optdepr = false; - optname = "Omega system time displaying flag"; optkey = ["Omega";"System"]; optread = read display_system_flag; optwrite = write display_system_flag } @@ -75,7 +74,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "Omega action display flag"; optkey = ["Omega";"Action"]; optread = read display_action_flag; optwrite = write display_action_flag } @@ -83,7 +81,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "Omega old style flag"; optkey = ["Omega";"OldStyle"]; optread = read old_style_flag; optwrite = write old_style_flag } @@ -91,7 +88,6 @@ let () = let () = declare_bool_option { optdepr = true; - optname = "Omega automatic reset of generated names"; optkey = ["Stable";"Omega"]; optread = read reset_flag; optwrite = write reset_flag } @@ -99,7 +95,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "Omega takes advantage of context variables with body"; optkey = ["Omega";"UseLocalDefs"]; optread = read letin_flag; optwrite = write letin_flag } diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 4cc32cfb26..ab34489de9 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -49,7 +49,6 @@ let pruning = ref true let opt_pruning= {optdepr=false; - optname="Rtauto Pruning"; optkey=["Rtauto";"Pruning"]; optread=(fun () -> !pruning); optwrite=(fun b -> pruning:=b)} diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 0c155c9d0a..b86c8d096c 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -227,7 +227,6 @@ let verbose = ref false let opt_verbose= {optdepr=false; - optname="Rtauto Verbose"; optkey=["Rtauto";"Verbose"]; optread=(fun () -> !verbose); optwrite=(fun b -> verbose:=b)} @@ -238,7 +237,6 @@ let check = ref false let opt_check= {optdepr=false; - optname="Rtauto Check"; optkey=["Rtauto";"Check"]; optread=(fun () -> !check); optwrite=(fun b -> check:=b)} diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index de3c660938..f95672a15d 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -906,10 +906,11 @@ let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty = | _ -> (mkCCast ty (mkCType None)).v)) ty in mk_term ' ' (force_type ty) in let strip_cast (sigma, t) = - let rec aux t = match EConstr.kind_of_type sigma t with - | CastType (t, ty) when !n_binders = 0 && EConstr.isSort sigma ty -> t - | ProdType(n,s,t) -> decr n_binders; EConstr.mkProd (n, s, aux t) - | LetInType(n,v,ty,t) -> decr n_binders; EConstr.mkLetIn (n, v, ty, aux t) + let open EConstr in + let rec aux t = match kind_of_type sigma t with + | CastType (t, ty) when !n_binders = 0 && isSort sigma ty -> t + | ProdType(n,s,t) -> decr n_binders; mkProd (n, s, aux t) + | LetInType(n,v,ty,t) -> decr n_binders; mkLetIn (n, v, ty, aux t) | _ -> anomaly "pf_interp_ty: ssr Type cast deleted by typecheck" in sigma, aux t in let sigma, cty as ty = strip_cast (interp_term ist gl ty) in @@ -930,11 +931,12 @@ exception NotEnoughProducts let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_of env sigma c) m = let rec loop ty args sigma n = + let open EConstr in if n = 0 then let args = List.rev args in (if beta then Reductionops.whd_beta sigma else fun x -> x) (EConstr.mkApp (c, Array.of_list (List.map snd args))), ty, args, sigma - else match EConstr.kind_of_type sigma ty with + else match kind_of_type sigma ty with | ProdType (_, src, tgt) -> let sigma = create_evar_defs sigma in let (sigma, x) = @@ -947,7 +949,7 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_ | AtomicType _ -> let ty = (* FIXME *) (Reductionops.whd_all env sigma) ty in - match EConstr.kind_of_type sigma ty with + match kind_of_type sigma ty with | ProdType _ -> loop ty args sigma n | _ -> raise NotEnoughProducts in diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 26962ee87b..7baccd3d75 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -13,7 +13,6 @@ open Util open Names open Printer -open Term open Constr open Context open Termops @@ -35,16 +34,17 @@ module RelDecl = Context.Rel.Declaration * argument (index), it computes it's arity and the arity of the eliminator and * checks if the eliminator is recursive or not *) let analyze_eliminator elimty env sigma = - let rec loop ctx t = match EConstr.kind_of_type sigma t with - | AtomicType (hd, args) when EConstr.isRel sigma hd -> - ctx, EConstr.destRel sigma hd, not (EConstr.Vars.noccurn sigma 1 t), Array.length args, t + let open EConstr in + let rec loop ctx t = match kind_of_type sigma t with + | AtomicType (hd, args) when isRel sigma hd -> + ctx, destRel sigma hd, not (Vars.noccurn sigma 1 t), Array.length args, t | CastType (t, _) -> loop ctx t | ProdType (x, ty, t) -> loop (RelDecl.LocalAssum (x, ty) :: ctx) t - | LetInType (x,b,ty,t) -> loop (RelDecl.LocalDef (x, b, ty) :: ctx) (EConstr.Vars.subst1 b t) + | LetInType (x,b,ty,t) -> loop (RelDecl.LocalDef (x, b, ty) :: ctx) (Vars.subst1 b t) | _ -> - let env' = EConstr.push_rel_context ctx env in + let env' = push_rel_context ctx env in let t' = Reductionops.whd_all env' sigma t in - if not (EConstr.eq_constr sigma t t') then loop ctx t' else + if not (eq_constr sigma t t') then loop ctx t' else errorstrm Pp.(str"The eliminator has the wrong shape."++spc()++ str"A (applied) bound variable was expected as the conclusion of "++ str"the eliminator's"++Pp.cut()++str"type:"++spc()++pr_econstr_env env' sigma elimty) in @@ -243,7 +243,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let sigma = project gl in ppdebug(lazy Pp.(str"elim= "++ pr_econstr_pat env sigma elim)); ppdebug(lazy Pp.(str"elimty= "++ pr_econstr_pat env sigma elimty)) in - let inf_deps_r = match EConstr.kind_of_type (project gl) elimty with + let open EConstr in + let inf_deps_r = match kind_of_type (project gl) elimty with | AtomicType (_, args) -> List.rev (Array.to_list args) | _ -> assert false in let saturate_until gl c c_ty f = diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index cdda84a18d..895f491510 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -13,7 +13,6 @@ open Ltac_plugin open Util open Names -open Term open Constr open Context open Vars @@ -34,8 +33,7 @@ open Tacmach let ssroldreworder = Summary.ref ~name:"SSR:oldreworder" false let () = Goptions.(declare_bool_option - { optname = "ssreflect 1.3 compatibility flag"; - optkey = ["SsrOldRewriteGoalsOrder"]; + { optkey = ["SsrOldRewriteGoalsOrder"]; optread = (fun _ -> !ssroldreworder); optdepr = false; optwrite = (fun b -> ssroldreworder := b) }) @@ -380,7 +378,8 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_ let hd_ty = Retyping.get_type_of env sigma hd in let names = let rec aux t = function 0 -> [] | n -> let t = Reductionops.whd_all env sigma t in - match EConstr.kind_of_type sigma t with + let open EConstr in + match kind_of_type sigma t with | ProdType (name, _, t) -> name.binder_name :: aux t (n-1) | _ -> assert false in aux hd_ty (Array.length args) in hd_ty, Util.List.map_filter (fun (t, name) -> @@ -413,7 +412,8 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl = let env, sigma, c, c_eq = pf_env gl, fst sr, snd sr, Coqlib.(lib_ref "core.eq.type") in let sigma, c_ty = Typing.type_of env sigma c in ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty)); - match EConstr.kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with + let open EConstr in + match kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with | AtomicType(e, a) when Ssrcommon.is_ind_ref sigma e c_eq -> let new_rdx = if dir = L2R then a.(2) else a.(1) in pirrel_rewrite ?under ?map_redex cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index f486d1e457..a6b9a43778 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -69,8 +69,7 @@ let ssrhaveNOtcresolution = Summary.ref ~name:"SSR:havenotcresolution" false let () = Goptions.(declare_bool_option - { optname = "have type classes"; - optkey = ["SsrHave";"NoTCResolution"]; + { optkey = ["SsrHave";"NoTCResolution"]; optread = (fun _ -> !ssrhaveNOtcresolution); optdepr = false; optwrite = (fun b -> ssrhaveNOtcresolution := b); @@ -362,8 +361,9 @@ let intro_lock ipats = let c = Proofview.Goal.concl gl in let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in - match EConstr.kind_of_type sigma c with - | Term.AtomicType(hd, args) when + let open EConstr in + match kind_of_type sigma c with + | AtomicType(hd, args) when Array.length args >= 2 && is_app_evar sigma (Array.last args) && Ssrequality.ssr_is_setoid env sigma hd args (* if the last condition above [ssr_is_setoid ...] holds @@ -376,8 +376,8 @@ let intro_lock ipats = protect_subgoal env sigma hd args | _ -> let t = Reductionops.whd_all env sigma c in - match EConstr.kind_of_type sigma t with - | Term.AtomicType(hd, args) when + match kind_of_type sigma t with + | AtomicType(hd, args) when Ssrcommon.is_ind_ref sigma hd (Coqlib.lib_ref "core.eq.type") && Array.length args = 3 && is_app_evar sigma args.(2) -> protect_subgoal env sigma hd args diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 580c0423e9..843adb40ac 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -610,8 +610,9 @@ let tclCompileIPats = IpatMachine.tclCompileIPats let with_defective maintac deps clr = Goal.enter begin fun g -> let sigma, concl = Goal.(sigma g, concl g) in let top_id = - match EConstr.kind_of_type sigma concl with - | Term.ProdType ({binder_name=Name id}, _, _) + let open EConstr in + match kind_of_type sigma concl with + | ProdType ({binder_name=Name id}, _, _) when Ssrcommon.is_discharged_id id -> id | _ -> Ssrcommon.top_id in let top_gen = Ssrequality.mkclr clr, Ssrmatching.cpattern_of_id top_id in @@ -641,10 +642,11 @@ let elim_intro_tac ipats ?seed what eqid ssrelim is_rec clr = | Some (IPatId ipat) when not is_rec -> let rec intro_eq () = Goal.enter begin fun g -> let sigma, env, concl = Goal.(sigma g, env g, concl g) in - match EConstr.kind_of_type sigma concl with - | Term.ProdType (_, src, tgt) -> begin - match EConstr.kind_of_type sigma src with - | Term.AtomicType (hd, _) when Ssrcommon.is_protect hd env sigma -> + let open EConstr in + match kind_of_type sigma concl with + | ProdType (_, src, tgt) -> begin + match kind_of_type sigma src with + | AtomicType (hd, _) when Ssrcommon.is_protect hd env sigma -> V82.tactic ~nf_evars:false Ssrcommon.unprotecttac <*> Ssrcommon.tclINTRO_ID ipat | _ -> Ssrcommon.tclINTRO_ANON () <*> intro_eq () @@ -669,8 +671,9 @@ let elim_intro_tac ipats ?seed what eqid ssrelim is_rec clr = let sigma, eq = EConstr.fresh_global env sigma (Coqlib.lib_ref "core.eq.type") in let ctx, last = EConstr.decompose_prod_assum sigma concl in - let args = match EConstr.kind_of_type sigma last with - | Term.AtomicType (hd, args) -> + let open EConstr in + let args = match kind_of_type sigma last with + | AtomicType (hd, args) -> if Ssrcommon.is_protect hd env sigma then args else Ssrcommon.errorstrm (Pp.str "Too many names in intro pattern") diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 22325f3fc3..21b832a326 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -1662,8 +1662,7 @@ let ssr_reserved_ids = Summary.ref ~name:"SSR:idents" true let () = Goptions.(declare_bool_option - { optname = "ssreflect identifiers"; - optkey = ["SsrIdents"]; + { optkey = ["SsrIdents"]; optdepr = false; optread = (fun _ -> !ssr_reserved_ids); optwrite = (fun b -> ssr_reserved_ids := b) @@ -2395,8 +2394,7 @@ let ssr_rw_syntax = Summary.ref ~name:"SSR:rewrite" true let () = Goptions.(declare_bool_option - { optname = "ssreflect rewrite"; - optkey = ["SsrRewrite"]; + { optkey = ["SsrRewrite"]; optread = (fun _ -> !ssr_rw_syntax); optdepr = false; optwrite = (fun b -> ssr_rw_syntax := b) }) diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index f0aed1a934..22250202b5 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -134,8 +134,7 @@ let ppdebug_ref = ref (fun _ -> ()) let ssr_pp s = Feedback.msg_debug (str"SSR: "++Lazy.force s) let () = Goptions.(declare_bool_option - { optname = "ssreflect debugging"; - optkey = ["Debug";"Ssreflect"]; + { optkey = ["Debug";"Ssreflect"]; optdepr = false; optread = (fun _ -> !ppdebug_ref == ssr_pp); optwrite = (fun b -> diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index f91b5e7aa2..d051836ebc 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -95,8 +95,9 @@ applied to the first assumption in the goal *) let vsBOOTSTRAP = Goal.enter_one ~__LOC__ begin fun gl -> let concl = Goal.concl gl in let id = (* We keep the orig name for checks in "in" tcl *) - match EConstr.kind_of_type (Goal.sigma gl) concl with - | Term.ProdType({binder_name=Name.Name id}, _, _) + let open EConstr in + match kind_of_type (Goal.sigma gl) concl with + | ProdType({binder_name=Name.Name id}, _, _) when Ssrcommon.is_discharged_id id -> id | _ -> mk_anon_id "view_subject" (Tacmach.New.pf_ids_of_hyps gl) in let view = EConstr.mkVar id in diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 915531cf3c..e45bae19ca 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -54,8 +54,7 @@ let debug b = if b then pp_ref := ssr_pp else pp_ref := fun _ -> () let _ = Goptions.declare_bool_option - { Goptions.optname = "ssrmatching debugging"; - Goptions.optkey = ["Debug";"SsrMatching"]; + { Goptions.optkey = ["Debug";"SsrMatching"]; Goptions.optdepr = false; Goptions.optread = (fun _ -> !pp_ref == ssr_pp); Goptions.optwrite = debug } diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 36f35a67c3..59ca418a39 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -11,7 +11,6 @@ (*i*) open Names open Globnames -open Term open Constr open Context open Environ @@ -78,14 +77,14 @@ let rename_type ty ref = let rec rename_type_aux c = function | [] -> c | rename :: rest as renamings -> - match kind_of_type c with - | ProdType (old, s, t) -> + match Constr.kind c with + | Prod (old, s, t) -> mkProd (name_override old rename, s, rename_type_aux t rest) - | LetInType(old, s, b, t) -> + | LetIn (old, s, b, t) -> mkLetIn (old ,s, b, rename_type_aux t renamings) - | CastType (t,_) -> rename_type_aux t renamings - | SortType _ -> c - | AtomicType _ -> c in + | Cast (t,_, _) -> rename_type_aux t renamings + | _ -> c + in try rename_type_aux ty (arguments_names ref) with Not_found -> ty diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 2b7ccbbcad..11c97221ec 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -196,7 +196,6 @@ let cofixp_reducible flgs _ stk = let get_debug_cbv = Goptions.declare_bool_option_and_ref ~depr:false ~value:false - ~name:"cbv visited constants display" ~key:["Debug";"Cbv"] (* Reduction of primitives *) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 3c7f9a8f00..c4aa3479bf 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -36,7 +36,6 @@ open Globnames let get_use_typeclasses_for_conversion = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"use typeclass resolution during conversion" ~key:["Typeclass"; "Resolution"; "For"; "Conversion"] ~value:true diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index b042437a22..83078660c5 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -228,7 +228,6 @@ let force_wildcard () = !wildcard_value let () = declare_bool_option { optdepr = false; - optname = "forced wildcard"; optkey = ["Printing";"Wildcard"]; optread = force_wildcard; optwrite = (:=) wildcard_value } @@ -237,7 +236,6 @@ let fast_name_generation = ref false let () = declare_bool_option { optdepr = false; - optname = "fast bound name generation algorithm"; optkey = ["Fast";"Name";"Printing"]; optread = (fun () -> !fast_name_generation); optwrite = (:=) fast_name_generation; @@ -248,7 +246,6 @@ let synthetize_type () = !synth_type_value let () = declare_bool_option { optdepr = false; - optname = "pattern matching return type synthesizability"; optkey = ["Printing";"Synth"]; optread = synthetize_type; optwrite = (:=) synth_type_value } @@ -258,7 +255,6 @@ let reverse_matching () = !reverse_matching_value let () = declare_bool_option { optdepr = false; - optname = "pattern-matching reversibility"; optkey = ["Printing";"Matching"]; optread = reverse_matching; optwrite = (:=) reverse_matching_value } @@ -268,7 +264,6 @@ let print_primproj_params () = !print_primproj_params_value let () = declare_bool_option { optdepr = false; - optname = "printing of primitive projection parameters"; optkey = ["Printing";"Primitive";"Projection";"Parameters"]; optread = print_primproj_params; optwrite = (:=) print_primproj_params_value } @@ -348,7 +343,6 @@ let print_factorize_match_patterns = ref true let () = declare_bool_option { optdepr = false; - optname = "factorization of \"match\" patterns in printing"; optkey = ["Printing";"Factorizable";"Match";"Patterns"]; optread = (fun () -> !print_factorize_match_patterns); optwrite = (fun b -> print_factorize_match_patterns := b) } @@ -358,7 +352,6 @@ let print_allow_match_default_clause = ref true let () = declare_bool_option { optdepr = false; - optname = "possible use of \"match\" default pattern in printing"; optkey = ["Printing";"Allow";"Match";"Default";"Clause"]; optread = (fun () -> !print_allow_match_default_clause); optwrite = (fun b -> print_allow_match_default_clause := b) } diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index c21af82659..c67019c7ac 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -50,8 +50,6 @@ let default_flags env = let debug_unification = ref (false) let () = Goptions.(declare_bool_option { optdepr = false; - optname = - "Print states sent to Evarconv unification"; optkey = ["Debug";"Unification"]; optread = (fun () -> !debug_unification); optwrite = (fun a -> debug_unification:=a); @@ -60,8 +58,6 @@ let () = Goptions.(declare_bool_option { let debug_ho_unification = ref (false) let () = Goptions.(declare_bool_option { optdepr = false; - optname = - "Print higher-order unification debug information"; optkey = ["Debug";"HO";"Unification"]; optread = (fun () -> !debug_ho_unification); optwrite = (fun a -> debug_ho_unification:=a); diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 816a8c4703..a4406aeba1 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -29,7 +29,7 @@ open Context.Rel.Declaration let type_of_inductive env (ind,u) = let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in Typeops.check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps; - Inductive.type_of_inductive env (specif,u) + Inductive.type_of_inductive (specif,u) (* Return type as quoted by the user *) let type_of_constructor env (cstr,u) = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 2d98d48aa0..ac1a4e88ef 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -125,7 +125,6 @@ let esearch_guard ?loc env sigma indexes fix = let is_strict_universe_declarations = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"strict universe declaration" ~key:["Strict";"Universe";"Declaration"] ~value:true diff --git a/pretyping/program.ml b/pretyping/program.ml index 1bc31646dd..9c478844aa 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -78,7 +78,6 @@ open Goptions let () = declare_bool_option { optdepr = false; - optname = "preferred transparency of Program obligations"; optkey = ["Transparent";"Obligations"]; optread = get_proofs_transparency; optwrite = set_proofs_transparency; } @@ -86,7 +85,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "program cases"; optkey = ["Program";"Cases"]; optread = (fun () -> !program_cases); optwrite = (:=) program_cases } @@ -94,7 +92,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "program generalized coercion"; optkey = ["Program";"Generalized";"Coercion"]; optread = (fun () -> !program_generalized_coercion); optwrite = (:=) program_generalized_coercion } diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index d5beebe690..838bf22c66 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -32,8 +32,6 @@ exception Elimconst let () = Goptions.(declare_bool_option { optdepr = false; - optname = - "Generate weak constraints between Irrelevant universes"; optkey = ["Cumulativity";"Weak";"Constraints"]; optread = (fun () -> not !UState.drop_weak_constraints); optwrite = (fun a -> UState.drop_weak_constraints:=not a); @@ -972,8 +970,6 @@ module CredNative = RedNative(CNativeEntries) let debug_RAKAM = ref (false) let () = Goptions.(declare_bool_option { optdepr = false; - optname = - "Print states of the Reductionops abstract machine"; optkey = ["Debug";"RAKAM"]; optread = (fun () -> !debug_RAKAM); optwrite = (fun a -> debug_RAKAM:=a); @@ -1711,7 +1707,7 @@ let splay_arity env sigma c = let l, c = splay_prod env sigma c in match EConstr.kind sigma c with | Sort s -> l,s - | _ -> invalid_arg "splay_arity" + | _ -> raise Reduction.NotArity let sort_of_arity env sigma c = snd (splay_arity env sigma c) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index e72f5f2793..c539ec55ed 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -236,12 +236,20 @@ val hnf_lam_applist : env -> evar_map -> constr -> constr list -> constr val splay_prod : env -> evar_map -> constr -> (Name.t Context.binder_annot * constr) list * constr val splay_lam : env -> evar_map -> constr -> (Name.t Context.binder_annot * constr) list * constr +val splay_prod_assum : env -> evar_map -> constr -> rel_context * constr + val splay_arity : env -> evar_map -> constr -> (Name.t Context.binder_annot * constr) list * ESorts.t +(** Raises [Reduction.NotArity] *) + val sort_of_arity : env -> evar_map -> constr -> ESorts.t +(** Raises [Reduction.NotArity] *) + val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr +(** Raises [Invalid_argument] *) + val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr -val splay_prod_assum : - env -> evar_map -> constr -> rel_context * constr +(** Raises [Invalid_argument] *) + type 'a miota_args = { mP : constr; (** the result type *) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index d2af957b54..87fe4cfcda 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -168,15 +168,21 @@ let retype ?(polyprop=true) sigma = | _ -> decomp_sort env sigma (type_of env t) and type_of_global_reference_knowing_parameters env c args = - let argtyps = - Array.map (fun c -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma (type_of env c))) args in match EConstr.kind sigma c with | Ind (ind, u) -> let u = EInstance.kind sigma u in let mip = lookup_mind_specif env ind in - EConstr.of_constr (try Inductive.type_of_inductive_knowing_parameters - ~polyprop env (mip, u) argtyps - with Reduction.NotArity -> retype_error NotAnArity) + let paramtyps = Array.map_to_list (fun arg () -> + let t = type_of env arg in + let s = try Reductionops.sort_of_arity env sigma t + with Reduction.NotArity -> retype_error NotAnArity + in + Sorts.univ_of_sort (ESorts.kind sigma s)) + args + in + EConstr.of_constr + (Inductive.type_of_inductive_knowing_parameters + ~polyprop (mip, u) paramtyps) | Construct (cstr, u) -> let u = EInstance.kind sigma u in EConstr.of_constr (type_of_constructor env (cstr, u)) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index d5c8c3bd19..aa2e96c2d7 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -31,7 +31,6 @@ type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen let get_typeclasses_unique_solutions = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"check that typeclasses proof search returns unique solutions" ~key:["Typeclasses";"Unique";"Solutions"] ~value:false diff --git a/pretyping/typing.ml b/pretyping/typing.ml index b4c19775a7..f067c075bf 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -38,8 +38,11 @@ let meta_type evd mv = let inductive_type_knowing_parameters env sigma (ind,u) jl = let u = Unsafe.to_instance u in let mspec = lookup_mind_specif env ind in - let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma j.uj_type)) jl in - Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp + let paramstyp = Array.map_to_list (fun j () -> + let s = Reductionops.sort_of_arity env sigma j.uj_type in + Sorts.univ_of_sort (EConstr.ESorts.kind sigma s)) jl + in + Inductive.type_of_inductive_knowing_parameters (mspec,u) paramstyp let type_judgment env sigma j = match EConstr.kind sigma (whd_all env sigma j.uj_type) with @@ -307,7 +310,7 @@ let type_of_inductive env sigma (ind,u) = let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in let () = check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in let u = EInstance.kind sigma u in - let ty, csts = Inductive.constrained_type_of_inductive env (specif,u) in + let ty, csts = Inductive.constrained_type_of_inductive (specif,u) in let sigma = Evd.add_constraints sigma csts in sigma, (EConstr.of_constr (rename_type ty (GR.IndRef ind))) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 2157c4ef6a..5b87603d54 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -46,7 +46,6 @@ module NamedDecl = Context.Named.Declaration let keyed_unification = ref (false) let () = Goptions.(declare_bool_option { optdepr = false; - optname = "Unification is keyed"; optkey = ["Keyed";"Unification"]; optread = (fun () -> !keyed_unification); optwrite = (fun a -> keyed_unification:=a); @@ -57,8 +56,6 @@ let is_keyed_unification () = !keyed_unification let debug_unification = ref (false) let () = Goptions.(declare_bool_option { optdepr = false; - optname = - "Print states sent to tactic unification"; optkey = ["Debug";"Tactic";"Unification"]; optread = (fun () -> !debug_unification); optwrite = (fun a -> debug_unification:=a); diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 885fc8980d..b04e59734d 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -98,7 +98,7 @@ let construct_of_constr_const env tag typ = let construct_of_constr_block = construct_of_constr false let type_of_ind env (ind, u) = - type_of_inductive env (Inductive.lookup_mind_specif env ind, u) + type_of_inductive (Inductive.lookup_mind_specif env ind, u) let build_branches_type env sigma (mind,_ as _ind) mib mip u params p = let rtbl = mip.mind_reloc_tbl in diff --git a/printing/printer.ml b/printing/printer.ml index 8af4d1d932..cc83a1dde0 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -38,7 +38,6 @@ let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "printing of unfocused goal"; optkey = ["Printing";"Unfocused"]; optread = (fun () -> !enable_unfocused_goal_printing); optwrite = (fun b -> enable_unfocused_goal_printing:=b) } @@ -49,7 +48,6 @@ let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "printing of goal tags"; optkey = ["Printing";"Goal";"Tags"]; optread = (fun () -> !enable_goal_tags_printing); optwrite = (fun b -> enable_goal_tags_printing:=b) } @@ -59,7 +57,6 @@ let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "printing of goal names"; optkey = ["Printing";"Goal";"Names"]; optread = (fun () -> !enable_goal_names_printing); optwrite = (fun b -> enable_goal_names_printing:=b) } @@ -416,7 +413,6 @@ let () = let open Goptions in declare_int_option { optdepr = false; - optname = "the hypotheses limit"; optkey = ["Hyps";"Limit"]; optread = (fun () -> !print_hyps_limit); optwrite = (fun x -> print_hyps_limit := x) } @@ -625,7 +621,6 @@ let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "Printing Dependent Evars Line"; optkey = ["Printing";"Dependent";"Evars";"Line"]; optread = (fun () -> !should_print_dependent_evars); optwrite = (fun v -> should_print_dependent_evars := v) } diff --git a/printing/printmod.ml b/printing/printmod.ml index 85bb287c22..b84113bde2 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -44,7 +44,6 @@ let short = ref false let () = declare_bool_option { optdepr = false; - optname = "short module printing"; optkey = ["Short";"Module";"Printing"]; optread = (fun () -> !short) ; optwrite = ((:=) short) } @@ -86,8 +85,8 @@ let print_constructors envpar sigma names types = in hv 0 (str " " ++ pc) -let build_ind_type env mip = - Inductive.type_of_inductive env mip +let build_ind_type mip = + Inductive.type_of_inductive mip let print_one_inductive env sigma mib ((_,i) as ind) = let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in @@ -95,7 +94,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) = let params = Inductive.inductive_paramdecls (mib,u) in let nparamdecls = Context.Rel.length params in let args = Context.Rel.to_extended_list mkRel 0 params in - let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type env ((mib,mip),u)) args in + let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in let cstrtypes = Array.map (fun c -> hnf_prod_applist_assum env nparamdecls c args) cstrtypes in let envpar = push_rel_context params env in @@ -147,7 +146,7 @@ let print_record env mind mib udecl = let params = Inductive.inductive_paramdecls (mib,u) in let nparamdecls = Context.Rel.length params in let args = Context.Rel.to_extended_list mkRel 0 params in - let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type env ((mib,mip),u)) args in + let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in let fields = get_fields cstrtype in diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index dec87f8071..d93dd15f91 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -69,7 +69,6 @@ let write_diffs_option opt = let () = Goptions.(declare_string_option { optdepr = false; - optname = "show diffs in proofs"; optkey = ["Diffs"]; optread = read_diffs_option; optwrite = write_diffs_option diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml index a6e27c238f..36b50d9e9f 100644 --- a/proofs/goal_select.ml +++ b/proofs/goal_select.ml @@ -56,7 +56,6 @@ let parse_goal_selector = function let () = let open Goptions in declare_string_option { optdepr = false; - optname = "default goal selector" ; optkey = ["Default";"Goal";"Selector"] ; optread = begin fun () -> Pp.string_of_ppcmds diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index 61e8741973..3ff0533b6b 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -179,7 +179,6 @@ let current_behavior = ref Strict.strict let () = Goptions.(declare_string_option { optdepr = false; - optname = "bullet behavior"; optkey = ["Bullet";"Behavior"]; optread = begin fun () -> (!current_behavior).name diff --git a/stm/stm.ml b/stm/stm.ml index 4c539684e3..a521f9001d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2154,6 +2154,7 @@ let collect_proof keep cur hd brkind id = let is_defined = function | _, { expr = e } -> is_defined_expr e.CAst.v.expr && (not (Vernacprop.has_Fail e)) in + let has_default_proof_using = Option.has_some (Proof_using.get_default_proof_using ()) in let proof_using_ast = function | VernacProof(_,Some _) -> true | _ -> false @@ -2162,7 +2163,7 @@ let collect_proof keep cur hd brkind id = | Some (_, v) when proof_using_ast v.expr.CAst.v.expr && (not (Vernacprop.has_Fail v.expr)) -> Some v | _ -> None in - let has_proof_using x = proof_using_ast x <> None in + let has_proof_using x = has_default_proof_using || (proof_using_ast x <> None) in let proof_no_using = function | VernacProof(t,None) -> t | _ -> assert false @@ -2849,7 +2850,6 @@ let process_back_meta_command ~newtip ~head oid aast = let get_allow_nested_proofs = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"Nested Proofs Allowed" ~key:Vernac_classifier.stm_allow_nested_proofs_option_name ~value:false diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index c5b3e0931b..65ef2ca8c6 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -131,7 +131,7 @@ let classify_vernac e = VtSideff ([id.CAst.v], VtLater) | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id, VtLater) | VernacInductive (_, _,_,l) -> - let ids = List.map (fun (((_,({v=id},_)),_,_,_,cl),_) -> id :: match cl with + let ids = List.map (fun (((_,({v=id},_)),_,_,cl),_) -> id :: match cl with | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @ CList.map_filter (function diff --git a/tactics/auto.ml b/tactics/auto.ml index 9c1a975330..1dde820075 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -177,7 +177,6 @@ let global_info_auto = ref false let add_option ls refe = Goptions.(declare_bool_option { optdepr = false; - optname = String.concat " " ls; optkey = ls; optread = (fun () -> !refe); optwrite = (:=) refe }) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index ccd88d2c35..28feeecb86 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -83,8 +83,6 @@ open Goptions let () = declare_bool_option { optdepr = false; - optname = "do typeclass search avoiding eta-expansions " ^ - " in proof terms (expensive)"; optkey = ["Typeclasses";"Limit";"Intros"]; optread = get_typeclasses_limit_intros; optwrite = set_typeclasses_limit_intros; } @@ -92,7 +90,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "during typeclass resolution, solve instances according to their dependency order"; optkey = ["Typeclasses";"Dependency";"Order"]; optread = get_typeclasses_dependency_order; optwrite = set_typeclasses_dependency_order; } @@ -100,7 +97,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "use iterative deepening strategy"; optkey = ["Typeclasses";"Iterative";"Deepening"]; optread = get_typeclasses_iterative_deepening; optwrite = set_typeclasses_iterative_deepening; } @@ -108,7 +104,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "compat"; optkey = ["Typeclasses";"Filtered";"Unification"]; optread = get_typeclasses_filtered_unification; optwrite = set_typeclasses_filtered_unification; } @@ -116,7 +111,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "debug output for typeclasses proof search"; optkey = ["Typeclasses";"Debug"]; optread = get_typeclasses_debug; optwrite = set_typeclasses_debug; } @@ -124,7 +118,6 @@ let () = let _ = declare_int_option { optdepr = false; - optname = "verbosity of debug output for typeclasses proof search"; optkey = ["Typeclasses";"Debug";"Verbosity"]; optread = get_typeclasses_verbose; optwrite = set_typeclasses_verbose; } @@ -132,7 +125,6 @@ let _ = let () = declare_int_option { optdepr = false; - optname = "depth for typeclasses proof search"; optkey = ["Typeclasses";"Depth"]; optread = get_typeclasses_depth; optwrite = set_typeclasses_depth; } diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 80ca124912..9a1e6a6736 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -331,7 +331,6 @@ let global_info_eauto = ref false let () = Goptions.(declare_bool_option { optdepr = false; - optname = "Debug Eauto"; optkey = ["Debug";"Eauto"]; optread = (fun () -> !global_debug_eauto); optwrite = (:=) global_debug_eauto }) @@ -339,7 +338,6 @@ let () = let () = Goptions.(declare_bool_option { optdepr = false; - optname = "Info Eauto"; optkey = ["Info";"Eauto"]; optread = (fun () -> !global_info_eauto); optwrite = (:=) global_info_eauto }) diff --git a/tactics/equality.ml b/tactics/equality.ml index 9ef5f478d3..7393454ba9 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -72,7 +72,6 @@ let use_injection_in_context = function let () = declare_bool_option { optdepr = false; - optname = "injection in context"; optkey = ["Structural";"Injection"]; optread = (fun () -> !injection_in_context) ; optwrite = (fun b -> injection_in_context := b) } @@ -734,7 +733,6 @@ let keep_proof_equalities_for_injection = ref false let () = declare_bool_option { optdepr = false; - optname = "injection on prop arguments"; optkey = ["Keep";"Proof";"Equalities"]; optread = (fun () -> !keep_proof_equalities_for_injection) ; optwrite = (fun b -> keep_proof_equalities_for_injection := b) } @@ -1686,7 +1684,6 @@ let regular_subst_tactic = ref true let () = declare_bool_option { optdepr = false; - optname = "more regular behavior of tactic subst"; optkey = ["Regular";"Subst";"Tactic"]; optread = (fun () -> !regular_subst_tactic); optwrite = (:=) regular_subst_tactic } diff --git a/tactics/hints.ml b/tactics/hints.ml index 73e8331bcb..86aa046586 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -205,7 +205,6 @@ let write_warn_hint = function let () = Goptions.(declare_string_option { optdepr = false; - optname = "behavior of non-imported hints"; optkey = ["Loose"; "Hint"; "Behavior"]; optread = read_warn_hint; optwrite = write_warn_hint; diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index a4a06873b8..72204e1d24 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -17,7 +17,6 @@ open Evd let use_unification_heuristics_ref = ref true let () = Goptions.(declare_bool_option { optdepr = false; - optname = "Solve unification constraints at every \".\""; optkey = ["Solve";"Unification";"Constraints"]; optread = (fun () -> !use_unification_heuristics_ref); optwrite = (fun a -> use_unification_heuristics_ref:=a); diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml index b1fd34e43c..4c470519d6 100644 --- a/tactics/proof_global.ml +++ b/tactics/proof_global.ml @@ -143,7 +143,6 @@ let private_poly_univs = let b = ref true in let _ = Goptions.(declare_bool_option { optdepr = false; - optname = "use private polymorphic universes for Qed constants"; optkey = ["Private";"Polymorphic";"Universes"]; optread = (fun () -> !b); optwrite = ((:=) b); diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index fc7b126ee5..a30c877435 100644 --- a/tactics/redexpr.ml +++ b/tactics/redexpr.ml @@ -56,8 +56,6 @@ let strong_cbn flags = let simplIsCbn = ref (false) let () = Goptions.(declare_bool_option { optdepr = false; - optname = - "Plug the simpl tactic to the new cbn mechanism"; optkey = ["SimplIsCbn"]; optread = (fun () -> !simplIsCbn); optwrite = (fun a -> simplIsCbn:=a); diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2d900a237a..8371da76b2 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -67,7 +67,6 @@ let use_clear_hyp_by_default () = !clear_hyp_by_default let () = declare_bool_option { optdepr = false; - optname = "default clearing of hypotheses after use"; optkey = ["Default";"Clearing";"Used";"Hypotheses"]; optread = (fun () -> !clear_hyp_by_default) ; optwrite = (fun b -> clear_hyp_by_default := b) } @@ -83,7 +82,6 @@ let accept_universal_lemma_under_conjunctions () = let () = declare_bool_option { optdepr = false; - optname = "trivial unification in tactics applying under conjunctions"; optkey = ["Universal";"Lemma";"Under";"Conjunction"]; optread = (fun () -> !universal_lemma_under_conjunctions) ; optwrite = (fun b -> universal_lemma_under_conjunctions := b) } @@ -102,7 +100,6 @@ let use_bracketing_last_or_and_intro_pattern () = let () = declare_bool_option { optdepr = true; - optname = "bracketing last or-and introduction pattern"; optkey = ["Bracketing";"Last";"Introduction";"Pattern"]; optread = (fun () -> !bracketing_last_or_and_intro_pattern); optwrite = (fun b -> bracketing_last_or_and_intro_pattern := b) } diff --git a/test-suite/README.md b/test-suite/README.md index a2d5905710..96926f70b9 100644 --- a/test-suite/README.md +++ b/test-suite/README.md @@ -67,7 +67,7 @@ See [`test-suite/Makefile`](Makefile) for more information. ## Adding a test Regression tests for closed bugs should be added to -[`bugs/closed`](bugs/closed), as `1234.v` where `1234` is the bug number. +[`bugs/closed`](bugs/closed), as `bug_1234.v` where `1234` is the bug number. Files in this directory are tested for successful compilation. When you fix a bug, you should usually add a regression test here as well. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 5093e785de..26ebd8efc3 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -86,8 +86,8 @@ Sequences of implicit arguments must be of different lengths. The command has indeed failed with message: Some argument names are duplicated: F The command has indeed failed with message: -Argument number 2 (anonymous in original definition) cannot be declared -implicit. +Argument number 3 is a trailing implicit, so it can't be declared non +maximal. Please use { } instead of [ ]. The command has indeed failed with message: Extra arguments: y. The command has indeed failed with message: diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v index 9713a9dbbe..6ac09cf771 100644 --- a/test-suite/output/Arguments_renaming.v +++ b/test-suite/output/Arguments_renaming.v @@ -49,7 +49,6 @@ Check @myplus. Fail Arguments eq_refl {F g}, [H] k. Fail Arguments eq_refl {F}, [F] : rename. Fail Arguments eq_refl {F F}, [F] F : rename. -Fail Arguments eq {F} x [z] : rename. +Fail Arguments eq {A} x [z] : rename. Fail Arguments eq {F} x z y. Fail Arguments eq {R} s t. - diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out index 3f4d5ef58c..190c34262f 100644 --- a/test-suite/output/PrintAssumptions.out +++ b/test-suite/output/PrintAssumptions.out @@ -3,6 +3,10 @@ foo : nat Axioms: foo : nat Axioms: +bli : Type +Axioms: +bli : Type +Axioms: extensionality : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g Axioms: diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v index 3d4dfe603d..4c980fddba 100644 --- a/test-suite/output/PrintAssumptions.v +++ b/test-suite/output/PrintAssumptions.v @@ -30,6 +30,21 @@ Module P := N M. Print Assumptions M.bar. (* Should answer: foo *) Print Assumptions P.bar. (* Should answer: foo *) +(* Print Assumptions used empty instances on polymorphic inductives *) +Module Poly. + + Set Universe Polymorphism. + Axiom bli : Type. + + Definition bla := bli -> bli. + + Inductive blo : bli -> Type := . + + Print Assumptions bla. + Print Assumptions blo. + +End Poly. + (* The original test-case of the bug-report *) diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index 668d765d83..59650d6822 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -169,3 +169,16 @@ Variable eq0le0' : forall (n : nat) {x : n = 0}, n <= 0. Axiom eq0le0'' : forall (n : nat) {x : n = 0}, n <= 0. Definition eq0le0''' : forall (n : nat) {x : n = 0}, n <= 0. Admitted. Fail Axiom eq0le0'''' : forall [n : nat] {x : n = 0}, n <= 0. + +Module TestUnnamedImplicit. + +Axiom foo : forall A, A -> A. + +Arguments foo {A} {_}. +Check foo (arg_2:=true) : bool. +Check foo : bool. + +Arguments foo {A} {x}. +Check foo (x:=true) : bool. + +End TestUnnamedImplicit. diff --git a/test-suite/success/uniform_inductive_parameters.v b/test-suite/success/uniform_inductive_parameters.v index 42236a5313..651247937d 100644 --- a/test-suite/success/uniform_inductive_parameters.v +++ b/test-suite/success/uniform_inductive_parameters.v @@ -1,13 +1,23 @@ +Module Att. + #[uniform] Inductive list (A : Type) := + | nil : list + | cons : A -> list -> list. + Check (list : Type -> Type). + Check (cons : forall A, A -> list A -> list A). +End Att. + Set Uniform Inductive Parameters. Inductive list (A : Type) := - | nil : list - | cons : A -> list -> list. +| nil : list +| cons : A -> list -> list. Check (list : Type -> Type). Check (cons : forall A, A -> list A -> list A). Inductive list2 (A : Type) (A' := prod A A) := - | nil2 : list2 - | cons2 : A' -> list2 -> list2. +| nil2 : list2 +| cons2 : A' -> list2 -> list2. Check (list2 : Type -> Type). Check (cons2 : forall A (A' := prod A A), A' -> list2 A -> list2 A). + +#[nonuniform] Inductive bla (n:nat) := c (_ : bla (S n)). diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index d3ed5e78b4..49fb88cd8c 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -91,6 +91,7 @@ COQDEP ?= "$(COQBIN)coqdep" COQDOC ?= "$(COQBIN)coqdoc" COQPP ?= "$(COQBIN)coqpp" COQMKFILE ?= "$(COQBIN)coq_makefile" +OCAMLLIBDEP ?= "$(COQBIN)ocamllibdep" # Timing scripts COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py" @@ -455,13 +456,13 @@ all.ps: $(VFILES) $(SHOW)'COQDOC -ps $(GAL)' $(HIDE)$(COQDOC) \ -toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \ - -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` + -o $@ `$(COQDEP) -sort $(VFILES)` all.pdf: $(VFILES) $(SHOW)'COQDOC -pdf $(GAL)' $(HIDE)$(COQDOC) \ -toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \ - -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` + -o $@ `$(COQDEP) -sort $(VFILES)` # FIXME: not quite right, since the output name is different gallinahtml: GAL=-g @@ -747,12 +748,12 @@ $(addsuffix .d,$(MLFILES)): %.ml.d: %.ml $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) $(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) $(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) # If this makefile is created using a _CoqProject we have coqdep get # options from it. This avoids argument length limits for pathological diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 950c784325..a96173c057 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -31,7 +31,6 @@ let option_sort = ref false let usage () = eprintf " usage: coqdep [options] <filename>+\n"; eprintf " options:\n"; - eprintf " -c : Also print the dependencies of caml modules (=ocamldep).\n"; eprintf " -boot : For coq developers, prints dependencies over coq library files (omitted by default).\n"; eprintf " -sort : output the given file name ordered by dependencies\n"; eprintf " -noglob | -no-glob : \n"; @@ -44,8 +43,6 @@ let usage () = eprintf " -vos : also output dependencies about .vos files\n"; eprintf " -exclude-dir dir : skip subdirectories named 'dir' during -R/-Q search\n"; eprintf " -coqlib dir : set the coq standard library directory\n"; - eprintf " -suffix s : \n"; - eprintf " -slash : deprecated, no effect\n"; eprintf " -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed\n"; exit 1 @@ -65,8 +62,6 @@ let treat_coqproject f = iter_sourced (fun f -> treat_file None f) (all_files project) let rec parse = function - (* TODO, deprecate option -c *) - | "-c" :: ll -> option_c := true; parse ll | "-boot" :: ll -> option_boot := true; parse ll | "-sort" :: ll -> option_sort := true; parse ll | "-vos" :: ll -> write_vos := true; parse ll @@ -81,8 +76,6 @@ let rec parse = function | "-exclude-dir" :: [] -> usage () | "-coqlib" :: r :: ll -> Envars.set_user_coqlib r; parse ll | "-coqlib" :: [] -> usage () - | "-suffix" :: s :: ll -> suffixe := s ; parse ll - | "-suffix" :: [] -> usage () | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll @@ -114,11 +107,7 @@ let coqdep () = (Envars.xdg_dirs ~warn:(fun x -> coqdep_warning "%s" x)); List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) Envars.coqpath; end; - List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu; - List.iter (fun (f,d) -> add_mllib_known f d ".mllib") !mllibAccu; - List.iter (fun (f,suff,d) -> add_ml_known f d suff) !mlAccu; if !option_sort then begin sort (); exit 0 end; - if !option_c then mL_dependencies (); coq_dependencies (); () diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 5ece595f13..683165f026 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -31,15 +31,12 @@ module StrListMap = Map.Make(StrList) type dynlink = Opt | Byte | Both | No | Variable -let option_c = ref false let option_noglob = ref false let option_dynlink = ref Both let option_boot = ref false let norec_dirs = ref StrSet.empty -let suffixe = ref ".vo" - type dir = string option (** [get_extension f l] checks whether [f] has one of the extensions @@ -58,18 +55,6 @@ let basename_noext filename = let fn = Filename.basename filename in try Filename.chop_extension fn with Invalid_argument _ -> fn -(** ML Files specified on the command line. In the entries: - - the first string is the basename of the file, without extension nor - directory part - - the second string of [mlAccu] is the extension (either .ml or .mlg) - - the [dir] part is the directory, with None used as the current directory -*) - -let mlAccu = ref ([] : (string * string * dir) list) -and mliAccu = ref ([] : (string * dir) list) -and mllibAccu = ref ([] : (string * dir) list) -and mlpackAccu = ref ([] : (string * dir) list) - (** Coq files specifies on the command line: - first string is the full filename, with only its extension removed - second string is the absolute version of the previous (via getcwd) @@ -125,8 +110,6 @@ let mkknown () = with Not_found -> None in add, iter, search -let add_ml_known, _, search_ml_known = mkknown () -let add_mli_known, _, search_mli_known = mkknown () let add_mllib_known, _, search_mllib_known = mkknown () let add_mlpack_known, _, search_mlpack_known = mkknown () @@ -231,64 +214,6 @@ let file_name s = function | None -> s | Some d -> d // s -let depend_ML str = - match search_mli_known str, search_ml_known str with - | Some mlidir, Some mldir -> - let mlifile = file_name str mlidir - and mlfile = file_name str mldir in - (" "^mlifile^".cmi"," "^mlfile^".cmx") - | None, Some mldir -> - let mlfile = file_name str mldir in - (" "^mlfile^".cmo"," "^mlfile^".cmx") - | Some mlidir, None -> - let mlifile = file_name str mlidir in - (" "^mlifile^".cmi"," "^mlifile^".cmi") - | None, None -> "", "" - -let traite_fichier_ML md ext = - try - let chan = open_in (md ^ ext) in - let buf = Lexing.from_channel chan in - let deja_vu = ref (StrSet.singleton md) in - let a_faire = ref "" in - let a_faire_opt = ref "" in - begin try - while true do - let (Use_module str) = caml_action buf in - if StrSet.mem str !deja_vu then - () - else begin - deja_vu := StrSet.add str !deja_vu; - let byte,opt = depend_ML str in - a_faire := !a_faire ^ byte; - a_faire_opt := !a_faire_opt ^ opt - end - done - with Fin_fichier -> () - end; - close_in chan; - (!a_faire, !a_faire_opt) - with Sys_error _ -> ("","") - -let traite_fichier_modules md ext = - try - let chan = open_in (md ^ ext) in - let list = mllib_list (Lexing.from_channel chan) in - List.fold_left - (fun a_faire str -> match search_mlpack_known str with - | Some mldir -> - let file = file_name str mldir in - a_faire @ [file] - | None -> - match search_ml_known str with - | Some mldir -> - let file = file_name str mldir in - a_faire @ [file] - | None -> a_faire) [] list - with - | Sys_error _ -> [] - | Syntax_error (i,j) -> error_cannot_parse (md^ext) (i,j) - (* Makefile's escaping rules are awful: $ is escaped by doubling and other special characters are escaped by backslash prefixing while backslashes themselves must be escaped only if part of a sequence @@ -418,10 +343,7 @@ let rec find_dependencies basename = | None -> match search_mlpack_known s with | Some mldir -> declare ".cmo" mldir s - | None -> - match search_ml_known s with - | Some mldir -> declare ".cmo" mldir s - | None -> warning_declare f str + | None -> warning_declare f str end in List.iter decl sl @@ -449,59 +371,16 @@ let rec find_dependencies basename = with Sys_error _ -> [] (* TODO: report an error? *) -let mL_dependencies () = - List.iter - (fun (name,ext,dirname) -> - let fullname = file_name name dirname in - let (dep,dep_opt) = traite_fichier_ML fullname ext in - let intf = match search_mli_known name with - | None -> "" - | Some mldir -> " "^(file_name name mldir)^".cmi" - in - let efullname = escape fullname in - printf "%s.cmo:%s%s\n" efullname dep intf; - printf "%s.cmx:%s%s\n%!" efullname dep_opt intf) - (List.rev !mlAccu); - List.iter - (fun (name,dirname) -> - let fullname = file_name name dirname in - let (dep,_) = traite_fichier_ML fullname ".mli" in - printf "%s.cmi:%s\n%!" (escape fullname) dep) - (List.rev !mliAccu); - List.iter - (fun (name,dirname) -> - let fullname = file_name name dirname in - let dep = traite_fichier_modules fullname ".mllib" in - let efullname = escape fullname in - printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname (String.concat " " dep); - printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname; - printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n%!" efullname efullname) - (List.rev !mllibAccu); - List.iter - (fun (name,dirname) -> - let fullname = file_name name dirname in - let dep = traite_fichier_modules fullname ".mlpack" in - let efullname = escape fullname in - printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname (String.concat " " dep); - printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname; - printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname; - let efullname_capital = String.capitalize_ascii (Filename.basename efullname) in - List.iter (fun dep -> - printf "%s.cmx : FOR_PACK=-for-pack %s\n" dep efullname_capital) - dep; - printf "%!") - (List.rev !mlpackAccu) - let write_vos = ref false let coq_dependencies () = List.iter (fun (name,_) -> let ename = escape name in - let glob = if !option_noglob then "" else " "^ename^".glob" in + let glob = if !option_noglob then "" else ename^".glob " in let deps = find_dependencies name in - printf "%s%s%s %s.v.beautified %s.required_vo: %s.v %s\n" ename !suffixe glob ename ename ename - (string_of_dependency_list !suffixe deps); + printf "%s.vo %s%s.v.beautified %s.required_vo: %s.v %s\n" ename glob ename ename ename + (string_of_dependency_list ".vo" deps); printf "%s.vio: %s.v %s\n" ename ename (string_of_dependency_list ".vio" deps); if !write_vos then @@ -517,10 +396,8 @@ let rec suffixes = function let add_caml_known phys_dir _ f = let basename,suff = - get_extension f [".ml";".mli";".mlg";".mllib";".mlpack"] in + get_extension f [".mllib"; ".mlpack"] in match suff with - | ".ml"|".mlg" -> add_ml_known basename (Some phys_dir) suff - | ".mli" -> add_mli_known basename (Some phys_dir) suff | ".mllib" -> add_mllib_known basename (Some phys_dir) suff | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff | _ -> () @@ -605,18 +482,15 @@ let rec treat_file old_dirname old_name = in Array.iter (treat_file (Some newdirname)) (Sys.readdir complete_name)) | S_REG -> - (match get_extension name [".v";".ml";".mli";".mlg";".mllib";".mlpack"] with - | (base,".v") -> - let name = file_name base dirname - and absname = absolute_file_name base dirname in - addQueue vAccu (name, absname) - | (base,(".ml"|".mlg" as ext)) -> addQueue mlAccu (base,ext,dirname) - | (base,".mli") -> addQueue mliAccu (base,dirname) - | (base,".mllib") -> addQueue mllibAccu (base,dirname) - | (base,".mlpack") -> addQueue mlpackAccu (base,dirname) - | _ -> ()) + (match get_extension name [".v"] with + | base,".v" -> + let name = file_name base dirname + and absname = absolute_file_name base dirname in + addQueue vAccu (name, absname) + | _ -> ()) | _ -> () +(* "[sort]" outputs `.v` files required by others *) let sort () = let seen = Hashtbl.create 97 in let rec loop file = @@ -639,7 +513,7 @@ let sort () = done with Fin_fichier -> close_in cin; - printf "%s%s " file !suffixe + printf "%s.v " file end in List.iter (fun (name,_) -> loop name) !vAccu diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 1820db4a1e..aca68cc780 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -21,11 +21,9 @@ val coqdep_warning : ('a, Format.formatter, unit, unit) format4 -> 'a val find_dir_logpath: string -> string list (** Options *) -val option_c : bool ref val option_noglob : bool ref val option_boot : bool ref val write_vos : bool ref -val suffixe : string ref type dynlink = Opt | Byte | Both | No | Variable val option_dynlink : dynlink ref @@ -36,18 +34,11 @@ type dir = string option val treat_file : dir -> string -> unit (** ML-related manipulation *) -val mlAccu : (string * string * dir) list ref -val mliAccu : (string * dir) list ref -val mllibAccu : (string * dir) list ref -val add_ml_known : string -> dir -> string -> unit -val add_mli_known : string -> dir -> string -> unit -val add_mllib_known : string -> dir -> string -> unit -val mL_dependencies : unit -> unit - val coq_dependencies : unit -> unit val add_known : bool -> string -> string list -> string -> unit val add_coqlib_known : bool -> string -> string list -> string -> unit +(* Used to locate plugins for [Declare ML Module] *) val add_caml_dir : string -> unit (** Simply add this directory and imports it, no subdirs. This is used diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli index 018fc1b7a2..24452f203a 100644 --- a/tools/coqdep_lexer.mli +++ b/tools/coqdep_lexer.mli @@ -8,12 +8,10 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -type mL_token = Use_module of string - type qualid = string list type coq_token = - Require of qualid option * qualid list + | Require of qualid option * qualid list | Declare of string list | Load of string | AddLoadPath of string @@ -23,6 +21,3 @@ exception Fin_fichier exception Syntax_error of int * int val coq_action : Lexing.lexbuf -> coq_token -val caml_action : Lexing.lexbuf -> mL_token -val mllib_list : Lexing.lexbuf -> string list -val ocamldep_parse : Lexing.lexbuf -> string list diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index 743da535b8..157c2b7dba 100644 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -13,8 +13,6 @@ open Filename open Lexing - type mL_token = Use_module of string - type qualid = string list type coq_token = @@ -152,56 +150,6 @@ and add_loadpath_as path = parse | dot { AddLoadPath path } -and caml_action = parse - | space + - { caml_action lexbuf } - | "open" space* (caml_up_ident as id) - { Use_module (String.uncapitalize_ascii id) } - | "module" space+ caml_up_ident - { caml_action lexbuf } - | caml_low_ident { caml_action lexbuf } - | caml_up_ident - { qual_id (Lexing.lexeme lexbuf) lexbuf } - | ['0'-'9']+ - | '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']+ - | '0' ['o' 'O'] ['0'-'7']+ - | '0' ['b' 'B'] ['0'-'1']+ - { caml_action lexbuf } - | ['0'-'9']+ ('.' ['0'-'9']*)? (['e' 'E'] ['+' '-']? ['0'-'9']+)? - { caml_action lexbuf } - | "\"" - { string lexbuf; caml_action lexbuf } - | "'" [^ '\\' '\''] "'" - { caml_action lexbuf } - | "'" '\\' ['\\' '\'' 'n' 't' 'b' 'r'] "'" - { caml_action lexbuf } - | "'" '\\' ['0'-'9'] ['0'-'9'] ['0'-'9'] "'" - { caml_action lexbuf } - | "(*" - { comment lexbuf; caml_action lexbuf } - | "#" | "&" | "&&" | "'" | "(" | ")" | "*" | "," | "?" | "->" | "." | ".." - | ".(" | ".[" | ":" | "::" | ":=" | ";" | ";;" | "<-" | "=" | "[" | "[|" - | "[<" | "]" | "_" | "{" | "|" | "||" | "|]" | ">]" | "}" | "!=" | "-" - | "-." { caml_action lexbuf } - - | ['!' '?' '~'] - ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * - { caml_action lexbuf } - | ['=' '<' '>' '@' '^' '|' '&' '$'] - ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * - { caml_action lexbuf } - | ['+' '-'] - ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * - { caml_action lexbuf } - | "**" - ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * - { caml_action lexbuf } - | ['*' '/' '%'] - ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * - { caml_action lexbuf } - | eof { raise Fin_fichier } - | _ { caml_action lexbuf } - and comment = parse | "(*" { comment lexbuf; comment lexbuf } @@ -218,20 +166,6 @@ and comment = parse | _ { comment lexbuf } -and string = parse - | '"' (* '"' *) - { () } - | '\\' ("\010" | "\013" | "\010\013") [' ' '\009'] * - { string lexbuf } - | '\\' ['\\' '"' 'n' 't' 'b' 'r'] (*'"'*) - { string lexbuf } - | '\\' ['0'-'9'] ['0'-'9'] ['0'-'9'] - { string lexbuf } - | eof - { raise Fin_fichier } - | _ - { string lexbuf } - and load_file = parse | '"' [^ '"']* '"' (*'"'*) { let s = lexeme lexbuf in @@ -320,20 +254,3 @@ and modules mllist = parse { syntax_error lexbuf } | _ { Declare (List.rev mllist) } - -and qual_id ml_module_name = parse - | '.' [^ '.' '(' '['] - { Use_module (String.uncapitalize_ascii ml_module_name) } - | eof { raise Fin_fichier } - | _ { caml_action lexbuf } - -and mllib_list = parse - | caml_up_ident { let s = String.uncapitalize_ascii (Lexing.lexeme lexbuf) - in s :: mllib_list lexbuf } - | "*predef*" { mllib_list lexbuf } - | space+ { mllib_list lexbuf } - | eof { [] } - | _ { syntax_error lexbuf } - -and ocamldep_parse = parse - | [^ ':' ]* ':' { mllib_list lexbuf } diff --git a/tools/dune b/tools/dune index 204bd09535..c0e4e20f72 100644 --- a/tools/dune +++ b/tools/dune @@ -29,7 +29,15 @@ (modules coqdep_lexer coqdep_common coqdep) (libraries coq.lib)) -(ocamllex coqdep_lexer) +; Bare-bones mllib/mlpack parser +(executable + (name ocamllibdep) + (public_name ocamllibdep) + (modules ocamllibdep) + (package coq) + (libraries unix)) + +(ocamllex coqdep_lexer ocamllibdep) (executable (name coqwc) diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll index 41a4e2a86a..2ecc20f1b0 100644 --- a/tools/ocamllibdep.mll +++ b/tools/ocamllibdep.mll @@ -195,6 +195,14 @@ let mllib_dependencies () = flush stdout) (List.rev !mllibAccu) +let coq_makefile_mode = ref false + +let print_for_pack modname d = + if !coq_makefile_mode then + printf "%s.cmx : FOR_PACK=-for-pack %s\n" d modname + else + printf "%s_FORPACK:= -for-pack %s\n" d modname + let mlpack_dependencies () = List.iter (fun (name,dirname) -> @@ -204,7 +212,7 @@ let mlpack_dependencies () = let sdeps = String.concat " " deps in let efullname = escape fullname in printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname sdeps; - List.iter (fun d -> printf "%s_FORPACK:= -for-pack %s\n" d modname) deps; + List.iter (print_for_pack modname) deps; printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname; printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" @@ -213,6 +221,7 @@ let mlpack_dependencies () = (List.rev !mlpackAccu) let rec parse = function + | "-c" :: r -> coq_makefile_mode := true; parse r | "-I" :: r :: ll -> (* To solve conflict (e.g. same filename in kernel and checker) we allow to state an explicit order *) diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 977cae6254..e4508e9bfc 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -368,103 +368,107 @@ let top_goal_print ~doc c oldp newp = let exit_on_error = let open Goptions in - declare_bool_option_and_ref ~depr:false ~name:"coqtop-exit-on-error" ~key:["Coqtop";"Exit";"On";"Error"] + declare_bool_option_and_ref ~depr:false ~key:["Coqtop";"Exit";"On";"Error"] ~value:false -let rec vernac_loop ~state = - let open CAst in +(* XXX: This is duplicated with Vernacentries.show_proof , at some + point we should consolidate the code *) +let show_proof_diff_to_pp pstate = + let p = Option.get pstate in + let sigma, env = Pfedit.get_proof_context p in + let pprf = Proof.partial_proof p in + Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf + +let show_proof_diff_cmd ~state removed = let open Vernac.State in - let open G_toplevel in - loop_flush_all (); - top_stderr (fnl()); - if !print_emacs then top_stderr (str (top_buffer.prompt state.doc)); - resynch_buffer top_buffer; - (* execute one command *) try - let input = top_buffer.tokens in - match read_sentence ~state input with - | Some (VernacBackTo bid) -> - let bid = Stateid.of_int bid in - let doc, res = Stm.edit_at ~doc:state.doc bid in - assert (res = `NewTip); - let state = { state with doc; sid = bid } in - vernac_loop ~state - - | Some VernacQuit -> - exit 0 - - | Some VernacDrop -> - if Mltop.is_ocaml_top() - then (drop_last_doc := Some state; state) - else (Feedback.msg_warning (str "There is no ML toplevel."); vernac_loop ~state) - - | Some VernacControl { loc; v=c } -> - let nstate = Vernac.process_expr ~state (make ?loc c) in - top_goal_print ~doc:state.doc c state.proof nstate.proof; - vernac_loop ~state:nstate - - | Some (VernacShowGoal {gid; sid}) -> - let proof = Stm.get_proof ~doc:state.doc (Stateid.of_int sid) in - let goal = Printer.pr_goal_emacs ~proof gid sid in - let evars = - match proof with - | None -> mt() - | Some p -> - let gl = (Evar.unsafe_of_int gid) in - let { Proof.sigma } = Proof.data p in - try Printer.print_dependent_evars (Some gl) sigma [ gl ] - with Not_found -> mt() - in - Feedback.msg_notice (v 0 (goal ++ evars)); - vernac_loop ~state - - | Some VernacShowProofDiffs removed -> - (* extension of Vernacentries.show_proof *) - let to_pp pstate = - let p = Option.get pstate in - let sigma, env = Pfedit.get_proof_context p in - let pprf = Proof.partial_proof p in - Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf - (* We print nothing if there are no goals left *) - in - - if not (Proof_diffs.color_enabled ()) then - CErrors.user_err Pp.(str "Show Proof Diffs requires setting the \"-color\" command line argument to \"on\" or \"auto\".") - else begin - let out = - try - let n_pp = to_pp state.proof in - if true (*Proof_diffs.show_diffs ()*) then - let doc = state.doc in - let oproof = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in - try - let o_pp = to_pp oproof in - let tokenize_string = Proof_diffs.tokenize_string in - let show_removed = Some removed in - Pp_diff.diff_pp_combined ~tokenize_string ?show_removed o_pp n_pp - with - | Pfedit.NoSuchGoal - | Option.IsNone -> n_pp - | Pp_diff.Diff_Failure msg -> begin - (* todo: print the unparsable string (if we know it) *) - Feedback.msg_warning Pp.(str ("Diff failure: " ^ msg) ++ cut() - ++ str "Showing results without diff highlighting" ); - n_pp - end - else - n_pp - with - | Pfedit.NoSuchGoal - | Option.IsNone -> - CErrors.user_err (str "No goals to show.") - in - Feedback.msg_notice out; - end; - vernac_loop ~state - - | None -> - top_stderr (fnl ()); exit 0 + let n_pp = show_proof_diff_to_pp state.proof in + if true (*Proof_diffs.show_diffs ()*) then + let doc = state.doc in + let oproof = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in + try + let o_pp = show_proof_diff_to_pp oproof in + let tokenize_string = Proof_diffs.tokenize_string in + let show_removed = Some removed in + Pp_diff.diff_pp_combined ~tokenize_string ?show_removed o_pp n_pp + with + | Pfedit.NoSuchGoal + | Option.IsNone -> n_pp + | Pp_diff.Diff_Failure msg -> begin + (* todo: print the unparsable string (if we know it) *) + Feedback.msg_warning Pp.(str ("Diff failure: " ^ msg) ++ cut() + ++ str "Showing results without diff highlighting" ); + n_pp + end + else + n_pp + with + | Pfedit.NoSuchGoal + | Option.IsNone -> + CErrors.user_err (str "No goals to show.") + +let process_toplevel_command ~state stm = + let open Vernac.State in + let open G_toplevel in + match stm with + (* Usually handled in the caller *) + | VernacDrop -> + state + + | VernacBackTo bid -> + let bid = Stateid.of_int bid in + let doc, res = Stm.edit_at ~doc:state.doc bid in + assert (res = `NewTip); + { state with doc; sid = bid } + + | VernacQuit -> + exit 0 + + | VernacControl { CAst.loc; v=c } -> + let nstate = Vernac.process_expr ~state (CAst.make ?loc c) in + top_goal_print ~doc:state.doc c state.proof nstate.proof; + nstate + + | VernacShowGoal { gid; sid } -> + let proof = Stm.get_proof ~doc:state.doc (Stateid.of_int sid) in + let goal = Printer.pr_goal_emacs ~proof gid sid in + let evars = + match proof with + | None -> mt() + | Some p -> + let gl = (Evar.unsafe_of_int gid) in + let { Proof.sigma } = Proof.data p in + try Printer.print_dependent_evars (Some gl) sigma [ gl ] + with Not_found -> mt() + in + Feedback.msg_notice (v 0 (goal ++ evars)); + state + + | VernacShowProofDiffs removed -> + (* We print nothing if there are no goals left *) + if not (Proof_diffs.color_enabled ()) then + CErrors.user_err Pp.(str "Show Proof Diffs requires setting the \"-color\" command line argument to \"on\" or \"auto\".") + else + let out = show_proof_diff_cmd ~state removed in + Feedback.msg_notice out; + state + +(* We return a new state and true if we got a `Drop` command *) +let read_and_execute_base ~state = + let input = top_buffer.tokens in + match read_sentence ~state input with + | Some G_toplevel.VernacDrop -> + if Mltop.is_ocaml_top() + then (drop_last_doc := Some state; state, true) + else (Feedback.msg_warning (str "There is no ML toplevel."); state, false) + | Some stm -> + process_toplevel_command ~state stm, false + (* End of file *) + | None -> + top_stderr (fnl ()); exit 0 +let read_and_execute ~state = + try read_and_execute_base ~state with (* Exception printing should be done by the feedback listener, however this is not yet ready so we rely on the exception for @@ -473,7 +477,7 @@ let rec vernac_loop ~state = (* the parser doesn't like nonblocking mode, cf #10918 *) let msg = Pp.(strbrk "Coqtop needs the standard input to be in blocking mode." ++ spc() - ++ str "One way of clearing the non-blocking flag is through python:" ++ fnl() + ++ str "One way of clearing the non-blocking flag is through Python:" ++ fnl() ++ str " import os" ++ fnl() ++ str " os.set_blocking(0, True)") in @@ -485,21 +489,17 @@ let rec vernac_loop ~state = let msg = CErrors.iprint (e, info) in TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer; if exit_on_error () then exit 1; - vernac_loop ~state + state, false -let rec loop ~state = +(* This function will only return on [Drop], careful to keep it tail-recursive *) +let rec vernac_loop ~state = let open Vernac.State in - Sys.catch_break true; - try - reset_input_buffer state.doc stdin top_buffer; - vernac_loop ~state - with - | any -> - top_stderr - (hov 0 (str "Anomaly: main loop exited with exception:" ++ spc () ++ - str (Printexc.to_string any)) ++ spc () ++ - hov 0 (str "Please report at " ++ str Coq_config.wwwbugtracker ++ str ".")); - loop ~state + loop_flush_all (); + top_stderr (fnl()); + if !print_emacs then top_stderr (str (top_buffer.prompt state.doc)); + resynch_buffer top_buffer; + let state, drop = read_and_execute ~state in + if drop then state else vernac_loop ~state (* Default toplevel loop *) @@ -511,7 +511,11 @@ let loop ~opts ~state = print_emacs := opts.config.print_emacs; (* We initialize the console only if we run the toploop_run *) let tl_feed = Feedback.add_feeder coqloop_feed in - let _ = loop ~state in + (* Initialize buffer *) + Sys.catch_break true; + reset_input_buffer state.Vernac.State.doc stdin top_buffer; + (* Call the main loop *) + let _ : Vernac.State.t = vernac_loop ~state in (* Initialise and launch the Ocaml toplevel *) Coqinit.init_ocaml_path(); Mltop.ocaml_toploop(); diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index bcc5f54505..d6db4a735c 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -824,7 +824,6 @@ let register_struct ?local str = match str with let _ = Goptions.declare_bool_option { Goptions.optdepr = false; - Goptions.optname = "print Ltac2 backtrace"; Goptions.optkey = ["Ltac2"; "Backtrace"]; Goptions.optread = (fun () -> !Tac2interp.print_ltac2_backtrace); Goptions.optwrite = (fun b -> Tac2interp.print_ltac2_backtrace := b); diff --git a/user-contrib/Ltac2/tac2quote.ml b/user-contrib/Ltac2/tac2quote.ml index 645b92c302..26ffe000ad 100644 --- a/user-contrib/Ltac2/tac2quote.ml +++ b/user-contrib/Ltac2/tac2quote.ml @@ -236,7 +236,7 @@ let pattern_vars pat = in aux () Id.Set.empty pat -let abstract_vars loc vars tac = +let abstract_vars loc ?typ vars tac = let get_name = function Name id -> Some id | Anonymous -> None in let def = try Some (List.find_map get_name vars) with Not_found -> None in let na, tac = match def with @@ -258,7 +258,15 @@ let abstract_vars loc vars tac = let tac = CAst.make ?loc @@ CTacLet (false, bnd, tac) in (Name id0, tac) in - CAst.make ?loc @@ CTacFun ([CAst.make ?loc @@ CPatVar na], tac) + let pat = CAst.make ?loc @@ CPatVar na in + let pat = match typ with + | None -> pat + | Some typ -> + let t_array = coq_core "array" in + let typ = CAst.make ?loc @@ CTypRef (AbsKn (Other t_array), [typ]) in + CAst.make ?loc @@ CPatCnv (pat, typ) + in + CAst.make ?loc @@ CTacFun ([pat], tac) let of_pattern p = inj_wit ?loc:p.CAst.loc wit_pattern p @@ -400,7 +408,12 @@ let of_constr_matching {loc;v=m} = (* Order of elements is crucial here! *) let vars = Id.Set.elements vars in let vars = List.map (fun id -> Name id) vars in - let e = abstract_vars loc vars tac in + (* Annotate the bound array variable with constr type *) + let typ = + let t_constr = coq_core "constr" in + CAst.make ?loc @@ CTypRef (AbsKn (Other t_constr), []) + in + let e = abstract_vars loc ~typ vars tac in let e = CAst.make ?loc @@ CTacFun ([CAst.make ?loc @@ CPatVar na], e) in let pat = inj_wit ?loc:ploc wit_pattern pat in of_tuple [knd; pat; e] diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 9f92eba729..46f616c4ff 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -239,10 +239,17 @@ and traverse_inductive (curr, data, ax2ty) mind obj = in (* Build the context of all arities *) let arities_ctx = - let global_env = Global.env () in + let instance = + let open Univ in + Instance.of_array + (Array.init + (AUContext.size + (Declareops.inductive_polymorphic_context mib)) + Level.var) + in Array.fold_left (fun accu oib -> - let pspecif = Univ.in_punivs (mib, oib) in - let ind_type = Inductive.type_of_inductive global_env pspecif in + let pspecif = ((mib, oib), instance) in + let ind_type = Inductive.type_of_inductive pspecif in let indr = oib.mind_relevance in let ind_name = Name oib.mind_typename in Context.Rel.add (Context.Rel.Declaration.LocalAssum (make_annot ind_name indr, ind_type)) accu) diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 68d2c3a00d..194308b77f 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -154,7 +154,6 @@ let program_mode = ref false let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "use of the program extension"; optkey = program_mode_option_name; optread = (fun () -> !program_mode); optwrite = (fun b -> program_mode:=b) } @@ -188,7 +187,6 @@ let is_universe_polymorphism = let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "universe polymorphism"; optkey = universe_polymorphism_option_name; optread = (fun () -> !b); optwrite = ((:=) b) } diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 6bdb3159cf..bdf8511cce 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -178,7 +178,7 @@ let build_beq_scheme mode kn = (* current inductive we are working on *) let cur_packet = mib.mind_packets.(snd (fst ind)) in (* Inductive toto : [rettyp] := *) - let rettyp = Inductive.type_of_inductive env ((mib,cur_packet),u) in + let rettyp = Inductive.type_of_inductive ((mib,cur_packet),u) in (* split rettyp in a list without the non rec params and the last -> e.g. Inductive vec (A:Set) : nat -> Set := ... will do [nat] *) let rettyp_l = quick_chop nparrec (deconstruct_type rettyp) in diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index dce0a70f72..d711c9aea0 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -42,7 +42,6 @@ let should_auto_template = let auto = ref true in let () = declare_bool_option { optdepr = false; - optname = "Automatically make some inductive types template polymorphic"; optkey = ["Auto";"Template";"Polymorphism"]; optread = (fun () -> !auto); optwrite = (fun b -> auto := b); } diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index b56b9c8ce2..dcb28b898f 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -56,7 +56,7 @@ type program_info = let get_shrink_obligations = Goptions.declare_bool_option_and_ref ~depr:true (* remove in 8.8 *) - ~name:"Shrinking of Program obligations" ~key:["Shrink"; "Obligations"] + ~key:["Shrink"; "Obligations"] ~value:true (* XXX: Is this the right place for this? *) @@ -133,7 +133,6 @@ let add_hint local prg cst = let get_hide_obligations = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"Hidding of Program obligations" ~key:["Hide"; "Obligations"] ~value:false diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index d0374bc4fa..74249301d7 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -21,7 +21,6 @@ open Constrexpr_ops open Extend open Decls open Declaremods -open Declarations open Namegen open Tok (* necessary for camlp5 *) @@ -200,9 +199,7 @@ GRAMMAR EXTEND Gram (* Gallina inductive declarations *) | cum = OPT cumulativity_token; priv = private_token; f = finite_token; indl = LIST1 inductive_definition SEP "with" -> - { let (k,f) = f in - let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in - VernacInductive (cum, priv,f,indl) } + { VernacInductive (cum, priv, f, indl) } | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> { VernacFixpoint (NoDischarge, recs) } | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> @@ -337,12 +334,12 @@ GRAMMAR EXTEND Gram ] ] ; finite_token: - [ [ IDENT "Inductive" -> { (Inductive_kw,Finite) } - | IDENT "CoInductive" -> { (CoInductive,CoFinite) } - | IDENT "Variant" -> { (Variant,BiFinite) } - | IDENT "Record" -> { (Record,BiFinite) } - | IDENT "Structure" -> { (Structure,BiFinite) } - | IDENT "Class" -> { (Class true,BiFinite) } ] ] + [ [ IDENT "Inductive" -> { Inductive_kw } + | IDENT "CoInductive" -> { CoInductive } + | IDENT "Variant" -> { Variant } + | IDENT "Record" -> { Record } + | IDENT "Structure" -> { Structure } + | IDENT "Class" -> { Class true } ] ] ; cumulativity_token: [ [ IDENT "Cumulative" -> { VernacCumulative } diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 2f0b1062a7..227d2f1554 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -44,7 +44,6 @@ let elim_flag = ref true let () = declare_bool_option { optdepr = false; - optname = "automatic declaration of induction schemes"; optkey = ["Elimination";"Schemes"]; optread = (fun () -> !elim_flag) ; optwrite = (fun b -> elim_flag := b) } @@ -53,7 +52,6 @@ let bifinite_elim_flag = ref false let () = declare_bool_option { optdepr = false; - optname = "automatic declaration of induction schemes for non-recursive types"; optkey = ["Nonrecursive";"Elimination";"Schemes"]; optread = (fun () -> !bifinite_elim_flag) ; optwrite = (fun b -> bifinite_elim_flag := b) } @@ -62,7 +60,6 @@ let case_flag = ref false let () = declare_bool_option { optdepr = false; - optname = "automatic declaration of case analysis schemes"; optkey = ["Case";"Analysis";"Schemes"]; optread = (fun () -> !case_flag) ; optwrite = (fun b -> case_flag := b) } @@ -71,7 +68,6 @@ let eq_flag = ref false let () = declare_bool_option { optdepr = false; - optname = "automatic declaration of boolean equality"; optkey = ["Boolean";"Equality";"Schemes"]; optread = (fun () -> !eq_flag) ; optwrite = (fun b -> eq_flag := b) } @@ -82,7 +78,6 @@ let eq_dec_flag = ref false let () = declare_bool_option { optdepr = false; - optname = "automatic declaration of decidable equality"; optkey = ["Decidable";"Equality";"Schemes"]; optread = (fun () -> !eq_dec_flag) ; optwrite = (fun b -> eq_dec_flag := b) } @@ -91,7 +86,6 @@ let rewriting_flag = ref false let () = declare_bool_option { optdepr = false; - optname ="automatic declaration of rewriting schemes for equality types"; optkey = ["Rewriting";"Schemes"]; optread = (fun () -> !rewriting_flag) ; optwrite = (fun b -> rewriting_flag := b) } diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 865eded545..f7606f4ede 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -268,7 +268,6 @@ let warn_let_as_axiom = let get_keep_admitted_vars = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"keep section variables in admitted proofs" ~key:["Keep"; "Admitted"; "Variables"] ~value:true diff --git a/vernac/mltop.ml b/vernac/mltop.ml index 2bac35b08f..ab9d008659 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -11,7 +11,6 @@ open CErrors open Util open Pp -open Libobject open System (* Code to hook Coq into the ML toplevel -- depends on having the @@ -304,23 +303,38 @@ let _ = (* Liboject entries of declared ML Modules *) +(* Digest of module used to compile the file *) +type ml_module_digest = + | NoDigest + | AnyDigest of Digest.t (* digest of any used cma / cmxa *) + type ml_module_object = { mlocal : Vernacexpr.locality_flag; - mnames : string list + mnames : (string * ml_module_digest) list } +let add_module_digest m = + try + let file = file_of_name m in + let path, file = System.where_in_path ~warn:false !coq_mlpath_copy file in + m, AnyDigest (Digest.file file) + with + | Not_found -> + m, NoDigest + let cache_ml_objects (_,{mnames=mnames}) = - let iter obj = trigger_ml_object true true true obj in + let iter (obj, _) = trigger_ml_object true true true obj in List.iter iter mnames let load_ml_objects _ (_,{mnames=mnames}) = - let iter obj = trigger_ml_object true false true obj in + let iter (obj, _) = trigger_ml_object true false true obj in List.iter iter mnames let classify_ml_objects ({mlocal=mlocal} as o) = - if mlocal then Dispose else Substitute o + if mlocal then Libobject.Dispose else Libobject.Substitute o -let inMLModule : ml_module_object -> obj = +let inMLModule : ml_module_object -> Libobject.obj = + let open Libobject in declare_object {(default_object "ML-MODULE") with cache_function = cache_ml_objects; @@ -330,6 +344,7 @@ let inMLModule : ml_module_object -> obj = let declare_ml_modules local l = let l = List.map mod_of_name l in + let l = List.map add_module_digest l in Lib.add_anonymous_leaf ~cache_first:false (inMLModule {mlocal=local; mnames=l}) let print_ml_path () = diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 82132a1af6..6240120cb0 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -476,7 +476,7 @@ let string_of_theorem_kind = let open Decls in function let prpri = match pri with None -> mt() | Some i -> str "| " ++ int i in prx ++ prpri ++ prlist (pr_decl_notation @@ pr_constr env sigma) ntn - let pr_record_decl b c fs = + let pr_record_decl c fs = pr_opt pr_lident c ++ (if c = None then str"{" else str" {") ++ hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}") @@ -802,7 +802,7 @@ let string_of_definition_object_kind = let open Decls in function (if coe then str":>" else str":") ++ Flags.without_option Flags.beautify pr_spc_lconstr c) in - let pr_constructor_list b l = match l with + let pr_constructor_list l = match l with | Constructors [] -> mt() | Constructors l -> let fst_sep = match l with [_] -> " " | _ -> " | " in @@ -810,21 +810,20 @@ let string_of_definition_object_kind = let open Decls in function fnl() ++ str fst_sep ++ prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l | RecordDecl (c,fs) -> - pr_record_decl b c fs + pr_record_decl c fs in - let pr_oneind key (((coe,iddecl),indpar,s,k,lc),ntn) = + let pr_oneind key (((coe,iddecl),indpar,s,lc),ntn) = hov 0 ( str key ++ spc() ++ (if coe then str"> " else str"") ++ pr_ident_decl iddecl ++ pr_and_type_binders_arg indpar ++ pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr env sigma s) s ++ - str" :=") ++ pr_constructor_list k lc ++ + str" :=") ++ pr_constructor_list lc ++ prlist (pr_decl_notation @@ pr_constr env sigma) ntn in let key = - let (_,_,_,k,_),_ = List.hd l in let kind = - match k with Record -> "Record" | Structure -> "Structure" + match f with Record -> "Record" | Structure -> "Structure" | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" | Class _ -> "Class" | Variant -> "Variant" in diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index cfb3248c7b..b329463cb0 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -140,7 +140,6 @@ let suggest_proof_using = ref false let () = Goptions.(declare_bool_option { optdepr = false; - optname = "suggest Proof using"; optkey = ["Suggest";"Proof";"Using"]; optread = (fun () -> !suggest_proof_using); optwrite = ((:=) suggest_proof_using) }) @@ -176,7 +175,6 @@ let proof_using_opt_name = ["Default";"Proof";"Using"] let () = Goptions.(declare_stringopt_option { optdepr = false; - optname = "default value for Proof using"; optkey = proof_using_opt_name; optread = (fun () -> Option.map using_to_string !value); optwrite = (fun b -> value := Option.map using_from_string b); diff --git a/vernac/record.ml b/vernac/record.ml index f6945838d7..3e44cd85cc 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -39,7 +39,6 @@ let primitive_flag = ref false let () = declare_bool_option { optdepr = false; - optname = "use of primitive projections"; optkey = ["Primitive";"Projections"]; optread = (fun () -> !primitive_flag) ; optwrite = (fun b -> primitive_flag := b) } @@ -48,7 +47,6 @@ let typeclasses_strict = ref false let () = declare_bool_option { optdepr = false; - optname = "strict typeclass resolution"; optkey = ["Typeclasses";"Strict";"Resolution"]; optread = (fun () -> !typeclasses_strict); optwrite = (fun b -> typeclasses_strict := b); } @@ -57,7 +55,6 @@ let typeclasses_unique = ref false let () = declare_bool_option { optdepr = false; - optname = "unique typeclass instances"; optkey = ["Typeclasses";"Unique";"Instances"]; optread = (fun () -> !typeclasses_unique); optwrite = (fun b -> typeclasses_unique := b); } @@ -625,7 +622,7 @@ let add_inductive_class env sigma ind = let env = push_context ~strict:false (Univ.AUContext.repr univs) env in let env = push_rel_context ctx env in let inst = Univ.make_abstract_instance univs in - let ty = Inductive.type_of_inductive env ((mind, oneind), inst) in + let ty = Inductive.type_of_inductive ((mind, oneind), inst) in let r = Inductive.relevance_of_inductive env ind in { cl_univs = univs; cl_impl = GlobRef.IndRef ind; diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index fd588f5b15..e469323f50 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -611,7 +611,6 @@ let vernac_assumption ~atts discharge kind l nl = let is_polymorphic_inductive_cumulativity = declare_bool_option_and_ref ~depr:false ~value:false - ~name:"Polymorphic inductive cumulativity" ~key:["Polymorphic"; "Inductive"; "Cumulativity"] let should_treat_as_cumulative cum poly = @@ -624,17 +623,18 @@ let should_treat_as_cumulative cum poly = else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.") | None -> poly && is_polymorphic_inductive_cumulativity () -let get_uniform_inductive_parameters = - Goptions.declare_bool_option_and_ref - ~depr:false - ~name:"Uniform inductive parameters" - ~key:["Uniform"; "Inductive"; "Parameters"] - ~value:false - -let should_treat_as_uniform () = - if get_uniform_inductive_parameters () - then ComInductive.UniformParameters - else ComInductive.NonUniformParameters +let uniform_att = + let get_uniform_inductive_parameters = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Uniform"; "Inductive"; "Parameters"] + ~value:false + in + let open Attributes.Notations in + Attributes.bool_attribute ~name:"uniform" ~on:"uniform" ~off:"nonuniform" >>= fun u -> + let u = match u with Some u -> u | None -> get_uniform_inductive_parameters () in + let u = if u then ComInductive.UniformParameters else ComInductive.NonUniformParameters in + return u let vernac_record ~template udecl cum k poly finite records = let cumulative = should_treat_as_cumulative cum poly in @@ -663,25 +663,29 @@ let vernac_record ~template udecl cum k poly finite records = let extract_inductive_udecl (indl:(inductive_expr * decl_notation list) list) = match indl with | [] -> assert false - | (((coe,(id,udecl)),b,c,k,d),e) :: rest -> - let rest = List.map (fun (((coe,(id,udecl)),b,c,k,d),e) -> + | (((coe,(id,udecl)),b,c,d),e) :: rest -> + let rest = List.map (fun (((coe,(id,udecl)),b,c,d),e) -> if Option.has_some udecl then user_err ~hdr:"inductive udecl" Pp.(strbrk "Universe binders must be on the first inductive of the block.") - else (((coe,id),b,c,k,d),e)) + else (((coe,id),b,c,d),e)) rest in - udecl, (((coe,id),b,c,k,d),e) :: rest + udecl, (((coe,id),b,c,d),e) :: rest + +let finite_of_kind = let open Declarations in function + | Inductive_kw -> Finite + | CoInductive -> CoFinite + | Variant | Record | Structure | Class _ -> BiFinite (** When [poly] is true the type is declared polymorphic. When [lo] is true, then the type is declared private (as per the [Private] keyword). [finite] indicates whether the type is inductive, co-inductive or neither. *) -let vernac_inductive ~atts cum lo finite indl = - let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in +let vernac_inductive ~atts cum lo kind indl = let open Pp in let udecl, indl = extract_inductive_udecl indl in if Dumpglob.dump () then - List.iter (fun (((coe,lid), _, _, _, cstrs), _) -> + List.iter (fun (((coe,lid), _, _, cstrs), _) -> match cstrs with | Constructors cstrs -> Dumpglob.dump_definition lid false "ind"; @@ -690,16 +694,17 @@ let vernac_inductive ~atts cum lo finite indl = | _ -> () (* dumping is done by vernac_record (called below) *) ) indl; + let finite = finite_of_kind kind in let is_record = function - | ((_ , _ , _ , _, RecordDecl _), _) -> true + | ((_ , _ , _ , RecordDecl _), _) -> true | _ -> false in let is_constructor = function - | ((_ , _ , _ , _, Constructors _), _) -> true + | ((_ , _ , _ , Constructors _), _) -> true | _ -> false in - let is_defclass = match indl with - | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> Some (id, bl, c, l) + let is_defclass = match kind, indl with + | Class _, [ ( id , bl , c , Constructors [l]), [] ] -> Some (id, bl, c, l) | _ -> None in if Option.has_some is_defclass then @@ -708,42 +713,42 @@ let vernac_inductive ~atts cum lo finite indl = let (coe, (lid, ce)) = l in let coe' = if coe then Some true else None in let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce), - { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } in + { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } + in + let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in vernac_record ~template udecl cum (Class true) poly finite [id, bl, c, None, [f]] else if List.for_all is_record indl then (* Mutual record case *) - let check_kind ((_, _, _, kind, _), _) = match kind with - | Variant -> - user_err (str "The Variant keyword does not support syntax { ... }.") - | Record | Structure | Class _ | Inductive_kw | CoInductive -> () + let () = match kind with + | Variant -> + user_err (str "The Variant keyword does not support syntax { ... }.") + | Record | Structure | Class _ | Inductive_kw | CoInductive -> () in - let () = List.iter check_kind indl in - let check_where ((_, _, _, _, _), wh) = match wh with + let check_where ((_, _, _, _), wh) = match wh with | [] -> () | _ :: _ -> user_err (str "where clause not supported for records") in let () = List.iter check_where indl in - let unpack ((id, bl, c, _, decl), _) = match decl with + let unpack ((id, bl, c, decl), _) = match decl with | RecordDecl (oc, fs) -> (id, bl, c, oc, fs) | Constructors _ -> assert false (* ruled out above *) in - let ((_, _, _, kind, _), _) = List.hd indl in let kind = match kind with Class _ -> Class false | _ -> kind in let recordl = List.map unpack indl in + let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in vernac_record ~template udecl cum kind poly finite recordl else if List.for_all is_constructor indl then (* Mutual inductive case *) - let check_kind ((_, _, _, kind, _), _) = match kind with + let () = match kind with | (Record | Structure) -> user_err (str "The Record keyword is for types defined using the syntax { ... }.") | Class _ -> user_err (str "Inductive classes not supported") | Variant | Inductive_kw | CoInductive -> () in - let () = List.iter check_kind indl in - let check_name ((na, _, _, _, _), _) = match na with + let check_name ((na, _, _, _), _) = match na with | (true, _) -> user_err (str "Variant types do not handle the \"> Name\" \ syntax, which is reserved for records. Use the \":>\" \ @@ -751,26 +756,19 @@ let vernac_inductive ~atts cum lo finite indl = | _ -> () in let () = List.iter check_name indl in - let unpack (((_, id) , bl, c, _, decl), ntn) = match decl with + let unpack (((_, id) , bl, c, decl), ntn) = match decl with | Constructors l -> (id, bl, c, l), ntn | RecordDecl _ -> assert false (* ruled out above *) in let indl = List.map unpack indl in + let (template, poly), uniform = + Attributes.(parse Notations.(template ++ polymorphic ++ uniform_att) atts) + in let cumulative = should_treat_as_cumulative cum poly in - let uniform = should_treat_as_uniform () in - ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind:lo ~uniform finite + ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly + ~private_ind:lo ~uniform finite else user_err (str "Mixed record-inductive definitions are not allowed") -(* - - match indl with - | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> - let f = - let (coe, ({loc;v=id}, ce)) = l in - let coe' = if coe then Some true else None in - (((coe', AssumExpr ((make ?loc @@ Name id), ce)), None), []) - in vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]] - *) let vernac_fixpoint_common ~atts discharge l = if Dumpglob.dump () then @@ -1220,7 +1218,6 @@ let vernac_generalizable ~local = let () = declare_bool_option { optdepr = false; - optname = "allow sprop"; optkey = ["Allow";"StrictProp"]; optread = (fun () -> Global.sprop_allowed()); optwrite = Global.set_allow_sprop } @@ -1228,7 +1225,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "silent"; optkey = ["Silent"]; optread = (fun () -> !Flags.quiet); optwrite = ((:=) Flags.quiet) } @@ -1236,7 +1232,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "implicit arguments"; optkey = ["Implicit";"Arguments"]; optread = Impargs.is_implicit_args; optwrite = Impargs.make_implicit_args } @@ -1244,7 +1239,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "strict implicit arguments"; optkey = ["Strict";"Implicit"]; optread = Impargs.is_strict_implicit_args; optwrite = Impargs.make_strict_implicit_args } @@ -1252,7 +1246,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "strong strict implicit arguments"; optkey = ["Strongly";"Strict";"Implicit"]; optread = Impargs.is_strongly_strict_implicit_args; optwrite = Impargs.make_strongly_strict_implicit_args } @@ -1260,7 +1253,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "contextual implicit arguments"; optkey = ["Contextual";"Implicit"]; optread = Impargs.is_contextual_implicit_args; optwrite = Impargs.make_contextual_implicit_args } @@ -1268,7 +1260,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "implicit status of reversible patterns"; optkey = ["Reversible";"Pattern";"Implicit"]; optread = Impargs.is_reversible_pattern_implicit_args; optwrite = Impargs.make_reversible_pattern_implicit_args } @@ -1276,7 +1267,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "maximal insertion of implicit"; optkey = ["Maximal";"Implicit";"Insertion"]; optread = Impargs.is_maximal_implicit_args; optwrite = Impargs.make_maximal_implicit_args } @@ -1284,7 +1274,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "coercion printing"; optkey = ["Printing";"Coercions"]; optread = (fun () -> !Constrextern.print_coercions); optwrite = (fun b -> Constrextern.print_coercions := b) } @@ -1292,7 +1281,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "printing of existential variable instances"; optkey = ["Printing";"Existential";"Instances"]; optread = (fun () -> !Detyping.print_evar_arguments); optwrite = (:=) Detyping.print_evar_arguments } @@ -1300,7 +1288,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "implicit arguments printing"; optkey = ["Printing";"Implicit"]; optread = (fun () -> !Constrextern.print_implicits); optwrite = (fun b -> Constrextern.print_implicits := b) } @@ -1308,7 +1295,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "implicit arguments defensive printing"; optkey = ["Printing";"Implicit";"Defensive"]; optread = (fun () -> !Constrextern.print_implicits_defensive); optwrite = (fun b -> Constrextern.print_implicits_defensive := b) } @@ -1316,7 +1302,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "projection printing using dot notation"; optkey = ["Printing";"Projections"]; optread = (fun () -> !Constrextern.print_projections); optwrite = (fun b -> Constrextern.print_projections := b) } @@ -1324,7 +1309,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "notations printing"; optkey = ["Printing";"Notations"]; optread = (fun () -> not !Constrextern.print_no_symbol); optwrite = (fun b -> Constrextern.print_no_symbol := not b) } @@ -1332,7 +1316,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "raw printing"; optkey = ["Printing";"All"]; optread = (fun () -> !Flags.raw_print); optwrite = (fun b -> Flags.raw_print := b) } @@ -1340,7 +1323,6 @@ let () = let () = declare_int_option { optdepr = false; - optname = "the level of inlining during functor application"; optkey = ["Inline";"Level"]; optread = (fun () -> Some (Flags.get_inline_level ())); optwrite = (fun o -> @@ -1350,7 +1332,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "kernel term sharing"; optkey = ["Kernel"; "Term"; "Sharing"]; optread = (fun () -> (Global.typing_flags ()).Declarations.share_reduction); optwrite = Global.set_share_reduction } @@ -1358,7 +1339,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "display compact goal contexts"; optkey = ["Printing";"Compact";"Contexts"]; optread = (fun () -> Printer.get_compact_context()); optwrite = (fun b -> Printer.set_compact_context b) } @@ -1366,7 +1346,6 @@ let () = let () = declare_int_option { optdepr = false; - optname = "the printing depth"; optkey = ["Printing";"Depth"]; optread = Topfmt.get_depth_boxes; optwrite = Topfmt.set_depth_boxes } @@ -1374,7 +1353,6 @@ let () = let () = declare_int_option { optdepr = false; - optname = "the printing width"; optkey = ["Printing";"Width"]; optread = Topfmt.get_margin; optwrite = Topfmt.set_margin } @@ -1382,7 +1360,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "printing of universes"; optkey = ["Printing";"Universes"]; optread = (fun () -> !Constrextern.print_universes); optwrite = (fun b -> Constrextern.print_universes:=b) } @@ -1390,7 +1367,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "dumping bytecode after compilation"; optkey = ["Dump";"Bytecode"]; optread = (fun () -> !Cbytegen.dump_bytecode); optwrite = (:=) Cbytegen.dump_bytecode } @@ -1398,7 +1374,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "dumping VM lambda code after compilation"; optkey = ["Dump";"Lambda"]; optread = (fun () -> !Clambda.dump_lambda); optwrite = (:=) Clambda.dump_lambda } @@ -1406,7 +1381,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "explicitly parsing implicit arguments"; optkey = ["Parsing";"Explicit"]; optread = (fun () -> !Constrintern.parsing_explicit); optwrite = (fun b -> Constrintern.parsing_explicit := b) } @@ -1414,7 +1388,6 @@ let () = let () = declare_string_option ~preprocess:CWarnings.normalize_flags_string { optdepr = false; - optname = "warnings display"; optkey = ["Warnings"]; optread = CWarnings.get_flags; optwrite = CWarnings.set_flags } @@ -1422,7 +1395,6 @@ let () = let () = declare_string_option { optdepr = false; - optname = "native_compute profiler output"; optkey = ["NativeCompute"; "Profile"; "Filename"]; optread = Nativenorm.get_profile_filename; optwrite = Nativenorm.set_profile_filename } @@ -1430,7 +1402,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "enable native compute profiling"; optkey = ["NativeCompute"; "Profiling"]; optread = Nativenorm.get_profiling_enabled; optwrite = Nativenorm.set_profiling_enabled } @@ -1438,7 +1409,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "enable native compute timing"; optkey = ["NativeCompute"; "Timing"]; optread = Nativenorm.get_timing_enabled; optwrite = Nativenorm.set_timing_enabled } @@ -1446,7 +1416,6 @@ let () = let _ = declare_bool_option { optdepr = false; - optname = "guard checking"; optkey = ["Guard"; "Checking"]; optread = (fun () -> (Global.typing_flags ()).Declarations.check_guarded); optwrite = (fun b -> Global.set_check_guarded b) } @@ -1454,7 +1423,6 @@ let _ = let _ = declare_bool_option { optdepr = false; - optname = "positivity/productivity checking"; optkey = ["Positivity"; "Checking"]; optread = (fun () -> (Global.typing_flags ()).Declarations.check_positive); optwrite = (fun b -> Global.set_check_positive b) } @@ -1462,7 +1430,6 @@ let _ = let _ = declare_bool_option { optdepr = false; - optname = "universes checking"; optkey = ["Universe"; "Checking"]; optread = (fun () -> (Global.typing_flags ()).Declarations.check_universes); optwrite = (fun b -> Global.set_check_universes b) } @@ -1777,7 +1744,6 @@ let search_output_name_only = ref false let () = declare_bool_option { optdepr = false; - optname = "output-name-only search"; optkey = ["Search";"Output";"Name";"Only"]; optread = (fun () -> !search_output_name_only); optwrite = (:=) search_output_name_only } diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 22a8de7f99..8ead56dfdf 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -104,7 +104,6 @@ type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) type instance_flag = bool option (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) type export_flag = bool (* true = Export; false = Import *) -type inductive_flag = Declarations.recursivity_kind type onlyparsing_flag = { onlyparsing : bool } (* Some v = Parse only; None = Print also. If v<>Current, it contains the name of the coq version @@ -165,7 +164,7 @@ type constructor_list_or_record_decl_expr = | Constructors of constructor_expr list | RecordDecl of lident option * (local_decl_expr * record_field_attr) list type inductive_expr = - ident_decl with_coercion * local_binder_expr list * constr_expr option * inductive_kind * + ident_decl with_coercion * local_binder_expr list * constr_expr option * constructor_list_or_record_decl_expr type one_inductive_expr = @@ -306,7 +305,7 @@ type nonrec vernac_expr = | VernacExactProof of constr_expr | VernacAssumption of (discharge * Decls.assumption_object_kind) * Declaremods.inline * (ident_decl list * constr_expr) with_coercion list - | VernacInductive of vernac_cumulative option * bool (* private *) * inductive_flag * (inductive_expr * decl_notation list) list + | VernacInductive of vernac_cumulative option * bool (* private *) * inductive_kind * (inductive_expr * decl_notation list) list | VernacFixpoint of discharge * fixpoint_expr list | VernacCoFixpoint of discharge * cofixpoint_expr list | VernacScheme of (lident option * scheme) list diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index c14fc78462..1ec09b6beb 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -65,7 +65,6 @@ let proof_mode_opt_name = ["Default";"Proof";"Mode"] let () = Goptions.declare_string_option Goptions.{ optdepr = false; - optname = "default proof mode" ; optkey = proof_mode_opt_name; optread = get_default_proof_mode_opt; optwrite = set_default_proof_mode_opt; @@ -249,7 +248,6 @@ let interp_qed_delayed_control ~proof ~info ~st ~control { CAst.loc; v=pe } = let () = let open Goptions in declare_int_option { optdepr = false; - optname = "the default timeout"; optkey = ["Default";"Timeout"]; optread = (fun () -> !default_timeout); optwrite = ((:=) default_timeout) } |