diff options
116 files changed, 1195 insertions, 1828 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index f439b0c34f..1a1d31bdd7 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -716,7 +716,11 @@ library:ci-fiat-crypto: - plugin:ci-rewriter library:ci-flocq: - extends: .ci-template + extends: .ci-template-flambda + artifacts: + name: "$CI_JOB_NAME" + paths: + - _build_ci library:ci-corn: extends: .ci-template-flambda @@ -772,6 +776,13 @@ library:ci-verdi-raft: library:ci-vst: extends: .ci-template-flambda + stage: stage-3 + needs: + - build:edge+flambda + - library:ci-flocq + dependencies: + - build:edge+flambda + - library:ci-flocq # Plugins are by definition the projects that depend on Coq's ML API diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 201d740073..3582d18cf6 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -30,17 +30,18 @@ well. - [Helping triage existing issues](#helping-triage-existing-issues) - [Code changes](#code-changes) - [Using GitHub pull requests](#using-github-pull-requests) + - [Fixing bugs and performing small changes](#fixing-bugs-and-performing-small-changes) + - [Proposing large changes: Coq Enhancement Proposals](#proposing-large-changes-coq-enhancement-proposals) + - [Seeking early feedback on work-in-progress](#seeking-early-feedback-on-work-in-progress) - [Taking feedback into account](#taking-feedback-into-account) - [Understanding automatic feedback](#understanding-automatic-feedback) - [Understanding reviewers' feedback](#understanding-reviewers-feedback) - [Fixing your branch](#fixing-your-branch) - [Improving the official documentation](#improving-the-official-documentation) - [Contributing to the standard library](#contributing-to-the-standard-library) - - [Fixing bugs and performing small changes](#fixing-bugs-and-performing-small-changes) - - [Proposing large changes: Coq Enhancement Proposals](#proposing-large-changes-coq-enhancement-proposals) - - [Collaborating on a pull request](#collaborating-on-a-pull-request) - [Becoming a maintainer](#becoming-a-maintainer) - [Reviewing pull requests](#reviewing-pull-requests) + - [Collaborating on a pull request](#collaborating-on-a-pull-request) - [Merging pull requests](#merging-pull-requests) - [Additional notes for pull request reviewers and assignees](#additional-notes-for-pull-request-reviewers-and-assignees) - [Joining / leaving maintainer teams](#joining--leaving-maintainer-teams) @@ -443,6 +444,72 @@ several months after your PR is merged). That said, you can start using the latest Coq `master` branch to take advantage of all the new features, improvements, and fixes. +#### Fixing bugs and performing small changes #### + +Before fixing a bug, it is best to check that it was reported before: + +- If it was already reported and you intend to fix it, self-assign the + issue (if you have the permission), or leave a comment marking your + intention to work on it (and a contributor with write-access may + then assign the issue to you). + +- If the issue already has an assignee, you should check with them if + they still intend to work on it. If the assignment is several + weeks, months, or even years (!) old, there are good chances that it + does not reflect their current priorities. + +- If the bug has not been reported before, it can be a good idea to + open an issue about it, while stating that you are preparing a fix. + The issue can be the place to discuss about the bug itself while the + PR will be the place to discuss your proposed fix. + +It is generally a good idea to add a regression test to the +test-suite. See the test-suite [README][test-suite-README] for how to +do so. + +Small fixes do not need any documentation, or changelog update. New, +or updated, user-facing features, and major bug fixes do. See above +on how to contribute to the documentation, and the README in +[`doc/changelog`][user-changelog] for how to add a changelog entry. + +#### Proposing large changes: Coq Enhancement Proposals #### + +You are always welcome to open a PR for a change of any size. +However, you should be aware that the larger the change, the higher +the chances it will take very long to review, and possibly never get +merged. + +So it is recommended that before spending a lot of time coding, you +seek feedback from maintainers to see if your change would be +supported, and if they have recommendations about its implementation. +You can do this informally by opening an issue, or more formally by +producing a design document as a [Coq Enhancement Proposal][CEP]. + +Another recommendation is that you do not put several unrelated +changes in the same PR (even if you produced them together). In +particular, make sure you split bug fixes into separate PRs when this +is possible. More generally, smaller-sized PRs, or PRs changing less +components, are more likely to be reviewed and merged promptly. + +#### Seeking early feedback on work-in-progress #### + +You should always feel free to open your PR before the documentation, +changelog entry and tests are ready. That's the purpose of the +checkboxes in the PR template which you can leave unticked. This can +be a way of getting reviewers' approval before spending time on +writing the documentation (but you should still do it before your PR +can be merged). + +If even the implementation is not ready but you are still looking for +early feedback on your code changes, please use the [draft +PR](#draft-pull-requests) mechanism. + +If you are looking for feedback on the design of your change, rather +than on its implementation, then please refrain from opening a PR. +You may open an issue to start a discussion, or create a [Coq +Enhancement Proposal][CEP] if you have a clear enough view of the +design to write a document about it. + ### Taking feedback into account ### #### Understanding automatic feedback #### @@ -644,59 +711,35 @@ Add coqdoc comments to extend the [standard library documentation][stdlib-doc]. See the [coqdoc documentation][coqdoc-documentation] to learn more. -### Fixing bugs and performing small changes ### - -Before fixing a bug, it is best to check that it was reported before: - -- If it was already reported and you intend to fix it, self-assign the - issue (if you have the permission), or leave a comment marking your - intention to work on it (and a contributor with write-access may - then assign the issue to you). - -- If the issue already has an assignee, you should check with them if - they still intend to work on it. If the assignment is several - weeks, months, or even years (!) old, there are good chances that it - does not reflect their current priorities. - -- If the bug has not been reported before, it can be a good idea to - open an issue about it, while stating that you are preparing a fix. - The issue can be the place to discuss about the bug itself while the - PR will be the place to discuss your proposed fix. - -In any case, feel free to just ignore the recommendation above, and -jump ahead and open a PR with your fix. If it is not yet complete, do -not hesitate to open a [*draft PR*][GitHub-draft-PR] to get early -feedback, and talk to developers on [Gitter][]. - -It is generally a good idea to add a regression test to the -test-suite. See the test-suite [README][test-suite-README] for how to -do so. - -Small fixes do not need any documentation, or changelog update. New, -or updated, user-facing features, and major bug fixes do. See above -on how to contribute to the documentation, and the README in -[`doc/changelog`][user-changelog] for how to add a changelog entry. +## Becoming a maintainer ## -### Proposing large changes: Coq Enhancement Proposals ### +### Reviewing pull requests ### -You are always welcome to open a PR for a change of any size. -However, you should be aware that the larger the change, the higher -the chances it will take very long to review, and possibly never get -merged. +You can start reviewing PRs as soon as you feel comfortable doing so +(anyone can review anything, although some designated reviewers +will have to give a final approval before a PR can be merged, as is +explained in the next sub-section). -So it is recommended that before spending a lot of time coding, you -seek feedback from maintainers to see if your change would be -supported, and if they have recommendations about its implementation. -You can do this informally by opening an issue, or more formally by -producing a design document as a [Coq Enhancement Proposal][CEP]. +Reviewers should ensure that the code that is changed or introduced is +in good shape and will not be a burden to maintain, is unlikely to +break anything, or the compatibility-breakage has been identified and +validated, includes documentation, changelog entries, and test files +when necessary. Reviewers can use labels, or change requests to +further emphasize what remains to be changed before they can approve +the PR. Once reviewers are satisfied (regarding the part they +reviewed), they should formally approve the PR, possibly stating what +they reviewed. -Another recommendation is that you do not put several unrelated -changes in the same PR (even if you produced them together). In -particular, make sure you split bug fixes into separate PRs when this -is possible. More generally, smaller-sized PRs, or PRs changing less -components, are more likely to be reviewed and merged promptly. +That being said, reviewers should also make sure that they do not make +the contributing process harder than necessary: they should make it +clear which comments are really required to perform before approving, +and which are just suggestions. They should strive to reduce the +number of rounds of feedback that are needed by posting most of their +comments at the same time. If they are opposed to the change, they +should clearly say so from the beginning to avoid the contributor +spending time in vain. -### Collaborating on a pull request ### +#### Collaborating on a pull request #### Beyond making suggestions to a PR author during the review process, you may want to collaborate further by checking out the code, making @@ -721,42 +764,14 @@ else), this should be reflected by adding ["Co-authored-by:" tags][GitHub-co-authored-by] at the end of the commit message. The line should contain the co-author name and committer e-mail address. -## Becoming a maintainer ## - -### Reviewing pull requests ### - -You can start reviewing PRs as soon as you feel comfortable doing so -(anyone can review anything, although some designated reviewers -will have to give a final approval before a PR can be merged, as is -explained in the next sub-section). - -Reviewers should ensure that the code that is changed or introduced is -in good shape and will not be a burden to maintain, is unlikely to -break anything, or the compatibility-breakage has been identified and -validated, includes documentation, changelog entries, and test files -when necessary. Reviewers can use labels, or change requests to -further emphasize what remains to be changed before they can approve -the PR. Once reviewers are satisfied (regarding the part they -reviewed), they should formally approve the PR, possibly stating what -they reviewed. - -That being said, reviewers should also make sure that they do not make -the contributing process harder than necessary: they should make it -clear which comments are really required to perform before approving, -and which are just suggestions. They should strive to reduce the -number of rounds of feedback that are needed by posting most of their -comments at the same time. If they are opposed to the change, they -should clearly say so from the beginning to avoid the contributor -spending time in vain. - ### Merging pull requests ### Our [CODEOWNERS][] file associates a team of maintainers to each -component. When a PR is opened (or a draft PR is marked as ready for -review), GitHub will automatically request reviews to maintainer teams -of affected components. As soon as it is the case, one available -member of a team that was requested a review should self-assign the -PR, and will act as its shepherd from then on. +component. When a PR is opened (or a [draft PR](#draft-pull-requests) +is marked as ready for review), GitHub will automatically request +reviews to maintainer teams of affected components. As soon as it is +the case, one available member of a team that was requested a review +should self-assign the PR, and will act as its shepherd from then on. The PR assignee is responsible for making sure that all the proposed changes have been reviewed by relevant maintainers (at least one @@ -1100,6 +1115,33 @@ interface to mark as read, save for later or mute threads. You can also manage your GitHub web notifications using a tool such as [Octobox][]. +##### Draft pull requests ##### + +[Draft PRs][GitHub-draft-PR] are a mechanism proposed by GitHub to +open a pull request before it is ready for review. + +Opening a draft PR is a way of announcing a change and seeking early +feedback without formally requesting maintainers' reviews. Indeed, +you should avoid cluttering our maintainers' review request lists +before a change is ready on your side. + +When opening a draft PR, make sure to give it a descriptive enough +title so that interested developers still notice it in their +notification feed. You may also advertise it by talking about it in +our [developer chat][Gitter]. If you know which developer would be +able to provide useful feedback to you, you may also ping them. + +###### Turning a PR into draft mode ###### + +If a PR was opened as ready for review, but it turns out that it still +needs work, it can be transformed into a draft PR. + +In this case, previous review requests won't be removed automatically. +Someone with write access to the repository should remove them +manually. Afterwards, upon marking the PR as ready for review, +someone with write access will have to manually add the review +requests that were previously removed. + #### GitLab documentation, tips and tricks #### We use GitLab mostly for its CI service. The [Coq organization on diff --git a/Makefile.build b/Makefile.build index 8a8500ba1a..d705219757 100644 --- a/Makefile.build +++ b/Makefile.build @@ -269,10 +269,6 @@ OPT:= BESTOBJ:=.cmo BESTLIB:=.cma BESTDYN:=.cma - -# needed while booting if non -local -CAML_LD_LIBRARY_PATH := $(PWD)/kernel/byterun:$(CAML_LD_LIBRARY_PATH) -export CAML_LD_LIBRARY_PATH endif define bestobj diff --git a/Makefile.ci b/Makefile.ci index d4383fd409..1a5e8166a2 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -76,6 +76,8 @@ ci-quickchick: ci-ext-lib ci-simple-io ci-metacoq: ci-equations +ci-vst: ci-flocq + # Generic rule, we use make to ease CI integration $(CI_TARGETS): ci-%: +./dev/ci/ci-wrapper.sh $* diff --git a/checker/check.mllib b/checker/check.mllib index d47a93c70d..a16a871dc3 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -1,5 +1,6 @@ Analyze +CheckFlags CheckInductive Mod_checking CheckTypes diff --git a/checker/checkFlags.ml b/checker/checkFlags.ml new file mode 100644 index 0000000000..1f5e76bd83 --- /dev/null +++ b/checker/checkFlags.ml @@ -0,0 +1,23 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Declarations + +let set_local_flags flags env = + let flags = + { (Environ.typing_flags env) with + check_guarded = flags.check_guarded; + check_positive = flags.check_positive; + check_universes = flags.check_universes; + conv_oracle = flags.conv_oracle; + cumulative_sprop = flags.cumulative_sprop; + } + in + Environ.set_typing_flags flags env diff --git a/checker/checkFlags.mli b/checker/checkFlags.mli new file mode 100644 index 0000000000..2e41e656f1 --- /dev/null +++ b/checker/checkFlags.mli @@ -0,0 +1,12 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +val set_local_flags : Declarations.typing_flags -> Environ.env -> Environ.env +(** Set flags except for those ignored by the checker (eg vm_compute). *) diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index a1d5aedb01..c370a77ea0 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -164,16 +164,7 @@ let check_inductive env mind mb = mind_private; mind_typing_flags; } = (* Locally set typing flags for further typechecking *) - let mb_flags = mb.mind_typing_flags in - let env = Environ.set_typing_flags - {env.env_typing_flags with - check_guarded = mb_flags.check_guarded; - check_positive = mb_flags.check_positive; - check_universes = mb_flags.check_universes; - conv_oracle = mb_flags.conv_oracle; - } - env - in + let env = CheckFlags.set_local_flags mb.mind_typing_flags env in Indtypes.check_inductive env ~sec_univs:None mind entry in let check = check mind in diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 44b7089fd0..8fd81d43be 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -17,14 +17,7 @@ let set_indirect_accessor f = indirect_accessor := f let check_constant_declaration env kn cb = Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ Constant.print kn); - let cb_flags = cb.const_typing_flags in - let env = Environ.set_typing_flags - {env.env_typing_flags with - check_guarded = cb_flags.check_guarded; - check_universes = cb_flags.check_universes; - conv_oracle = cb_flags.conv_oracle;} - env - in + let env = CheckFlags.set_local_flags cb.const_typing_flags env in let poly, env = match cb.const_universes with | Monomorphic ctx -> diff --git a/checker/values.ml b/checker/values.ml index b9efce6948..9bd381e4a9 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -241,7 +241,10 @@ let v_cst_def = [|[|Opt Int|]; [|v_cstr_subst|]; [|v_opaque|]; [|v_primitive|]|] let v_typing_flags = - v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|] + v_tuple "typing_flags" + [|v_bool; v_bool; v_bool; + v_oracle; v_bool; v_bool; + v_bool; v_bool; v_bool|] let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] diff --git a/configure.ml b/configure.ml index eaa0e321b0..282b40db27 100644 --- a/configure.ml +++ b/configure.ml @@ -983,7 +983,7 @@ let config_runtime () = ["-dllib";"-lcoqrun";"-dllpath";("\"" ^ coqtop ^ "/kernel/byterun\"")] | _ -> let ld="CAML_LD_LIBRARY_PATH" in - build_loadpath := sprintf "export %s:='%s/kernel/byterun':$(%s)" ld coqtop ld; + build_loadpath := sprintf "export %s:=%s/kernel/byterun:$(%s)" ld coqtop ld; ["-dllib";"-lcoqrun";"-dllpath";coqlib/"kernel/byterun"] let vmbyteflags = config_runtime () diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh index e9f8324f28..7a9531216e 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")" git_download Flocq -( cd "${CI_BUILD_DIR}/Flocq" && autoconf && ./configure && ./remake "-j${NJOBS}" ) +( cd "${CI_BUILD_DIR}/Flocq" && autoconf && ./configure && ./remake "-j${NJOBS}" && ./remake install ) diff --git a/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh b/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh new file mode 100644 index 0000000000..cd6b408813 --- /dev/null +++ b/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh @@ -0,0 +1,24 @@ +if [ "$CI_PULL_REQUEST" = "11896" ] || [ "$CI_BRANCH" = "evar-inst-list" ]; then + + coqhammer_CI_REF="evar-inst-list" + coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer + + elpi_CI_REF="evar-inst-list" + elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi + + equations_CI_REF="evar-inst-list" + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + + metacoq_CI_REF="evar-inst-list" + metacoq_CI_GITURL=https://github.com/ppedrot/metacoq + + mtac2_CI_REF="evar-inst-list" + mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 + + quickchick_CI_REF="evar-inst-list" + quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick + + unicoq_CI_REF="evar-inst-list" + unicoq_CI_GITURL=https://github.com/ppedrot/unicoq + +fi diff --git a/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh b/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh new file mode 100644 index 0000000000..6bee3c7bb6 --- /dev/null +++ b/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh @@ -0,0 +1,15 @@ +if [ "$CI_PULL_REQUEST" = "12023" ] || [ "$CI_BRANCH" = "master+fixing-empty-Ltac-v-file" ]; then + + fiat_crypto_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file + fiat_crypto_CI_GITURL=https://github.com/herbelin/fiat-crypto + + mtac2_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file + mtac2_CI_GITURL=https://github.com/herbelin/Mtac2 + + metacoq_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file + metacoq_CI_GITURL=https://github.com/herbelin/template-coq + + unimath_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file + unimath_CI_GITURL=https://github.com/herbelin/UniMath + +fi diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 542893ad0b..00050a89e1 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -287,7 +287,7 @@ let constr_display csr = "LetIn("^(name_display na)^","^(term_display b)^"," ^(term_display t)^","^(term_display c)^")" | App (c,l) -> "App("^(term_display c)^","^(array_display l)^")\n" - | Evar (e,l) -> "Evar("^(Pp.string_of_ppcmds (Evar.print e))^","^(array_display l)^")" + | Evar (e,l) -> "Evar("^(Pp.string_of_ppcmds (Evar.print e))^","^(array_display (Array.of_list l))^")" | Const (c,u) -> "Const("^(Constant.to_string c)^","^(universes_display u)^")" | Ind ((sp,i),u) -> "MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^","^(universes_display u)^")" @@ -383,7 +383,7 @@ let print_pure_constr csr = Array.iter (fun x -> print_space (); box_display x) l; print_string ")" | Evar (e,l) -> print_string "Evar#"; print_int (Evar.repr e); print_string "{"; - Array.iter (fun x -> print_space (); box_display x) l; + List.iter (fun x -> print_space (); box_display x) l; print_string"}" | Const (c,u) -> print_string "Cons("; sp_con_display c; diff --git a/doc/changelog/04-tactics/11883-fix-autounfold.rst b/doc/changelog/04-tactics/11883-fix-autounfold.rst new file mode 100644 index 0000000000..83ff177380 --- /dev/null +++ b/doc/changelog/04-tactics/11883-fix-autounfold.rst @@ -0,0 +1,13 @@ +- **Fixed:** + The behavior of :tacn:`autounfold` no longer depends on the names of terms and modules + (`#11883 <https://github.com/coq/coq/pull/11883>`_, + fixes `#7812 <https://github.com/coq/coq/issues/7812>`_, + by Attila Gáspár). +- **Changed:** + `at` clauses can no longer be used with :tacn:`autounfold`. Since they had no effect, it is safe to remove them + (`#11883 <https://github.com/coq/coq/pull/11883>`_, + by Attila Gáspár). +- **Changed:** + :tacn:`autounfold` no longer fails when the :cmd:`Opaque` command is used on constants in the hint databases + (`#11883 <https://github.com/coq/coq/pull/11883>`_, + by Attila Gáspár). diff --git a/doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst b/doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst new file mode 100644 index 0000000000..f10208e9b2 --- /dev/null +++ b/doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst @@ -0,0 +1,6 @@ +- **Changed:** + Tactics with qualified name of the form ``Coq.Init.Notations`` are + now qualified with prefix ``Coq.Init.Ltac``; users of the -noinit + option should now import Coq.Init.Ltac if they want to use Ltac + (`#12023 <https://github.com/coq/coq/pull/12023>`_, + by Hugo Herbelin; minor source of incompatibilities). diff --git a/doc/changelog/04-tactics/12116-master+fix12045-missing-reduction-in-using-ind-scheme.rst b/doc/changelog/04-tactics/12116-master+fix12045-missing-reduction-in-using-ind-scheme.rst new file mode 100644 index 0000000000..7af2b4d97b --- /dev/null +++ b/doc/changelog/04-tactics/12116-master+fix12045-missing-reduction-in-using-ind-scheme.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Anomaly with induction schemes whose conclusion is not normalized + (`#12116 <https://github.com/coq/coq/pull/12116>`_, + by Hugo Herbelin; fixes + `#12045 <https://github.com/coq/coq/pull/12045>`_) diff --git a/doc/changelog/07-commands-and-options/12034-cumul-sprop.rst b/doc/changelog/07-commands-and-options/12034-cumul-sprop.rst new file mode 100644 index 0000000000..ad7cf44482 --- /dev/null +++ b/doc/changelog/07-commands-and-options/12034-cumul-sprop.rst @@ -0,0 +1,5 @@ +- **Changed:** + Added :flag:`Cumulative StrictProp` to control cumulativity of + |SProp| and deprecated now redundant command line + ``--cumulative-sprop`` (`#12034 + <https://github.com/coq/coq/pull/12034>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/09-coqide/12060-ide-disable-csd.rst b/doc/changelog/09-coqide/12060-ide-disable-csd.rst new file mode 100644 index 0000000000..b61ab26007 --- /dev/null +++ b/doc/changelog/09-coqide/12060-ide-disable-csd.rst @@ -0,0 +1,6 @@ +- **Changed:** + CoqIDE now uses native window frames by default on Windows. + The GTK window frames can be restored by setting the `GTK_CSD` environment variable to `1` + (`#12060 <https://github.com/coq/coq/pull/12060>`_, + fixes `#11080 <https://github.com/coq/coq/issues/11080>`_, + by Attila Gáspár). diff --git a/doc/changelog/10-standard-library/12014-ollibs-vector.rst b/doc/changelog/10-standard-library/12014-ollibs-vector.rst new file mode 100644 index 0000000000..87625dd23b --- /dev/null +++ b/doc/changelog/10-standard-library/12014-ollibs-vector.rst @@ -0,0 +1,10 @@ +- **Added:** + Properties of some operations on vectors: + + - ``nth_order``: ``nth_order_hd``, ``nth_order_tl``, ``nth_order_ext`` + - ``replace``: ``nth_order_replace_eq``, ``nth_order_replace_neq``, ``replace_id``, ``replace_replace_eq``, ``replace_replace_neq`` + - ``map``: ``map_id``, ``map_map``, ``map_ext_in``, ``map_ext`` + - ``Forall`` and ``Forall2``: ``Forall_impl``, ``Forall_forall``, ``Forall_nth_order``, ``Forall2_nth_order`` + + (`#12014 <https://github.com/coq/coq/pull/12014>`_, + by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/12031-ollibs-cpermutation.rst b/doc/changelog/10-standard-library/12031-ollibs-cpermutation.rst new file mode 100644 index 0000000000..95b4cce2f7 --- /dev/null +++ b/doc/changelog/10-standard-library/12031-ollibs-cpermutation.rst @@ -0,0 +1,4 @@ +- **Added:** + Definition and properties of cyclic permutations / circular shifts: ``CPermutation`` + (`#12031 <https://github.com/coq/coq/pull/12031>`_, + by Olivier Laurent). diff --git a/doc/common/styles/html/coqremote/sites/all/themes/coq/coqdoc.css b/doc/common/styles/html/coqremote/sites/all/themes/coq/coqdoc.css deleted file mode 100644 index d23ea8f362..0000000000 --- a/doc/common/styles/html/coqremote/sites/all/themes/coq/coqdoc.css +++ /dev/null @@ -1,329 +0,0 @@ -body { padding: 0px 0px; - margin: 0px 0px; - background-color: white } - -#page { display: block; - padding: 0px; - margin: 0px; - padding-bottom: 10px; } - -#header { display: block; - position: relative; - padding: 0; - margin: 0; - vertical-align: middle; - border-bottom-style: solid; - border-width: thin } - -#header h1 { padding: 0; - margin: 0;} - - -/* Contents */ - -#main{ display: block; - padding: 10px; - font-family: sans-serif; - font-size: 100%; - line-height: 100% } - -#main h1 { line-height: 95% } /* allow for multi-line headers */ - -#main a.idref:visited {color : #416DFF; text-decoration : none; } -#main a.idref:link {color : #416DFF; text-decoration : none; } -#main a.idref:hover {text-decoration : none; } -#main a.idref:active {text-decoration : none; } - -#main a.modref:visited {color : #416DFF; text-decoration : none; } -#main a.modref:link {color : #416DFF; text-decoration : none; } -#main a.modref:hover {text-decoration : none; } -#main a.modref:active {text-decoration : none; } - -#main .keyword { color : #cf1d1d } -#main { color: black } - -.section { background-color: rgb(60%,60%,100%); - padding-top: 13px; - padding-bottom: 13px; - padding-left: 3px; - margin-top: 5px; - margin-bottom: 5px; - font-size : 175% } - -h2.section { background-color: rgb(80%,80%,100%); - padding-left: 3px; - padding-top: 12px; - padding-bottom: 10px; - font-size : 130% } - -h3.section { background-color: rgb(90%,90%,100%); - padding-left: 3px; - padding-top: 7px; - padding-bottom: 7px; - font-size : 115% } - -h4.section { -/* - background-color: rgb(80%,80%,80%); - max-width: 20em; - padding-left: 5px; - padding-top: 5px; - padding-bottom: 5px; -*/ - background-color: white; - padding-left: 0px; - padding-top: 0px; - padding-bottom: 0px; - font-size : 100%; - font-weight : bold; - text-decoration : underline; - } - -#main .doc { margin: 0px; - font-family: sans-serif; - font-size: 100%; - line-height: 125%; - max-width: 40em; - color: black; - padding: 10px; - background-color: #90bdff} - -.inlinecode { - display: inline; -/* font-size: 125%; */ - color: #666666; - font-family: monospace } - -.doc .inlinecode { - display: inline; - font-size: 120%; - color: rgb(30%,30%,70%); - font-family: monospace } - -.doc .inlinecode .id { - color: rgb(30%,30%,70%); -} - -.inlinecodenm { - display: inline; - color: #444444; -} - -.doc .code { - display: inline; - font-size: 120%; - color: rgb(30%,30%,70%); - font-family: monospace } - -.comment { - display: inline; - font-family: monospace; - color: rgb(50%,50%,80%); -} - -.code { - display: block; -/* padding-left: 15px; */ - font-size: 110%; - font-family: monospace; - } - -table.infrule { - border: 0px; - margin-left: 50px; - margin-top: 10px; - margin-bottom: 10px; -} - -td.infrule { - font-family: monospace; - text-align: center; -/* color: rgb(35%,35%,70%); */ - padding: 0px; - line-height: 100%; -} - -tr.infrulemiddle hr { - margin: 1px 0 1px 0; -} - -.infrulenamecol { - color: rgb(60%,60%,60%); - font-size: 80%; - padding-left: 1em; - padding-bottom: 0.1em -} - -/* Pied de page */ - -#footer { font-size: 65%; - font-family: sans-serif; } - -/* Identifiers: <span class="id" title="...">) */ - -.id { display: inline; } - -.id[title="constructor"] { - color: rgb(60%,0%,0%); -} - -.id[title="var"] { - color: rgb(40%,0%,40%); -} - -.id[title="variable"] { - color: rgb(40%,0%,40%); -} - -.id[title="definition"] { - color: rgb(0%,40%,0%); -} - -.id[title="abbreviation"] { - color: rgb(0%,40%,0%); -} - -.id[title="lemma"] { - color: rgb(0%,40%,0%); -} - -.id[title="instance"] { - color: rgb(0%,40%,0%); -} - -.id[title="projection"] { - color: rgb(0%,40%,0%); -} - -.id[title="method"] { - color: rgb(0%,40%,0%); -} - -.id[title="inductive"] { - color: rgb(0%,0%,80%); -} - -.id[title="record"] { - color: rgb(0%,0%,80%); -} - -.id[title="class"] { - color: rgb(0%,0%,80%); -} - -.id[title="keyword"] { - color : #cf1d1d; -/* color: black; */ -} - -/* Deprecated rules using the 'type' attribute of <span> (not xhtml valid) */ - -.id[type="constructor"] { - color: rgb(60%,0%,0%); -} - -.id[type="var"] { - color: rgb(40%,0%,40%); -} - -.id[type="variable"] { - color: rgb(40%,0%,40%); -} - -.id[type="definition"] { - color: rgb(0%,40%,0%); -} - -.id[type="abbreviation"] { - color: rgb(0%,40%,0%); -} - -.id[type="lemma"] { - color: rgb(0%,40%,0%); -} - -.id[type="instance"] { - color: rgb(0%,40%,0%); -} - -.id[type="projection"] { - color: rgb(0%,40%,0%); -} - -.id[type="method"] { - color: rgb(0%,40%,0%); -} - -.id[type="inductive"] { - color: rgb(0%,0%,80%); -} - -.id[type="record"] { - color: rgb(0%,0%,80%); -} - -.id[type="class"] { - color: rgb(0%,0%,80%); -} - -.id[type="keyword"] { - color : #cf1d1d; -/* color: black; */ -} - -.inlinecode .id { - color: rgb(0%,0%,0%); -} - - -/* TOC */ - -#toc h2 { - padding: 10px; - background-color: rgb(60%,60%,100%); -} - -#toc li { - padding-bottom: 8px; -} - -/* Index */ - -#index { - margin: 0; - padding: 0; - width: 100%; -} - -#index #frontispiece { - margin: 1em auto; - padding: 1em; - width: 60%; -} - -.booktitle { font-size : 140% } -.authors { font-size : 90%; - line-height: 115%; } -.moreauthors { font-size : 60% } - -#index #entrance { - text-align: center; -} - -#index #entrance .spacer { - margin: 0 30px 0 30px; -} - -#index #footer { - position: absolute; - bottom: 0; -} - -.paragraph { - height: 0.75em; -} - -ul.doclist { - margin-top: 0em; - margin-bottom: 0em; -} diff --git a/doc/common/styles/html/coqremote/sites/all/themes/coq/style.css b/doc/common/styles/html/coqremote/sites/all/themes/coq/style.css deleted file mode 100644 index 32c0b33166..0000000000 --- a/doc/common/styles/html/coqremote/sites/all/themes/coq/style.css +++ /dev/null @@ -1,801 +0,0 @@ -body -{ - background: white; - color:#444; - font:normal normal normal small/1.5em "Lucida Grande", Verdana, sans-serif; - margin:0; - padding:0; -} - -h2 -{ - font-size:150%; - font-weight:normal; - margin:20px 0 0; -} - -h3 -{ - font-size:130%; - font-weight:normal; -} - -a:link,a:visited -{ - color:#660403; - font-weight:normal; - text-decoration:none; -} - -a:hover -{ - color: red; - text-decoration:none; -} - -#container -{ - margin: 0; - padding: 0; - } - - /*----------header, logo and site name styles----------*/ - #headertop - { - display: block; - /* position:absolute; */ - min-width: 700px; - top: 0; - width: 100%; - height:30px; - z-index: 1; - background: transparent url('images/header_top.png') repeat-x; - } - - #header - { - min-width: 700px; - width: 100%; height:70px; - position: relative; - left: 0; top: 0; - background: transparent url('images/header_bot.png') repeat-x; - } - - #logo - { - float:left; - z-index: 2; - position: absolute; - top: -15px; - left: 0px; - } - - #logo img - { - border:0; - float:left; - } - - #logoWrapper - { - line-height:4em; - } - - #siteName - { - position: relative; - top: 10px; left: 80px; - color:#fff; - float:left; - font-size:350%; - } - - #siteName a - { - color:#fff; - text-decoration:none; - } - - #siteName a:hover - { - color:#ddd; - text-decoration:none; - } - - #siteSlogan - { - color:#eee; - float:left; - font-size:170%; - margin:50px 0 0 10px; - text-transform:lowercase; - white-space:nowrap; - } - - /*----------nav styles -- primary links in header----------*/ - - #nav -{ - position:absolute; right:0; - margin: 0; - padding: 5px; - } - -#nav ul - { - list-style:none outside none; - list-style-image:none; - margin:0; - padding:0; - } - - #nav li - { - display: inline; - margin: 0; padding: 4px; - } - - #nav li a - { - border:medium none; - color:#ccc; - font-weight:normal; - padding-left:10px; - padding-right:10px; - text-decoration:none; - } - - #nav li a:hover - { - background:#7B0505 none repeat; - border:medium none; - border-left:1px solid #ddd; - border-right:1px solid #ddd; - color:#fff; - padding: 6px 9px 5px 9px; - } - - -/************** FOOTER *******************/ - - -#footer -{ - background:transparent url('images/footer.png') repeat-x; - width:100%; - clear:both; - font-size:85%; - text-align:center; - /* position:fixed; */ - margin: 0; - padding: 0; -} - - -#nav-footer -{ - display: inline; - color:#444; - margin: 0; - padding: 0; - text-align:right; - } - -#nav-footer ul - { - list-style:none outside none; - list-style-image:none; - margin:0; - padding:0px; padding-right: 5px; - } - -#nav-footer li -{ - display:inline; padding: 4px; -} - - #nav-footer li a - { - border:medium none; - color:#ccc; - font-size: 11px; - font-weight:normal; - padding-left: 10px; - padding-right: 10px; - text-decoration:none; - } - - #nav-footer li a:hover - { - background:#7B0505 none repeat; - border:medium none; - border-left:1px solid #ddd; - border-right:1px solid #ddd; - color:#fff; - margin:0; - padding: 3px 9px 0px 9px; - } - - - /*----------main content----------*/ - #content - { - display: block; - position: static; - -/* min-width: 640px; */ - max-width: 800px; - - margin-left:40px; - margin-right:300px; - padding: 2ex 2ex; - - z-index:1; - } - -.content { - display: block; - position: relative; - - margin: 0; - padding: 0; -} - - /*----------sidebar styles----------*/ - #sidebarWrapper - { - /* background:transparent url('images/sidebar_bottom.jpg') no-repeat scroll left bottom;*/ - display:block; - position:fixed; - /* avant : top: 100px; right:0px*/ - top: 15px; /* 180 */ - right:0px; - left: auto; - - margin-right: 0px; - - /* avant - width: 12%; - min-width:80px; */ - - /* width: 18%; */ - /* min-*/ - width:270px; - - z-index:0; - overflow:hidden; - -/* ajout precedent:*/ -/* min-height:320px; - padding:10px; - background-image:url('http://www.lix.polytechnique.fr/Labo/Denis.Cousineau/data/coq/rttr340bis.png'); - background-repeat : repeat-x ;*/ - -/* last ajout */ - /* min-height:510px; */ /* 360 */ - padding-left:0px; - padding-right:0px; - padding-top:105px; /* 40 */ - padding-bottom:/*105px*/115px; - /* background:transparent url('http://www.lix.polytechnique.fr/Labo/Denis.Cousineau/data/coq/trig6b.png') no-repeat scroll left top; */ - background:transparent url('images/sidebarbot.png') no-repeat scroll right bottom; - - } - -#sidebar { - padding-left: 40px; - padding-top: 105px; - overflow: visible; - background:transparent url('images/sidebartop.png') no-repeat scroll right top; -} - -#sidebar .title -{ - /* avant :border-bottom:1px solid #eee;*/ - /* avant : color:#660403;*/ - color:#2D0102; - font-size:120%; - font-weight:bold; - line-height:19px; - margin:10px 0; -} - -/*----------page styles----------*/ -.pageTitle -{ - color:#2D0102; - font-size:220%; - margin:10px 0 20px; -} - -.mission -{ - background-color:#efefef; - border:solid 1px #ccc; - margin:0 0 10px 0; - padding:10px; -} - -.messages -{ - color:#C80000; - font-size:110%; - margin:10px 0; -} - -/*----------node styles----------*/ -.nodeTitle -{ - background: url('images/nodeTitle.gif') no-repeat 0 100%; - color:#9a0000; - font-size: 100%; - margin:0; -} - -.nodeTitle a -{ - color:#660403; - text-decoration:none; -} - -.nodeTitle a:hover -{ - color:#d00000; - text-decoration:none; -} - -.node -{ - margin:0 0 20px; -} - -.content p -{ - margin:10px 0; -} - -.submitted -{ - color:#a3a3a3; - font-size:70%; -} - -.nodeLinks -{ - font-size:95%; - margin:0; - padding:0; -} - -.taxonomy -{ - background:url('icons/tag_red.png') no-repeat 0 7px; - font-size:80%; - padding:0 0 5px 16px; -} - -/*----------comment styles----------*/ -.commentTitle -{ - Border-bottom:1px solid #ddd; - color:#9a0000; - font-size:130%; - margin:20px 0 0; -} - -.commentTitle a -{ - color:#660403; - text-decoration:none; -} - -.commentTitle a:hover -{ - color:#d00000; - text-decoration:none; -} - -.commentLinks -{ - background:#f7f7f7; - border:1px solid #e1e1e1; - color:#444; - font-size:95%; - margin:20px 0 30px; - padding:4px 0 4px 4px; -} - - -/*----------img styles----------*/ -img -{ - padding:3px; -} - -/*----------icons for links----------*/ -.comment_comments a -{ - background:url('icons/comment.png') no-repeat 0 2px; - padding-bottom:5px; - padding-left:20px; -} - -.node_read_more a -{ - background:url('icons/page_white_go.png') no-repeat; - padding-bottom:5px; - padding-left:20px; -} - -.comment_add a,.comment_reply a -{ - background:url('icons/comment_add.png') no-repeat; - padding-bottom:5px; - padding-left:20px; -} -.comment_delete a -{ - background:url('icons/comment_delete.png') no-repeat; - padding-bottom:5px; - padding-left:20px; -} - -.comment_edit a -{ - background:url('icons/comment_edit.png') no-repeat; - padding-bottom:5px; - padding-left:20px; -} - -/*----------TinyMCE editor----------*/ -body.mceContentBody -{ - background:#fff; - color:#000; - font-size:12px; -} - -body.mceContentBody a:link -{ - color:#ff0000; -} - -/*----------table styles----------*/ -table -{ - margin:1em 0; - width:100%; -} - -thead th -{ - border-bottom:2px solid #AAA; - color:#494949; - font-weight:bold; -} - -td,th -{ - padding:.3em 0 .5em; -} - -tr.even,tr.odd,tbody th -{ - border:solid #D5D6D7; - border-width:1px 0; -} - -tr.even -{ - background:#fff; -} - -td.region,td.module,td.container -{ - background:#D5D6D7; - border-bottom:1px solid #AAA; - border-top:1.5em solid #fff; - color:#455067; - font-weight:bold; -} - -tr:first-child td.region,tr:first-child td.module,tr:first-child td.container -{ - border-top-width:0; -} - -td.menu-disabled,td.menu-disabled a -{ - background-color:#D5C2C2; - color:#000; -} - -/*----------other styles----------*/ - -.block -{ - margin:5px 0 20px; -} - -.thumbnail,.preview -{ - border:1px solid #ccc; -} - -.lstlisting { - display: block; - font-family: monospace; - white-space: pre; - margin: 1em 0; -} -.center { - text-align: center; -} -.centered { - display: block-inline; -} - -/*----------download table------------*/ - -table.downloadtable -{ - width:90%; - margin-left:auto; - margin-right:auto; -} - -table.downloadtable td.downloadheader -{ -padding: 2px 1em; -font-weight: bold; -font-size: 120%; -color: white; -background: transparent url('images/header_bot.png') repeat-x; -/*background-color: #660403; */ -border: solid 2px white; -border-left: none; -} - -table.downloadtable td.downloadcategory -{ -padding: 2px 1em; -background-color: #dfbfbe; -text-indent: 0; -} - -table.downloadtable td.downloadsize -{ -text-indent: 0; -white-space: nowrap; -height: 52px; -} - -table.downloadtable td -{ -padding: 2px 1em; -background-color: #dfbfbe; -border-right: solid white 2px; -} - - -table.downloadtable td.downloadtopline -{ -border-top: solid white 2px; -} - -table.downloadtable td.downloadtoprightline -{ -border-top: solid 2px white; -border-right: solid 2px white; -} - -table.downloadtable td.downloadbottomline -{ -border-bottom: solid 2px white; -border-right: solid 2px white; -} - -table.downloadtable td.downloadbottomrightline -{ -border-bottom: solid 2px white; -border-right: solid 2px white; -} - -table.downloadtable td.downloadrightline -{ -border-right: solid 2px white; -} - -table.downloadtable td.downloadback -{ -background-color: #efe4e4; -} - -table.downloadtable td.downloadbottomback -{ -border-bottom: solid 2px white; -background-color: #efe4e4; -} - - -/*********** Normal text style ************/ - -p { - text-indent:3em; -} - -ul { - margin: 0px; - margin-left:4em; - padding: 0px; - list-style-type:square; -} - -li -{ - text-indent: 0px; - margin: 0px; - padding: 0px; -} - -tt { font-size: 1em; } - -pre { font-size: 1em; } - -/*********** Framework ***********/ -.framework -{ - display: block; - position:relative; - border:solid 1px #660033; - margin: 8ex 1em; /* 8ex 8ex 1em 1em; */ - padding: 0; -} - -.frameworkcontent -{ - position:relative; - left:0px; - - - margin: 0; - padding: .5ex 2em; - - text-indent: 2em; - text-align: justify; -} - - -.frameworklabel -{ - display: inline; - position:relative; - top:-1.3ex; - - margin-left:2ex; - padding-top:.4ex; - padding-bottom:.4ex; - padding-right:1ex; - padding-left:1ex; - - border: none; - background: white; - color: black; - - font-weight: bold; - font-size:115%; -} - -.frameworklinks { - display:block; - position:relative; - top:1.4ex; - - margin-right:2ex; - - text-align:right; - font-size:100% - } - -.frameworklinks ul -{ - display: inline; - padding: 0px 1ex; - - border: none; - background: white; -} - - -.frameworklinks li - { - display:inline; - padding: 1ex 0px; - } - - .frameworklinks li a -{ - border:medium none; - - margin: 0px 1ex; - padding-left:2px; - padding-right:3px; - - font-weight:normal; - text-decoration:none; - - color: #660003; -} - - .frameworklinks li a:hover - { - color: red; - - border: none; - } - -/* General flat lists */ -.flatlist li {display: inline} - -/* For sections in bycat.html */ -.bycatsection dt { - text-indent: 3em -} - -.bycatsection dt a -{ - font-weight: bold; - color:#444; -} - -/* footnote is used in the new contribution form */ -.footnote { - text-indent: 0pt; - font-size: 80%; - color: silver; - text-align: justify -} - -/****************** CoqIDE Screenshots *****************/ - - -.SCpager { - position:relative; - top:5px; - width:630px; - background: transparent url('images/header_bot.png') repeat-x; - padding:4px; -} - -.SCpagercontent { - width:390px; - position:relative; - margin-left:auto; - margin-right:auto; -} - -.SCthumb { - height:45px; - margin-left:2px; - margin-right:2px; -} - -.SCthumbselected { - height:55px; - margin-left:2px; - margin-right:2px; -} - -.SCcontent { - position:relative; - top:5px; - width:638px; - background-color: #dfbfbe; -} - -.SCscreenshot { - position:relative; - height:400px; - width:auto; - margin:15px auto 15px 19px; -} diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst index 9acdd18b89..b2d3687780 100644 --- a/doc/sphinx/addendum/sprop.rst +++ b/doc/sphinx/addendum/sprop.rst @@ -240,3 +240,10 @@ so correctly converts ``x`` and ``y``. the kernel when it is passed a term with incorrect relevance marks. To avoid conversion issues as in ``late_mark`` you may wish to use it to find when your tactics are producing incorrect marks. + +.. flag:: Cumulative StrictProp + :name: Cumulative StrictProp + + Set this flag (it is off by default) to make the kernel accept + cumulativity between |SProp| and other universes. This makes + typechecking incomplete. diff --git a/doc/sphinx/coqdoc.css b/doc/sphinx/coqdoc.css deleted file mode 100644 index a325a33842..0000000000 --- a/doc/sphinx/coqdoc.css +++ /dev/null @@ -1,338 +0,0 @@ -/************************************************************************/ -/* * The Coq Proof Assistant / The Coq Development Team */ -/* v * Copyright INRIA, CNRS and contributors */ -/* <O___,, * (see version control and CREDITS file for authors & dates) */ -/* \VV/ **************************************************************/ -/* // * This file is distributed under the terms of the */ -/* * GNU Lesser General Public License Version 2.1 */ -/* * (see LICENSE file for the text of the license) */ -/************************************************************************/ -body { padding: 0px 0px; - margin: 0px 0px; - background-color: white } - -#page { display: block; - padding: 0px; - margin: 0px; - padding-bottom: 10px; } - -#header { display: block; - position: relative; - padding: 0; - margin: 0; - vertical-align: middle; - border-bottom-style: solid; - border-width: thin } - -#header h1 { padding: 0; - margin: 0;} - - -/* Contents */ - -#main{ display: block; - padding: 10px; - font-family: sans-serif; - font-size: 100%; - line-height: 100% } - -#main h1 { line-height: 95% } /* allow for multi-line headers */ - -#main a.idref:visited {color : #416DFF; text-decoration : none; } -#main a.idref:link {color : #416DFF; text-decoration : none; } -#main a.idref:hover {text-decoration : none; } -#main a.idref:active {text-decoration : none; } - -#main a.modref:visited {color : #416DFF; text-decoration : none; } -#main a.modref:link {color : #416DFF; text-decoration : none; } -#main a.modref:hover {text-decoration : none; } -#main a.modref:active {text-decoration : none; } - -#main .keyword { color : #cf1d1d } -#main { color: black } - -.section { background-color: rgb(60%,60%,100%); - padding-top: 13px; - padding-bottom: 13px; - padding-left: 3px; - margin-top: 5px; - margin-bottom: 5px; - font-size : 175% } - -h2.section { background-color: rgb(80%,80%,100%); - padding-left: 3px; - padding-top: 12px; - padding-bottom: 10px; - font-size : 130% } - -h3.section { background-color: rgb(90%,90%,100%); - padding-left: 3px; - padding-top: 7px; - padding-bottom: 7px; - font-size : 115% } - -h4.section { -/* - background-color: rgb(80%,80%,80%); - max-width: 20em; - padding-left: 5px; - padding-top: 5px; - padding-bottom: 5px; -*/ - background-color: white; - padding-left: 0px; - padding-top: 0px; - padding-bottom: 0px; - font-size : 100%; - font-weight : bold; - text-decoration : underline; - } - -#main .doc { margin: 0px; - font-family: sans-serif; - font-size: 100%; - line-height: 125%; - max-width: 40em; - color: black; - padding: 10px; - background-color: #90bdff } - -.inlinecode { - display: inline; -/* font-size: 125%; */ - color: #666666; - font-family: monospace } - -.doc .inlinecode { - display: inline; - font-size: 120%; - color: rgb(30%,30%,70%); - font-family: monospace } - -.doc .inlinecode .id { - color: rgb(30%,30%,70%); -} - -.inlinecodenm { - display: inline; - color: #444444; -} - -.doc .code { - display: inline; - font-size: 120%; - color: rgb(30%,30%,70%); - font-family: monospace } - -.comment { - display: inline; - font-family: monospace; - color: rgb(50%,50%,80%); -} - -.code { - display: block; -/* padding-left: 15px; */ - font-size: 110%; - font-family: monospace; - } - -table.infrule { - border: 0px; - margin-left: 50px; - margin-top: 10px; - margin-bottom: 10px; -} - -td.infrule { - font-family: monospace; - text-align: center; -/* color: rgb(35%,35%,70%); */ - padding: 0px; - line-height: 100%; -} - -tr.infrulemiddle hr { - margin: 1px 0 1px 0; -} - -.infrulenamecol { - color: rgb(60%,60%,60%); - font-size: 80%; - padding-left: 1em; - padding-bottom: 0.1em -} - -/* Pied de page */ - -#footer { font-size: 65%; - font-family: sans-serif; } - -/* Identifiers: <span class="id" title="...">) */ - -.id { display: inline; } - -.id[title="constructor"] { - color: rgb(60%,0%,0%); -} - -.id[title="var"] { - color: rgb(40%,0%,40%); -} - -.id[title="variable"] { - color: rgb(40%,0%,40%); -} - -.id[title="definition"] { - color: rgb(0%,40%,0%); -} - -.id[title="abbreviation"] { - color: rgb(0%,40%,0%); -} - -.id[title="lemma"] { - color: rgb(0%,40%,0%); -} - -.id[title="instance"] { - color: rgb(0%,40%,0%); -} - -.id[title="projection"] { - color: rgb(0%,40%,0%); -} - -.id[title="method"] { - color: rgb(0%,40%,0%); -} - -.id[title="inductive"] { - color: rgb(0%,0%,80%); -} - -.id[title="record"] { - color: rgb(0%,0%,80%); -} - -.id[title="class"] { - color: rgb(0%,0%,80%); -} - -.id[title="keyword"] { - color : #cf1d1d; -/* color: black; */ -} - -/* Deprecated rules using the 'type' attribute of <span> (not xhtml valid) */ - -.id[type="constructor"] { - color: rgb(60%,0%,0%); -} - -.id[type="var"] { - color: rgb(40%,0%,40%); -} - -.id[type="variable"] { - color: rgb(40%,0%,40%); -} - -.id[type="definition"] { - color: rgb(0%,40%,0%); -} - -.id[type="abbreviation"] { - color: rgb(0%,40%,0%); -} - -.id[type="lemma"] { - color: rgb(0%,40%,0%); -} - -.id[type="instance"] { - color: rgb(0%,40%,0%); -} - -.id[type="projection"] { - color: rgb(0%,40%,0%); -} - -.id[type="method"] { - color: rgb(0%,40%,0%); -} - -.id[type="inductive"] { - color: rgb(0%,0%,80%); -} - -.id[type="record"] { - color: rgb(0%,0%,80%); -} - -.id[type="class"] { - color: rgb(0%,0%,80%); -} - -.id[type="keyword"] { - color : #cf1d1d; -/* color: black; */ -} - -.inlinecode .id { - color: rgb(0%,0%,0%); -} - - -/* TOC */ - -#toc h2 { - padding: 10px; - background-color: rgb(60%,60%,100%); -} - -#toc li { - padding-bottom: 8px; -} - -/* Index */ - -#index { - margin: 0; - padding: 0; - width: 100%; -} - -#index #frontispiece { - margin: 1em auto; - padding: 1em; - width: 60%; -} - -.booktitle { font-size : 140% } -.authors { font-size : 90%; - line-height: 115%; } -.moreauthors { font-size : 60% } - -#index #entrance { - text-align: center; -} - -#index #entrance .spacer { - margin: 0 30px 0 30px; -} - -#index #footer { - position: absolute; - bottom: 0; -} - -.paragraph { - height: 0.75em; -} - -ul.doclist { - margin-top: 0em; - margin-bottom: 0em; -} diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 7d031b9b7a..60fdbf0a9d 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -91,9 +91,15 @@ capital letter. This command supports the :attr:`local`, :attr:`global` and :attr:`export` attributes. They are described :ref:`here <set_unset_scope_qualifiers>`. - .. warn:: There is no option @setting_name. + .. warn:: There is no flag or option with this name: "@setting_name". - This message also appears for unknown flags. + This warning message can be raised by :cmd:`Set` and + :cmd:`Unset` when :n:`@setting_name` is unknown. It is a + warning rather than an error because this helps library authors + produce Coq code that is compatible with several Coq versions. + To preserve the same behavior, they may need to set some + compatibility flags or options that did not exist in previous + Coq versions. .. cmd:: Unset @setting_name :name: Unset @@ -119,6 +125,20 @@ capital letter. whether the table contains each specified value, otherise this is equivalent to :cmd:`Print Table`. The `for` clause is not valid for flags and options. + .. exn:: There is no flag, option or table with this name: "@setting_name". + + This error message is raised when calling the :cmd:`Test` + command (without the `for` clause), or the :cmd:`Print Table` + command, for an unknown :n:`@setting_name`. + + .. exn:: There is no qualid-valued table with this name: "@setting_name". + There is no string-valued table with this name: "@setting_name". + + These error messages are raised when calling the :cmd:`Add` or + :cmd:`Remove` commands, or the :cmd:`Test` command with the + `for` clause, if :n:`@setting_name` is unknown or does not have + the right type. + .. cmd:: Print Options Prints the current value of all flags and options, and the names of all tables. @@ -1076,6 +1096,8 @@ Controlling Typing Flags Print the status of the three typing flags: guard checking, positivity checking and universe checking. +See also :flag:`Cumulative StrictProp` in the |SProp| chapter. + .. example:: .. coqtop:: all reset diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 7fa621c11c..b2c9c936c9 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -13,6 +13,7 @@ through the <tt>Require Import</tt> command.</p> The core library (automatically loaded when starting Coq) </dt> <dd> + theories/Init/Ltac.v theories/Init/Notations.v theories/Init/Datatypes.v theories/Init/Logic.v @@ -444,6 +445,7 @@ through the <tt>Require Import</tt> command.</p> theories/Sorting/PermutSetoid.v theories/Sorting/Mergesort.v theories/Sorting/Sorted.v + theories/Sorting/CPermutation.v </dd> <dt> <b>Wellfounded</b>: diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 5034d9a3c9..700170b3c6 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -906,14 +906,14 @@ command: [ | DELETE "Unset" option_table | REPLACE "Set" option_table option_setting | WITH OPT "Export" "Set" option_table (* set flag *) -| REPLACE "Test" option_table "for" LIST1 option_ref_value -| WITH "Test" option_table OPT ( "for" LIST1 option_ref_value ) +| REPLACE "Test" option_table "for" LIST1 table_value +| WITH "Test" option_table OPT ( "for" LIST1 table_value ) | DELETE "Test" option_table (* hide the fact that table names are limited to 2 IDENTs *) -| REPLACE "Add" IDENT IDENT LIST1 option_ref_value -| WITH "Add" option_table LIST1 option_ref_value -| DELETE "Add" IDENT LIST1 option_ref_value +| REPLACE "Add" IDENT IDENT LIST1 table_value +| WITH "Add" option_table LIST1 table_value +| DELETE "Add" IDENT LIST1 table_value | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "as" ident | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident @@ -969,9 +969,9 @@ command: [ | DELETE "Preterm" (* hide the fact that table names are limited to 2 IDENTs *) -| REPLACE "Remove" IDENT IDENT LIST1 option_ref_value -| WITH "Remove" option_table LIST1 option_ref_value -| DELETE "Remove" IDENT LIST1 option_ref_value +| REPLACE "Remove" IDENT IDENT LIST1 table_value +| WITH "Remove" option_table LIST1 table_value +| DELETE "Remove" IDENT LIST1 table_value | DELETE "Restore" "State" IDENT | DELETE "Restore" "State" ne_string | "Restore" "State" [ IDENT | ne_string ] @@ -1550,7 +1550,7 @@ SPLICE: [ | constructor_type | record_binder | at_level_opt -| option_ref_value +| table_value | positive_search_mark | in_or_out_modules | option_setting diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 04c20a7203..4274dccb40 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -524,12 +524,12 @@ command: [ | "Set" option_table option_setting | "Unset" option_table | "Print" "Table" option_table -| "Add" IDENT IDENT LIST1 option_ref_value -| "Add" IDENT LIST1 option_ref_value -| "Test" option_table "for" LIST1 option_ref_value +| "Add" IDENT IDENT LIST1 table_value +| "Add" IDENT LIST1 table_value +| "Test" option_table "for" LIST1 table_value | "Test" option_table -| "Remove" IDENT IDENT LIST1 option_ref_value -| "Remove" IDENT LIST1 option_ref_value +| "Remove" IDENT IDENT LIST1 table_value +| "Remove" IDENT LIST1 table_value | "Write" "State" IDENT | "Write" "State" ne_string | "Restore" "State" IDENT @@ -1318,7 +1318,7 @@ option_setting: [ | STRING ] -option_ref_value: [ +table_value: [ | global | STRING ] diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 4508633858..ca681e58f8 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -355,7 +355,7 @@ let iter_with_full_binders sigma g f n c = | Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c | LetIn (na,b,t,c) -> f n b; f n t; f (g (LocalDef (na, b, t)) n) c | App (c,l) -> f n c; Array.Fun1.iter f n l - | Evar (_,l) -> Array.Fun1.iter f n l + | Evar (_,l) -> List.iter (fun c -> f n c) l | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl | Proj (p,c) -> f n c | Fix (_,(lna,tl,bl)) -> @@ -717,7 +717,7 @@ let val_of_named_context e = val_of_named_context (cast_named_context unsafe_eq let named_context_of_val e = cast_named_context (sym unsafe_eq) (named_context_of_val e) let of_existential : Constr.existential -> existential = - let gen : type a b. (a,b) eq -> 'c * b array -> 'c * a array = fun Refl x -> x in + let gen : type a b. (a,b) eq -> 'c * b list -> 'c * a list = fun Refl x -> x in gen unsafe_eq let lookup_rel i e = cast_rel_decl (sym unsafe_eq) (lookup_rel i e) diff --git a/engine/evarutil.ml b/engine/evarutil.ml index fdcdfe11f4..5fcadfcef7 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -200,7 +200,7 @@ let make_pure_subst evi args = match args with | a::rest -> (rest, (NamedDecl.get_id decl, a)::l) | _ -> anomaly (Pp.str "Instance does not match its signature.")) - (evar_filtered_context evi) (Array.rev_to_list args,[])) + (evar_filtered_context evi) (List.rev args,[])) (*------------------------------------* * functional operations on evar sets * @@ -448,7 +448,7 @@ let new_evar_instance ?src ?filter ?abstract_arguments ?candidates ?naming ?type assert (not !Flags.debug || List.distinct (ids_of_named_context (named_context_of_val sign))); let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate ?principal typ in - evd, mkEvar (newevk,Array.of_list instance) + evd, mkEvar (newevk, instance) let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ = let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in @@ -506,7 +506,7 @@ let generalize_evar_over_rels sigma (ev,args) = List.fold_left2 (fun (c,inst as x) a d -> if isRel sigma a then (mkNamedProd_or_LetIn d c,a::inst) else x) - (evi.evar_concl,[]) (Array.to_list args) sign + (evi.evar_concl,[]) args sign (************************************) (* Removing a dependency in an evar *) @@ -594,7 +594,7 @@ let rec check_and_clear_in_constr env evdref err ids global c = (* No dependency at all, we can keep this ev's context hyp *) (ri, true::filter) with Depends id -> (Id.Map.add (NamedDecl.get_id h) id ri, false::filter)) - ctxt (Array.to_list l) (Id.Map.empty,[]) in + ctxt l (Id.Map.empty,[]) in (* Check if some rid to clear in the context of ev has dependencies in the type of ev and adjust the source of the dependency *) let _nconcl = @@ -736,7 +736,7 @@ let undefined_evars_of_term evd t = match EConstr.kind evd c with | Evar (n, l) -> let acc = Evar.Set.add n acc in - Array.fold_left evrec acc l + List.fold_left evrec acc l | _ -> EConstr.fold evd evrec acc c in evrec Evar.Set.empty t diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 1dec63aaf0..b5c7ccb283 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -88,7 +88,7 @@ val new_evar_instance : named_context_val -> evar_map -> types -> constr list -> evar_map * constr -val make_pure_subst : evar_info -> 'a array -> (Id.t * 'a) list +val make_pure_subst : evar_info -> 'a list -> (Id.t * 'a) list val safe_evar_value : evar_map -> Constr.existential -> Constr.constr option diff --git a/engine/evd.ml b/engine/evd.ml index 65fe261ff4..5642145f6d 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -233,32 +233,27 @@ exception NotInstantiatedEvar (* Note: let-in contributes to the instance *) let evar_instance_array test_id info args = - let len = Array.length args in - let rec instrec filter ctxt i = match filter, ctxt with - | [], [] -> - if Int.equal i len then [] - else instance_mismatch () - | false :: filter, _ :: ctxt -> - instrec filter ctxt i - | true :: filter, d :: ctxt -> - if i < len then - let c = Array.unsafe_get args i in - if test_id d c then instrec filter ctxt (succ i) - else (NamedDecl.get_id d, c) :: instrec filter ctxt (succ i) - else instance_mismatch () + let rec instrec filter ctxt args = match filter, ctxt, args with + | [], [], [] -> [] + | false :: filter, _ :: ctxt, args -> + instrec filter ctxt args + | true :: filter, d :: ctxt, c :: args -> + if test_id d c then instrec filter ctxt args + else (NamedDecl.get_id d, c) :: instrec filter ctxt args | _ -> instance_mismatch () in match Filter.repr (evar_filter info) with | None -> - let map i d = - if (i < len) then - let c = Array.unsafe_get args i in - if test_id d c then None else Some (NamedDecl.get_id d, c) - else instance_mismatch () + let rec instance ctxt args = match ctxt, args with + | [], [] -> [] + | d :: ctxt, c :: args -> + if test_id d c then instance ctxt args + else (NamedDecl.get_id d, c) :: instance ctxt args + | _ -> instance_mismatch () in - List.map_filter_i map (evar_context info) + instance (evar_context info) args | Some filter -> - instrec filter (evar_context info) 0 + instrec filter (evar_context info) args let make_evar_instance_array info args = evar_instance_array (NamedDecl.get_id %> isVarId) info args @@ -794,7 +789,7 @@ let restrict evk filter ?candidates ?src evd = | _ -> Evar.Set.add evk evd.last_mods in let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in let ctxt = Filter.filter_list filter (evar_context evar_info) in - let id_inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in + let id_inst = List.map (NamedDecl.get_id %> mkVar) ctxt in let body = mkEvar(evk',id_inst) in let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in let evar_flags = declare_restricted_evar evd.evar_flags evk evk' in @@ -1405,7 +1400,7 @@ let evars_of_term evd c = let rec evrec acc c = let c = MiniEConstr.whd_evar evd c in match kind c with - | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l) + | Evar (n, l) -> Evar.Set.add n (List.fold_left evrec acc l) | _ -> Constr.fold evrec acc c in evrec Evar.Set.empty c @@ -1413,7 +1408,7 @@ let evars_of_term evd c = let evar_nodes_of_term c = let rec evrec acc c = match kind c with - | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l) + | Evar (n, l) -> Evar.Set.add n (List.fold_left evrec acc l) | _ -> Constr.fold evrec acc c in evrec Evar.Set.empty c diff --git a/engine/evd.mli b/engine/evd.mli index bbdb63a467..c6c4a71b22 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -247,9 +247,9 @@ val existential_opt_value : evar_map -> econstr pexistential -> econstr option val existential_opt_value0 : evar_map -> existential -> constr option val evar_instance_array : (Constr.named_declaration -> 'a -> bool) -> evar_info -> - 'a array -> (Id.t * 'a) list + 'a list -> (Id.t * 'a) list -val instantiate_evar_array : evar_info -> econstr -> econstr array -> econstr +val instantiate_evar_array : evar_info -> econstr -> econstr list -> econstr val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool -> evar_map -> evar_map -> evar_map diff --git a/engine/termops.ml b/engine/termops.ml index 16f2a87c1e..6d779e6a35 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -636,8 +636,8 @@ let map_constr_with_binders_left_to_right sigma g f l c = if b' == b then c else mkProj (p, b') | Evar (e,al) -> - let al' = Array.map_left (f l) al in - if Array.for_all2 (==) al' al then c + let al' = List.map_left (f l) al in + if List.for_all2 (==) al' al then c else mkEvar (e, al') | Case (ci,p,b,bl) -> (* In v8 concrete syntax, predicate is after the term to match! *) @@ -707,8 +707,8 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr = let c' = f l c in if c' == c then cstr else mkProj (p, c') | Evar (e,al) -> - let al' = Array.map (f l) al in - if Array.for_all2 (==) al al' then cstr else mkEvar (e, al') + let al' = List.map (f l) al in + if List.for_all2 (==) al al' then cstr else mkEvar (e, al') | Case (ci,p,c,bl) when userview -> let p' = map_return_predicate_with_full_binders sigma g f l ci p in let c' = f l c in diff --git a/engine/uState.ml b/engine/uState.ml index ff85f09efa..abd5f2828f 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -39,7 +39,7 @@ type t = uctx_weak_constraints : UPairSet.t } -let initial_sprop_cumulative = UGraph.make_sprop_cumulative UGraph.initial_universes +let initial_sprop_cumulative = UGraph.set_cumulative_sprop true UGraph.initial_universes let empty = { uctx_names = UNameMap.empty, LMap.empty; @@ -57,11 +57,11 @@ let elaboration_sprop_cumul = ~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true let make ~lbound u = - let u = if elaboration_sprop_cumul () then UGraph.make_sprop_cumulative u else u in - { empty with - uctx_universes = u; - uctx_universes_lbound = lbound; - uctx_initial_universes = u} + let u = UGraph.set_cumulative_sprop (elaboration_sprop_cumul ()) u in + { empty with + uctx_universes = u; + uctx_universes_lbound = lbound; + uctx_initial_universes = u} let is_empty ctx = ContextSet.is_empty ctx.uctx_local && @@ -547,10 +547,11 @@ let emit_side_effects eff u = merge_seff u uctx let update_sigma_env uctx env = - let univs = UGraph.make_sprop_cumulative (Environ.universes env) in + let univs = UGraph.set_cumulative_sprop (elaboration_sprop_cumul()) (Environ.universes env) in let eunivs = - { uctx with uctx_initial_universes = univs; - uctx_universes = univs } + { uctx with + uctx_initial_universes = univs; + uctx_universes = univs } in merge_seff eunivs eunivs.uctx_local diff --git a/engine/univSubst.ml b/engine/univSubst.ml index 6000650ad9..a691239ee2 100644 --- a/engine/univSubst.ml +++ b/engine/univSubst.ml @@ -131,7 +131,7 @@ let nf_evars_and_universes_opt_subst f subst = let rec aux c = match kind c with | Evar (evk, args) -> - let args = Array.map aux args in + let args = List.map aux args in (match try f (evk, args) with Not_found -> None with | None -> mkEvar (evk, args) | Some c -> aux c) diff --git a/ide/coqide_WIN32.ml.in b/ide/coqide_WIN32.ml.in index 2d3964f210..be8aab9e49 100644 --- a/ide/coqide_WIN32.ml.in +++ b/ide/coqide_WIN32.ml.in @@ -44,6 +44,7 @@ let () = Coq.gio_channel_of_descr_socket := Glib.Io.channel_of_descr_socket; set_win32_path (); Coq.interrupter := win32_interrupt; - reroute_stdout_stderr () + reroute_stdout_stderr (); + try ignore (Unix.getenv "GTK_CSD") with Not_found -> Unix.putenv "GTK_CSD" "0" let init () = () diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 7a14ca3e48..a37bac3275 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -282,9 +282,9 @@ let insert_pat_alias ?loc p = function | Anonymous -> p | Name _ as na -> CAst.make ?loc @@ CPatAlias (p,(CAst.make ?loc na)) -let rec insert_coercion ?loc l c = match l with +let rec insert_entry_coercion ?loc l c = match l with | [] -> c - | (inscope,ntn)::l -> CAst.make ?loc @@ CNotation (Some inscope,ntn,([insert_coercion ?loc l c],[],[],[])) + | (inscope,ntn)::l -> CAst.make ?loc @@ CNotation (Some inscope,ntn,([insert_entry_coercion ?loc l c],[],[],[])) let rec insert_pat_coercion ?loc l c = match l with | [] -> c @@ -453,7 +453,8 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = with No_match -> let loc = pat.CAst.loc in match DAst.get pat with - | PatVar (Name id) when entry_has_ident custom -> CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id))) + | PatVar (Name id) when entry_has_global custom || entry_has_ident custom -> + CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id))) | pat -> match availability_of_entry_coercion custom InConstrEntrySomeLevel with | None -> raise No_match @@ -615,6 +616,10 @@ let is_projection nargs r = let is_hole = function CHole _ | CEvar _ -> true | _ -> false +let isCRef_no_univ = function + | CRef (_,None) -> true + | _ -> false + let is_significant_implicit a = not (is_hole (a.CAst.v)) @@ -849,7 +854,7 @@ let extern_possible_prim_token (custom,scopes) r = | Some coercion -> match availability_of_prim_token n sc scopes with | None -> raise No_match - | Some key -> insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key) + | Some key -> insert_entry_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key) let filter_enough_applied nargs l = match nargs with @@ -931,7 +936,8 @@ let rec extern inctx ?impargs scopes vars r = match DAst.get r with | GRef (ref,us) when entry_has_global (fst scopes) -> CAst.make ?loc (extern_ref vars ref us) - | GVar id when entry_has_ident (fst scopes) -> CAst.make ?loc (extern_var ?loc id) + | GVar id when entry_has_global (fst scopes) || entry_has_ident (fst scopes) -> + CAst.make ?loc (extern_var ?loc id) | c -> @@ -1081,7 +1087,7 @@ let rec extern inctx ?impargs scopes vars r = | GFloat f -> extern_float f (snd scopes) - in insert_coercion coercion (CAst.make ?loc c) + in insert_entry_coercion coercion (CAst.make ?loc c) and extern_typ ?impargs (subentry,(_,scopes)) = extern true ?impargs (subentry,(Notation.current_type_scope_name (),scopes)) @@ -1279,14 +1285,11 @@ and extern_notation (custom,scopes as allscopes) vars t rules = pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl)) binderlists in let c = make_notation loc specific_ntn (l,ll,bl,bll) in - let c = insert_coercion coercion (insert_delimiters c key) in + let c = insert_entry_coercion coercion (insert_delimiters c key) in let args = fill_arg_scopes args argsscopes allscopes in let args = extern_args (extern true) vars args in CAst.make ?loc @@ extern_applied_notation nallargs argsimpls c args) | SynDefRule kn -> - match availability_of_entry_coercion custom InConstrEntrySomeLevel with - | None -> raise No_match - | Some coercion -> let l = List.map (fun (c,(subentry,(scopt,scl))) -> extern true (subentry,(scopt,scl@snd scopes)) vars c) @@ -1296,7 +1299,10 @@ and extern_notation (custom,scopes as allscopes) vars t rules = let args = fill_arg_scopes args argsscopes allscopes in let args = extern_args (extern true) vars args in let c = CAst.make ?loc @@ extern_applied_syntactic_definition nallargs argsimpls (a,cf) l args in - insert_coercion coercion c + if isCRef_no_univ c.CAst.v && entry_has_global custom then c + else match availability_of_entry_coercion custom InConstrEntrySomeLevel with + | None -> raise No_match + | Some coercion -> insert_entry_coercion coercion c with No_match -> extern_notation allscopes vars t rules diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index c31cdae6f5..de02882370 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -613,7 +613,7 @@ let rec to_constr lfts v = subst_constr subs f) | FEvar ((ev,args),env) -> let subs = comp_subs lfts env in - mkEvar(ev,Array.map (fun a -> subst_constr subs a) args) + mkEvar(ev,List.map (fun a -> subst_constr subs a) args) | FLIFT (k,a) -> to_constr (el_shft k lfts) a | FInt i -> @@ -1408,7 +1408,7 @@ and norm_head info tab m = Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in mkFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds)) | FEvar((i,args),env) -> - mkEvar(i, Array.map (fun a -> kl info tab (mk_clos env a)) args) + mkEvar(i, List.map (fun a -> kl info tab (mk_clos env a)) args) | FProj (p,c) -> mkProj (p, kl info tab c) | FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FConstruct _ diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 8c7aa6b17a..65de52c0f6 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -670,7 +670,7 @@ let rec lambda_of_constr env c = match Constr.kind c with | Meta _ -> raise (Invalid_argument "Cbytegen.lambda_of_constr: Meta") | Evar (evk, args) -> - let args = lambda_of_args env 0 args in + let args = Array.map_of_list (fun c -> lambda_of_constr env c) args in Levar (evk, args) | Cast (c, _, _) -> lambda_of_constr env c @@ -799,9 +799,6 @@ and lambda_of_args env start args = (fun i -> lambda_of_constr env args.(start + i)) else empty_args - - - (*********************************) let dump_lambda = ref false diff --git a/kernel/constr.ml b/kernel/constr.ml index ade03fdf93..703e3616a0 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -71,7 +71,7 @@ type case_info = (* [constr array] is an instance matching definitional [named_context] in the same order (i.e. last argument first) *) -type 'constr pexistential = existential_key * 'constr array +type 'constr pexistential = existential_key * 'constr list type ('constr, 'types) prec_declaration = Name.t binder_annot array * 'types array * 'constr array type ('constr, 'types) pfixpoint = @@ -110,7 +110,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = type t = (t, t, Sorts.t, Instance.t) kind_of_term type constr = t -type existential = existential_key * constr array +type existential = existential_key * constr list type types = constr @@ -470,7 +470,7 @@ let fold f acc c = match kind c with | LetIn (_,b,t,c) -> f (f (f acc b) t) c | App (c,l) -> Array.fold_left f (f acc c) l | Proj (_p,c) -> f acc c - | Evar (_,l) -> Array.fold_left f acc l + | Evar (_,l) -> List.fold_left f acc l | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl | Fix (_,(_lna,tl,bl)) -> Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl @@ -490,7 +490,7 @@ let iter f c = match kind c with | LetIn (_,b,t,c) -> f b; f t; f c | App (c,l) -> f c; Array.iter f l | Proj (_p,c) -> f c - | Evar (_,l) -> Array.iter f l + | Evar (_,l) -> List.iter f l | Case (_,p,c,bl) -> f p; f c; Array.iter f bl | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl @@ -509,7 +509,7 @@ let iter_with_binders g f n c = match kind c with | Lambda (_,t,c) -> f n t; f (g n) c | LetIn (_,b,t,c) -> f n b; f n t; f (g n) c | App (c,l) -> f n c; Array.Fun1.iter f n l - | Evar (_,l) -> Array.Fun1.iter f n l + | Evar (_,l) -> List.iter (fun c -> f n c) l | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl | Proj (_p,c) -> f n c | Fix (_,(_,tl,bl)) -> @@ -536,7 +536,7 @@ let fold_constr_with_binders g f n acc c = | LetIn (_na,b,t,c) -> f (g n) (f n (f n acc b) t) c | App (c,l) -> Array.fold_left (f n) (f n acc c) l | Proj (_p,c) -> f n acc c - | Evar (_,l) -> Array.fold_left (f n) acc l + | Evar (_,l) -> List.fold_left (f n) acc l | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl | Fix (_,(_,tl,bl)) -> let n' = iterate g (Array.length tl) n in @@ -657,7 +657,7 @@ let map_gen userview f c = match kind c with if t' == t then c else mkProj (p, t') | Evar (e,l) -> - let l' = Array.Smart.map f l in + let l' = List.Smart.map f l in if l'==l then c else mkEvar (e, l') | Case (ci,p,b,bl) when userview -> @@ -722,7 +722,8 @@ let fold_map f accu c = match kind c with if t' == t then accu, c else accu, mkProj (p, t') | Evar (e,l) -> - let accu, l' = Array.Smart.fold_left_map f accu l in + (* Doesn't matter, we should not hashcons evars anyways *) + let accu, l' = List.fold_left_map f accu l in if l'==l then accu, c else accu, mkEvar (e, l') | Case (ci,p,b,bl) -> @@ -782,7 +783,7 @@ let map_with_binders g f l c0 = match kind c0 with if t' == t then c0 else mkProj (p, t') | Evar (e, al) -> - let al' = Array.Fun1.Smart.map f l al in + let al' = List.Smart.map (fun c -> f l c) al in if al' == al then c0 else mkEvar (e, al') | Case (ci, p, c, bl) -> @@ -834,7 +835,7 @@ let fold_with_full_binders g f n acc c = | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c | App (c,l) -> Array.fold_left (f n) (f n acc c) l | Proj (_,c) -> f n acc c - | Evar (_,l) -> Array.fold_left (f n) acc l + | Evar (_,l) -> List.fold_left (f n) acc l | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl | Fix (_,(lna,tl,bl)) -> let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in @@ -880,7 +881,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t Int.equal len (Array.length l2) && leq (nargs+len) c1 c2 && Array.equal_norefl (eq 0) l1 l2 | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq 0 c1 c2 - | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal (eq 0) l1 l2 + | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && List.equal (eq 0) l1 l2 | Const (c1,u1), Const (c2,u2) -> (* The args length currently isn't used but may as well pass it. *) Constant.equal c1 c2 && leq_universes (GlobRef.ConstRef c1) nargs u1 u2 @@ -1039,7 +1040,7 @@ let constr_ord_int f t1 t2 = | Meta m1, Meta m2 -> Int.compare m1 m2 | Meta _, _ -> -1 | _, Meta _ -> 1 | Evar (e1,l1), Evar (e2,l2) -> - (Evar.compare =? (Array.compare f)) e1 e2 l1 l2 + (Evar.compare =? (List.compare f)) e1 e2 l1 l2 | Evar _, _ -> -1 | _, Evar _ -> 1 | Sort s1, Sort s2 -> Sorts.compare s1 s2 | Sort _, _ -> -1 | _, Sort _ -> 1 @@ -1141,7 +1142,7 @@ let hasheq t1 t2 = n1 == n2 && b1 == b2 && t1 == t2 && c1 == c2 | App (c1,l1), App (c2,l2) -> c1 == c2 && array_eqeq l1 l2 | Proj (p1,c1), Proj(p2,c2) -> p1 == p2 && c1 == c2 - | Evar (e1,l1), Evar (e2,l2) -> e1 == e2 && array_eqeq l1 l2 + | Evar (e1,l1), Evar (e2,l2) -> e1 == e2 && List.equal (==) l1 l2 | Const (c1,u1), Const (c2,u2) -> c1 == c2 && u1 == u2 | Ind (ind1,u1), Ind (ind2,u2) -> ind1 == ind2 && u1 == u2 | Construct (cstr1,u1), Construct (cstr2,u2) -> cstr1 == cstr2 && u1 == u2 @@ -1221,7 +1222,7 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = let l, hl = hash_term_array l in (App (c,l), combinesmall 7 (combine hl hc)) | Evar (e,l) -> - let l, hl = hash_term_array l in + let l, hl = hash_list_array l in (Evar (e,l), combinesmall 8 (combine (Evar.hash e) hl)) | Const (c,u) -> let c' = sh_con c in @@ -1289,6 +1290,14 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = let h = !accu land 0x3FFFFFFF in (HashsetTermArray.repr h t term_array_table, h) + and hash_list_array l = + let fold accu c = + let c, h = sh_rec c in + (combine accu h, c) + in + let h, l = List.fold_left_map fold 0 l in + (l, h land 0x3FFFFFFF) + in (* Make sure our statically allocated Rels (1 to 16) are considered as canonical, and hence hash-consed to themselves *) @@ -1316,7 +1325,7 @@ let rec hash t = | App (c,l) -> combinesmall 7 (combine (hash_term_array l) (hash c)) | Evar (e,l) -> - combinesmall 8 (combine (Evar.hash e) (hash_term_array l)) + combinesmall 8 (combine (Evar.hash e) (hash_term_list l)) | Const (c,u) -> combinesmall 9 (combine (Constant.hash c) (Instance.hash u)) | Ind (ind,u) -> @@ -1339,6 +1348,9 @@ let rec hash t = and hash_term_array t = Array.fold_left (fun acc t -> combine acc (hash t)) 0 t +and hash_term_list t = + List.fold_left (fun acc t -> combine (hash t) acc) 0 t + module CaseinfoHash = struct type t = case_info @@ -1458,7 +1470,7 @@ let rec debug_print c = prlist_with_sep spc debug_print (Array.to_list l) ++ str")") | Evar (e,l) -> hov 1 (str"Evar#" ++ int (Evar.repr e) ++ str"{" ++ - prlist_with_sep spc debug_print (Array.to_list l) ++str"}") + prlist_with_sep spc debug_print l ++str"}") | Const (c,u) -> str"Cst(" ++ pr_puniverses (Constant.debug_print c) u ++ str")" | Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i) u ++ str")" | Construct (((sp,i),j),u) -> diff --git a/kernel/constr.mli b/kernel/constr.mli index 16919b705a..00051d7551 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -83,7 +83,7 @@ val mkFloat : Float64.t -> constr val mkMeta : metavariable -> constr (** Constructs an existential variable *) -type existential = Evar.t * constr array +type existential = Evar.t * constr list val mkEvar : existential -> constr (** Construct a sort *) @@ -203,9 +203,9 @@ val mkCoFix : cofixpoint -> constr (** {6 Concrete type for making pattern-matching. } *) -(** [constr array] is an instance matching definitional [named_context] in +(** [constr list] is an instance matching definitional [named_context] in the same order (i.e. last argument first) *) -type 'constr pexistential = Evar.t * 'constr array +type 'constr pexistential = Evar.t * 'constr list type ('constr, 'types, 'sort, 'univs) kind_of_term = | Rel of int (** Gallina-variable introduced by [forall], [fun], [let-in], [fix], or [cofix]. *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 244cd2865d..11d4120d7c 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -92,6 +92,8 @@ type typing_flags = { indices_matter: bool; (** The universe of an inductive type must be above that of its indices. *) + cumulative_sprop : bool; + (** SProp <= Type *) } (* some contraints are in constant_constraints, some other may be in diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 20dc21900c..b347152c16 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -26,6 +26,7 @@ let safe_flags oracle = { enable_VM = true; enable_native_compiler = true; indices_matter = true; + cumulative_sprop = false; } (** {6 Arities } *) diff --git a/kernel/environ.ml b/kernel/environ.ml index de8692ff21..cf01711fe7 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -431,7 +431,7 @@ let push_subgraph (levels,csts) env = in map_universes add_subgraph env -let set_engagement c env = (* Unsafe *) +let set_engagement c env = { env with env_stratification = { env.env_stratification with env_engagement = c } } @@ -445,6 +445,7 @@ let same_flags { share_reduction; enable_VM; enable_native_compiler; + cumulative_sprop; } alt = check_guarded == alt.check_guarded && check_positive == alt.check_positive && @@ -453,14 +454,18 @@ let same_flags { indices_matter == alt.indices_matter && share_reduction == alt.share_reduction && enable_VM == alt.enable_VM && - enable_native_compiler == alt.enable_native_compiler + enable_native_compiler == alt.enable_native_compiler && + cumulative_sprop == alt.cumulative_sprop [@warning "+9"] -let set_typing_flags c env = (* Unsafe *) +let set_cumulative_sprop b = map_universes (UGraph.set_cumulative_sprop b) + +let set_typing_flags c env = if same_flags env.env_typing_flags c then env - else { env with env_typing_flags = c } + else set_cumulative_sprop c.cumulative_sprop { env with env_typing_flags = c } -let make_sprop_cumulative = map_universes UGraph.make_sprop_cumulative +let set_cumulative_sprop b env = + set_typing_flags {env.env_typing_flags with cumulative_sprop=b} env let set_allow_sprop b env = { env with env_stratification = diff --git a/kernel/environ.mli b/kernel/environ.mli index 25ecdfd852..4195f112ca 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -310,7 +310,7 @@ val push_subgraph : Univ.ContextSet.t -> env -> env val set_engagement : engagement -> env -> env val set_typing_flags : typing_flags -> env -> env -val make_sprop_cumulative : env -> env +val set_cumulative_sprop : bool -> env -> env val set_allow_sprop : bool -> env -> env val sprop_allowed : env -> bool diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml index f987164d52..662ad550b8 100644 --- a/kernel/inferCumulativity.ml +++ b/kernel/inferCumulativity.ml @@ -99,7 +99,7 @@ let rec infer_fterm cv_pb infos variances hd stk = end | FEvar ((_,args),e) -> let variances = infer_stack infos variances stk in - infer_vect infos variances (Array.map (mk_clos e) args) + infer_list infos variances (List.map (mk_clos e) args) | FRel _ -> infer_stack infos variances stk | FInt _ -> infer_stack infos variances stk | FFloat _ -> infer_stack infos variances stk @@ -168,6 +168,9 @@ and infer_stack infos variances (stk:CClosure.stack) = and infer_vect infos variances v = Array.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances v +and infer_list infos variances v = + List.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances v + let infer_term cv_pb env variances c = let open CClosure in let infos = (create_clos_infos all env, create_tab ()) in diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index aa513c1536..317141e324 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -405,7 +405,7 @@ let rec map_kn f f' c = if (ct'== ct && l'==l) then c else mkApp (ct',l') | Evar (e,l) -> - let l' = Array.Smart.map func l in + let l' = List.Smart.map func l in if (l'==l) then c else mkEvar (e,l') | Fix (ln,(lna,tl,bl)) -> diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 9ed0f6f411..02ee501f5f 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -474,7 +474,7 @@ let rec lambda_of_constr cache env sigma c = | Evar (evk,args as ev) -> (match evar_value sigma ev with | None -> - let args = Array.map (lambda_of_constr cache env sigma) args in + let args = Array.map_of_list (fun c -> lambda_of_constr cache env sigma c) args in Levar(evk, args) | Some t -> lambda_of_constr cache env sigma t) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 7574d7b21e..4ff90dd70d 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -367,9 +367,9 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let el1 = el_stack lft1 v1 in let el2 = el_stack lft2 v2 in let cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv in - convert_vect l2r infos el1 el2 - (Array.map (mk_clos env1) args1) - (Array.map (mk_clos env2) args2) cuniv + convert_list l2r infos el1 el2 + (List.map (mk_clos env1) args1) + (List.map (mk_clos env2) args2) cuniv else raise NotConvertible (* 2 index known to be bound to no constant *) @@ -702,6 +702,13 @@ and convert_branches l2r infos ci e1 e2 lft1 lft2 br1 br2 cuniv = in Array.fold_right3 fold ci.ci_cstr_nargs br1 br2 cuniv +and convert_list l2r infos lft1 lft2 v1 v2 cuniv = match v1, v2 with +| [], [] -> cuniv +| c1 :: v1, c2 :: v2 -> + let cuniv = ccnv CONV l2r infos lft1 lft2 c1 c2 cuniv in + convert_list l2r infos lft1 lft2 v1 v2 cuniv +| _, _ -> raise NotConvertible + let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 = let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in let infos = create_clos_infos ~evars reds env in diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 58b516dfdd..9fabb441d1 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -243,8 +243,6 @@ let set_native_compiler b senv = let flags = Environ.typing_flags senv.env in set_typing_flags { flags with enable_native_compiler = b } senv -let make_sprop_cumulative senv = { senv with env = Environ.make_sprop_cumulative senv.env } - let set_allow_sprop b senv = { senv with env = Environ.set_allow_sprop b senv.env } (** Check that the engagement [c] expected by a library matches diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index b42746a882..f5bd27ca12 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -135,7 +135,6 @@ val set_check_positive : bool -> safe_transformer0 val set_check_universes : bool -> safe_transformer0 val set_VM : bool -> safe_transformer0 val set_native_compiler : bool -> safe_transformer0 -val make_sprop_cumulative : safe_transformer0 val set_allow_sprop : bool -> safe_transformer0 val check_engagement : Environ.env -> Declarations.set_predicativity -> unit diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 449cd0f0f9..5f5f0ef8cd 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -37,7 +37,7 @@ let g_map f g = if g.graph == g' then g else {g with graph=g'} -let make_sprop_cumulative g = {g with sprop_cumulative=true} +let set_cumulative_sprop b g = {g with sprop_cumulative=b} let check_smaller_expr g (u,n) (v,m) = let diff = n - m in diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index 8a8c09e911..8d9afb0990 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -13,8 +13,8 @@ open Univ (** {6 Graphs of universes. } *) type t -val make_sprop_cumulative : t -> t -(** Don't use this in the kernel, it makes the system incomplete. *) +val set_cumulative_sprop : bool -> t -> t +(** Makes the system incomplete. *) type 'a check_function = t -> 'a -> 'a -> bool diff --git a/library/global.ml b/library/global.ml index abc04a5e14..5c847fda96 100644 --- a/library/global.ml +++ b/library/global.ml @@ -99,7 +99,9 @@ let set_check_guarded c = globalize0 (Safe_typing.set_check_guarded c) let set_check_positive c = globalize0 (Safe_typing.set_check_positive c) let set_check_universes c = globalize0 (Safe_typing.set_check_universes c) let typing_flags () = Environ.typing_flags (env ()) -let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative +let set_cumulative_sprop b = + set_typing_flags {(typing_flags()) with Declarations.cumulative_sprop = b} +let is_cumulative_sprop () = (typing_flags()).Declarations.cumulative_sprop let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b) let sprop_allowed () = Environ.sprop_allowed (env()) let export_private_constants cd = globalize (Safe_typing.export_private_constants cd) diff --git a/library/global.mli b/library/global.mli index e7133a1034..2acd7e2a67 100644 --- a/library/global.mli +++ b/library/global.mli @@ -36,7 +36,8 @@ val set_check_guarded : bool -> unit val set_check_positive : bool -> unit val set_check_universes : bool -> unit val typing_flags : unit -> Declarations.typing_flags -val make_sprop_cumulative : unit -> unit +val set_cumulative_sprop : bool -> unit +val is_cumulative_sprop : unit -> bool val set_allow_sprop : bool -> unit val sprop_allowed : unit -> bool diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 35e131020b..f002bbc57a 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1559,7 +1559,7 @@ let assert_replacing id newt tac = if Id.equal n id then ev' else mkVar n in let (e, _) = destEvar sigma ev in - (sigma, mkEvar (e, Array.map_of_list map nc)) + (sigma, mkEvar (e, List.map map nc)) end end in Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index e0b083a70a..134a9e4b36 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -537,7 +537,7 @@ let pf_abs_evars2 gl rigid (sigma, c0) = let rec put evlist c = match Constr.kind c with | Evar (k, a) -> if List.mem_assoc k evlist || Evd.mem sigma0 k || List.mem k rigid then evlist else - let n = max 0 (Array.length a - nenv) in + let n = max 0 (List.length a - nenv) in let t = abs_evar n k in (k, (n, t)) :: put evlist t | _ -> Constr.fold put evlist c in let evlist = put [] c0 in @@ -549,6 +549,7 @@ let pf_abs_evars2 gl rigid (sigma, c0) = | Evar (ev, a) -> let j, n = lookup ev i evlist in if j = 0 then Constr.map (get i) c else if n = 0 then mkRel j else + let a = Array.of_list a in mkApp (mkRel j, Array.init n (fun k -> get i a.(n - 1 - k))) | _ -> Constr.map_with_binders ((+) 1) get i c in let rec loop c i = function @@ -598,7 +599,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) = let rec put evlist c = match Constr.kind c with | Evar (k, a) -> if List.mem_assoc k evlist || Evd.mem sigma0 k then evlist else - let n = max 0 (Array.length a - nenv) in + let n = max 0 (List.length a - nenv) in let k_ty = Retyping.get_sort_family_of (pf_env gl) sigma (Evd.evar_concl (Evd.find sigma k)) in @@ -636,6 +637,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) = | Evar (ev, a) -> let j, n = lookup ev i evlist in if j = 0 then Constr.map (get evlist i) c else if n = 0 then mkRel j else + let a = Array.of_list a in mkApp (mkRel j, Array.init n (fun k -> get evlist i a.(n - 1 - k))) | _ -> Constr.map_with_binders ((+) 1) (get evlist) i c in let rec app extra_args i c = match decompose_app c with diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 1c776398e7..d5a781e472 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -263,7 +263,7 @@ let nf_open_term sigma0 ise c = let rec nf c' = match kind c' with | Evar ex -> begin try nf (existential_value0 s ex) with _ -> - let k, a = ex in let a' = Array.map nf a in + let k, a = ex in let a' = List.map nf a in if not (Evd.mem !s' k) then s' := Evd.add !s' k (Evarutil.nf_evar_info s (Evd.find s k)); mkEvar (k, a') @@ -307,7 +307,7 @@ let pf_unify_HO gl t1 t2 = (* This is what the definition of iter_constr should be... *) let iter_constr_LR f c = match kind c with - | Evar (k, a) -> Array.iter f a + | Evar (k, a) -> List.iter f a | Cast (cc, _, t) -> f cc; f t | Prod (_, t, b) | Lambda (_, t, b) -> f t; f b | LetIn (_, v, t, b) -> f v; f t; f b @@ -387,7 +387,7 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = with NotInstantiatedEvar -> if Evd.mem sigma0 k then map put c else let evi = Evd.find !sigma k in - let dc = List.firstn (max 0 (Array.length a - nenv)) (evar_filtered_context evi) in + let dc = List.firstn (max 0 (List.length a - nenv)) (evar_filtered_context evi) in let abs_dc (d, c) = function | Context.Named.Declaration.LocalDef (x, b, t) -> d, mkNamedLetIn x (put b) (put t) c @@ -601,7 +601,8 @@ let match_upats_HO ~on_instance upats env sigma0 ise c = | KpatFixed | KpatConst -> ise | KpatEvar _ -> let _, pka = destEvar u.up_f and _, ka = destEvar f in - unif_HO_args env ise pka 0 ka + let fold ise pk k = unif_HO env ise (EConstr.of_constr pk) (EConstr.of_constr k) in + List.fold_left2 fold ise pka ka | KpatLet -> let x, v, t, b = destLetIn f in let _, pv, _, pb = destLetIn u.up_f in diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index f816599a17..b39ec37cd1 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -446,7 +446,7 @@ let rec norm_head info env t stack = Some c -> norm_head info env c stack | None -> let e, xs = ev in - let xs' = Array.map (apply_env env) xs in + let xs' = List.map (apply_env env) xs in (VAL(0, mkEvar (e,xs')), stack)) (* non-neutral cases *) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index f85635528d..25aa8915ba 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -404,7 +404,7 @@ let matches_core env sigma allow_bound_rels Array.fold_left2 (fun subst na1 na2 -> add_binders na1 na2 binding_vars subst) subst lna1 lna2 | PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 -> - Array.fold_left2 (sorec ctx env) subst args1 args2 + List.fold_left2 (sorec ctx env) subst args1 args2 | PInt i1, Int i2 when Uint63.equal i1 i2 -> subst | PFloat f1, Float f2 when Float64.equal f1 f2 -> subst | (PRef _ | PVar _ | PRel _ | PApp _ | PProj _ | PLambda _ diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 857918c928..ff278baf9f 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -790,7 +790,7 @@ and detype_r d flags avoid env sigma t = id,l with Not_found -> Id.of_string ("X" ^ string_of_int (Evar.repr evk)), - (Array.map_to_list (fun c -> (Id.of_string "__",c)) cl) + (List.map (fun c -> (Id.of_string "__",c)) cl) in GEvar (id, List.map (on_snd (detype d flags avoid env sigma)) l) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3d887e1a95..f1506f5f59 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -195,7 +195,7 @@ let occur_rigidly flags env evd (evk,_) t = | Evar (evk',l as ev) -> if Evar.equal evk evk' then Rigid true else if is_frozen flags ev then - Rigid (Array.exists (fun x -> rigid_normal_occ (aux x)) l) + Rigid (List.exists (fun x -> rigid_normal_occ (aux x)) l) else Reducible | Cast (p, _, _) -> aux p | Lambda (na, t, b) -> aux b @@ -351,6 +351,14 @@ let ise_array2 evd f v1 v2 = if Int.equal lv1 (Array.length v2) then allrec evd (pred lv1) else UnifFailure (evd,NotSameArgSize) +let rec ise_inst2 evd f l1 l2 = match l1, l2 with +| [], [] -> Success evd +| [], (_ :: _) | (_ :: _), [] -> assert false +| c1 :: l1, c2 :: l2 -> + match ise_inst2 evd f l1 l2 with + | Success evd' -> f evd' c1 c2 + | UnifFailure _ as x -> x + (* Applicative node of stack are read from the outermost to the innermost but are unified the other way. *) let rec ise_app_stack2 env f evd sk1 sk2 = @@ -1019,7 +1027,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty if Evar.equal sp1 sp2 then match ise_stack2 false env evd (evar_conv_x flags) sk1 sk2 with |None, Success i' -> - ise_array2 i' (fun i' -> evar_conv_x flags env i' CONV) al1 al2 + ise_inst2 i' (fun i' -> evar_conv_x flags env i' CONV) al1 al2 |_, (UnifFailure _ as x) -> x |Some _, _ -> UnifFailure (evd,NotSameArgSize) else UnifFailure (evd,NotSameHead) @@ -1241,6 +1249,7 @@ let filter_possible_projections evd c ty ctxt args = (* Since args in the types will be replaced by holes, we count the fv of args to have a well-typed filter; don't know how necessary it is however to have a well-typed filter here *) + let args = Array.of_list args in let fv1 = free_rels evd (mkApp (c,args)) (* Hack: locally untyped *) in let fv2 = collect_vars evd (mkApp (c,args)) in let len = Array.length args in @@ -1309,8 +1318,8 @@ let thin_evars env sigma sign c = match kind !sigma t with | Evar (ev, args) -> let evi = Evd.find_undefined !sigma ev in - let filter = Array.map (fun c -> Id.Set.subset (collect_vars !sigma c) ctx) args in - let filter = Filter.make (Array.to_list filter) in + let filter = List.map (fun c -> Id.Set.subset (collect_vars !sigma c) ctx) args in + let filter = Filter.make filter in let candidates = Option.map (List.map EConstr.of_constr) (evar_candidates evi) in let evd, ev = restrict_evar !sigma ev filter candidates in sigma := evd; whd_evar !sigma t @@ -1336,9 +1345,9 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = if debug_ho_unification () then (Feedback.msg_debug Pp.(str"env rhs: " ++ Termops.Internal.print_env env_rhs); Feedback.msg_debug Pp.(str"env evars: " ++ Termops.Internal.print_env env_evar)); - let args = Array.map (nf_evar evd) args in + let args = List.map (nf_evar evd) args in let vars = List.map NamedDecl.get_id ctxt in - let argsubst = List.map2 (fun id c -> (id, c)) vars (Array.to_list args) in + let argsubst = List.map2 (fun id c -> (id, c)) vars args in let instance = List.map mkVar vars in let rhs = nf_evar evd rhs in if not (noccur_evar env_rhs evd evk rhs) then raise (TypingFailed evd); @@ -1416,7 +1425,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = set_holes env_rhs' evd rhs' subst | [] -> evd, rhs in - let subst = make_subst (ctxt,Array.to_list args,argoccs) in + let subst = make_subst (ctxt,args,argoccs) in let evd, rhs' = set_holes env_rhs evd rhs subst in let rhs' = nf_evar evd rhs' in @@ -1533,7 +1542,7 @@ let default_evar_selection flags evd (ev,args) = in spec :: aux args abs | l, [] -> List.map (fun _ -> default_occurrence_selection) l | [], _ :: _ -> assert false - in aux (Array.to_list args) evi.evar_abstract_arguments + in aux args evi.evar_abstract_arguments let second_order_matching_with_args flags env evd with_ho pbty ev l t = if with_ho then diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index 50187d82cc..71edcaa231 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -113,7 +113,7 @@ let define_evar_as_product env evd (evk,args) = (* Quick way to compute the instantiation of evk with args *) let na,dom,rng = destProd evd prod in let evdom = mkEvar (fst (destEvar evd dom), args) in - let evrngargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in + let evrngargs = mkRel 1 :: List.map (lift 1) args in let evrng = mkEvar (fst (destEvar evd rng), evrngargs) in evd, mkProd (na, evdom, evrng) @@ -152,7 +152,7 @@ let define_evar_as_lambda env evd (evk,args) = let evd,lam = define_pure_evar_as_lambda env evd evk in (* Quick way to compute the instantiation of evk with args *) let na,dom,body = destLambda evd lam in - let evbodyargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in + let evbodyargs = mkRel 1 :: List.map (lift 1) args in let evbody = mkEvar (fst (destEvar evd body), evbodyargs) in evd, mkLambda (na, dom, evbody) @@ -163,7 +163,7 @@ let rec evar_absorb_arguments env evd (evk,args as ev) = function let evd,lam = define_pure_evar_as_lambda env evd evk in let _,_,body = destLambda evd lam in let evk = fst (destEvar evd body) in - evar_absorb_arguments env evd (evk, Array.cons a args) l + evar_absorb_arguments env evd (evk, a :: args) l (* Refining an evar to a sort *) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index e475e4c52b..34684e4a34 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -217,7 +217,7 @@ type 'a update = | NoUpdate open Context.Named.Declaration -let inst_of_vars sign = Array.map_of_list (get_id %> mkVar) sign +let inst_of_vars sign = List.map (get_id %> mkVar) sign let restrict_evar_key evd evk filter candidates = match filter, candidates with @@ -247,7 +247,7 @@ let restrict_applied_evar evd (evk,argsv) filter candidates = | Some filter -> let evi = Evd.find evd evk in let subfilter = Filter.compose (evar_filter evi) filter in - Filter.filter_array subfilter argsv in + Filter.filter_list subfilter argsv in evd,(newevk,newargsv) (* Restrict an evar in the current evar_map *) @@ -258,7 +258,7 @@ let restrict_evar evd evk filter candidates = let restrict_instance evd evk filter argsv = match filter with None -> argsv | Some filter -> let evi = Evd.find evd evk in - Filter.filter_array (Filter.compose (evar_filter evi) filter) argsv + Filter.filter_list (Filter.compose (evar_filter evi) filter) argsv open Context.Rel.Declaration let noccur_evar env evd evk c = @@ -269,7 +269,7 @@ let noccur_evar env evd evk c = if Evar.equal evk evk' then raise Occur else (if check_types then occur_rec false acc (existential_type evd ev'); - Array.iter (occur_rec check_types acc) args') + List.iter (occur_rec check_types acc) args') | Rel i when i > k -> if not (Int.Set.mem (i-k) !cache) then let decl = Environ.lookup_rel i env in @@ -552,17 +552,13 @@ let get_actual_deps env evd aliases l t = open Context.Named.Declaration let remove_instance_local_defs evd evk args = let evi = Evd.find evd evk in - let len = Array.length args in - let rec aux sign i = match sign with - | [] -> - let () = assert (i = len) in [] - | LocalAssum _ :: sign -> - let () = assert (i < len) in - (Array.unsafe_get args i) :: aux sign (succ i) - | LocalDef _ :: sign -> - aux sign (succ i) + let rec aux sign args = match sign, args with + | [], [] -> [] + | LocalAssum _ :: sign, c :: args -> c :: aux sign args + | LocalDef _ :: sign, _ :: args -> aux sign args + | _ -> assert false in - aux (evar_filtered_context evi) 0 + aux (evar_filtered_context evi) args (* Check if an applied evar "?X[args] l" is a Miller's pattern *) @@ -688,7 +684,7 @@ let make_projectable_subst aliases sigma evi args = let all = Int.Map.add i [a, id] all in (rest,all,cstrs,revmap)) | _ -> anomaly (Pp.str "Instance does not match its signature.")) 0 - sign (Array.rev_to_list args,Int.Map.empty,Constrmap.empty,Id.Map.empty) in + sign (List.rev args,Int.Map.empty,Constrmap.empty,Id.Map.empty) in (full_subst,cstr_subst) (*------------------------------------* @@ -765,7 +761,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = (mkRel 1)::(List.map (lift 1) inst_in_sign), push_rel d env,evd,Id.Set.add id.binder_name avoid)) rel_sign - (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,avoid) + (sign1,filter1,args1,inst_in_sign,env1,evd,avoid) in let evd,ev2ty_in_sign = let s = Retyping.get_sort_of env evd ty_in_env in @@ -775,11 +771,12 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = ty_t_in_sign sign2 filter2 inst2_in_env in let (evd, ev2_in_sign) = new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src inst2_in_sign in - let ev2_in_env = (fst (destEvar evd ev2_in_sign), Array.of_list inst2_in_env) in + let ev2_in_env = (fst (destEvar evd ev2_in_sign), inst2_in_env) in (evd, ev2_in_sign, ev2_in_env) let restrict_upon_filter evd evk p args = let oldfullfilter = evar_filter (Evd.find_undefined evd evk) in + let args = Array.of_list args in let len = Array.length args in Filter.restrict_upon oldfullfilter len (fun i -> p (Array.unsafe_get args i)) @@ -1034,7 +1031,7 @@ let invert_invertible_arg fullenv evd aliases k (evk,argsv) args' = let p = invert_arg fullenv evd aliases k evk subst arg in extract_unique_projection p in - Array.map invert args' + List.map invert args' (* Redefines an evar with a smaller context (i.e. it may depend on less * variables) such that c becomes closed. @@ -1390,9 +1387,9 @@ let solve_refl ?(can_drop=false) unify flags env evd pbty evk argsv1 argsv2 = try evdref := Evd.add_universe_constraints !evdref cstr; true with UniversesDiffer -> false in - if Array.equal eq_constr argsv1 argsv2 then !evdref else + if List.equal eq_constr argsv1 argsv2 then !evdref else (* Filter and restrict if needed *) - let args = Array.map2 (fun a1 a2 -> (a1, a2)) argsv1 argsv2 in + let args = List.map2 (fun a1 a2 -> (a1, a2)) argsv1 argsv2 in let untypedfilter = restrict_upon_filter evd evk (fun (a1,a2) -> unify flags TermUnification env evd Reduction.CONV a1 a2) args in @@ -1452,7 +1449,7 @@ let occur_evar_upto_types sigma n c = | Evar (sp,_) when Evar.equal sp n -> raise Occur | Evar (sp,args as e) -> if Evar.Set.mem sp !seen then - Array.iter occur_rec args + List.iter occur_rec args else ( seen := Evar.Set.add sp !seen; Option.iter occur_rec (existential_opt_value0 sigma e); @@ -1570,7 +1567,7 @@ let rec invert_definition unify flags choose imitate_defs (* Evar/Evar problem (but left evar is virtual) *) let aliases = lift_aliases k aliases in (try - let ev = (evk,Array.map (lift k) argsv) in + let ev = (evk,List.map (lift k) argsv) in let evd,body = project_evar_on_evar false unify flags env' !evdref aliases k None ev' ev in evdref := evd; body @@ -1648,7 +1645,7 @@ let rec invert_definition unify flags choose imitate_defs | [], [] -> true | _ -> false in - is_id_subst filter_ctxt (Array.to_list argsv) && + is_id_subst filter_ctxt argsv && closed0 evd rhs && Id.Set.subset (collect_vars evd rhs) !names in diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 0a1b731e6b..3fb80432ad 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -99,7 +99,7 @@ val refresh_universes : env -> evar_map -> types -> evar_map * types val solve_refl : ?can_drop:bool -> conversion_check -> unify_flags -> env -> evar_map -> - bool option -> Evar.t -> constr array -> constr array -> evar_map + bool option -> Evar.t -> constr list -> constr list -> evar_map val solve_evar_evar : ?force:bool -> (env -> evar_map -> bool option -> existential -> constr -> evar_map) -> @@ -128,7 +128,7 @@ val check_evar_instance : unifier -> unify_flags -> env -> evar_map -> Evar.t -> constr -> evar_map val remove_instance_local_defs : - evar_map -> Evar.t -> 'a array -> 'a list + evar_map -> Evar.t -> 'a list -> 'a list val get_type_of_refresh : ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> evar_map * types diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 34498458a4..d672ddc906 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -423,8 +423,8 @@ and nf_evar env sigma evk args = let hyps = Environ.named_context_of_val (Evd.evar_filtered_hyps evi) in let ty = EConstr.to_constr ~abort_on_undefined_evars:false sigma @@ Evd.evar_concl evi in if List.is_empty hyps then begin - assert (Int.equal (Array.length args) 0); - mkEvar (evk, [||]), ty + assert (Array.is_empty args); + mkEvar (evk, []), ty end else (* Let-bound arguments are present in the evar arguments but not @@ -436,7 +436,7 @@ and nf_evar env sigma evk args = (* nf_args takes arguments in the reverse order but produces them in the correct one, so we have to reverse them again for the evar node *) - mkEvar (evk, Array.rev_of_list args), ty + mkEvar (evk, List.rev args), ty let evars_of_evar_map sigma = { Nativelambda.evars_val = Evd.existential_opt_value0 sigma; diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 3f2e690da5..1dfb8b2cd1 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -24,7 +24,7 @@ type case_info_pattern = type constr_pattern = | PRef of GlobRef.t | PVar of Id.t - | PEvar of Evar.t * constr_pattern array + | PEvar of constr_pattern Constr.pexistential | PRel of int | PApp of constr_pattern * constr_pattern array | PSoApp of patvar * constr_pattern list diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index b8635d03b7..6d30e0338e 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -31,7 +31,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with | PRef r1, PRef r2 -> GlobRef.equal r1 r2 | PVar v1, PVar v2 -> Id.equal v1 v2 | PEvar (ev1, ctx1), PEvar (ev2, ctx2) -> - Evar.equal ev1 ev2 && Array.equal constr_pattern_eq ctx1 ctx2 + Evar.equal ev1 ev2 && List.equal constr_pattern_eq ctx1 ctx2 | PRel i1, PRel i2 -> Int.equal i1 i2 | PApp (t1, arg1), PApp (t2, arg2) -> @@ -115,7 +115,7 @@ let rec occurn_pattern n = function (occurn_pattern n c) || (List.exists (fun (_,_,p) -> occurn_pattern n p) br) | PMeta _ | PSoApp _ -> true - | PEvar (_,args) -> Array.exists (occurn_pattern n) args + | PEvar (_,args) -> List.exists (occurn_pattern n) args | PVar _ | PRef _ | PSort _ | PInt _ | PFloat _ -> false | PFix (_,(_,tl,bl)) -> Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl @@ -190,7 +190,7 @@ let pattern_of_constr env sigma t = (* These are the two evar kinds used for existing goals *) (* see Proofview.mark_in_evm *) if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value0 sigma ev) - else PEvar (evk,Array.map (pattern_of_constr env) ctxt) + else PEvar (evk,List.map (pattern_of_constr env) ctxt) | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false | _ -> PMeta None) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 940150b15a..f7e3d651ff 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -607,7 +607,7 @@ let pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk ((id,c)::subst, update, sigma) in let subst,inst,sigma = List.fold_right f hyps ([],update,sigma) in check_instance loc subst inst; - sigma, Array.map_of_list snd subst + sigma, List.map snd subst module Default = struct diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 70605d58ab..2c717b8774 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -86,7 +86,7 @@ let evaluable_reference_eq sigma r1 r2 = match r1, r2 with | EvalVar id1, EvalVar id2 -> Id.equal id1 id2 | EvalRel i1, EvalRel i2 -> Int.equal i1 i2 | EvalEvar (e1, ctx1), EvalEvar (e2, ctx2) -> - Evar.equal e1 e2 && Array.equal (EConstr.eq_constr sigma) ctx1 ctx2 + Evar.equal e1 e2 && List.equal (EConstr.eq_constr sigma) ctx1 ctx2 | _ -> false let mkEvalRef ref u = @@ -408,7 +408,7 @@ let substl_with_function subst sigma constr = let (sigma, evk) = Evarutil.new_pure_evar venv sigma dummy in evd := sigma; minargs := Evar.Map.add evk min !minargs; - Vars.lift k (mkEvar (evk, [|fx;ref|])) + Vars.lift k (mkEvar (evk, [fx; ref])) | (fx, None) -> Vars.lift k fx else mkRel (i - Array.length v) | _ -> @@ -455,7 +455,7 @@ let substl_checking_arity env subst sigma c = (* we propagate the constraints: solved problems are substituted; the other ones are replaced by the function symbol *) let rec nf_fix c = match EConstr.kind sigma c with - | Evar (i,[|fx;f|]) when Evar.Map.mem i minargs -> + | Evar (i,[fx;f]) when Evar.Map.mem i minargs -> (* FIXME: find a less hackish way of doing this *) begin match EConstr.kind sigma' c with | Evar _ -> f diff --git a/pretyping/unification.ml b/pretyping/unification.ml index e168f6d1b6..f5aaac315a 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -76,7 +76,7 @@ let occur_meta_or_undefined_evar evd c = | Evar (ev,args) -> (match evar_body (Evd.find evd ev) with | Evar_defined c -> - occrec (EConstr.Unsafe.to_constr c); Array.iter occrec args + occrec (EConstr.Unsafe.to_constr c); List.iter occrec args | Evar_empty -> raise Occur) | _ -> Constr.iter occrec c in try occrec c; false with Occur | Not_found -> true @@ -138,9 +138,9 @@ let abstract_list_all env evd typ c l = error_cannot_find_well_typed_abstraction env evd p l (Some (env',x)) in evd,(p,typp) -let set_occurrences_of_last_arg args = +let set_occurrences_of_last_arg n = Evarconv.AtOccurrences AllOccurrences :: - List.tl (Array.map_to_list (fun _ -> Evarconv.Unspecified Abstraction.Abstract) args) + List.tl (List.init n (fun _ -> Evarconv.Unspecified Abstraction.Abstract)) let occurrence_test _ _ _ env sigma _ c1 c2 = match EConstr.eq_constr_universes env sigma c1 c2 with @@ -153,7 +153,8 @@ let abstract_list_all_with_dependencies env evd typ c l = let (evd, ev) = new_evar env evd typ in let evd,ev' = evar_absorb_arguments env evd (destEvar evd ev) l in let n = List.length l in - let argoccs = set_occurrences_of_last_arg (Array.sub (snd ev') 0 n) in + let () = assert (n <= List.length (snd ev')) in + let argoccs = set_occurrences_of_last_arg n in let evd,b = Evarconv.second_order_matching (Evarconv.default_flags_of TransparentState.empty) @@ -623,7 +624,7 @@ let subst_defined_metas_evars sigma (bl,el) c = substrec (EConstr.Unsafe.to_constr (pi2 (List.find select bl))) | Evar (evk,args) -> let eq c1 c2 = Constr.equal c1 (EConstr.Unsafe.to_constr c2) in - let select (_,(evk',args'),_) = Evar.equal evk evk' && Array.for_all2 eq args args' in + let select (_,(evk',args'),_) = Evar.equal evk evk' && List.for_all2 eq args args' in (try substrec (EConstr.Unsafe.to_constr (pi3 (List.find select el))) with Not_found -> Constr.map substrec c) | _ -> Constr.map substrec c diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index d4da93cc5b..37c34d55cf 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -205,7 +205,7 @@ and nf_evar env sigma evk stk = let hyps = Environ.named_context_of_val (Evd.evar_filtered_hyps evi) in let concl = EConstr.to_constr ~abort_on_undefined_evars:false sigma @@ Evd.evar_concl evi in if List.is_empty hyps then - nf_stk env sigma (mkEvar (evk, [||])) concl stk + nf_stk env sigma (mkEvar (evk, [])) concl stk else match stk with | Zapp args :: stk -> (* We assume that there is no consecutive Zapp nodes in a VM stack. Is that @@ -217,6 +217,7 @@ and nf_evar env sigma evk stk = let t = List.fold_left fold concl hyps in let t, args = nf_args env sigma args t in let inst, args = Array.chop (List.length hyps) args in + let inst = Array.to_list inst in let c = mkApp (mkEvar (evk, inst), args) in nf_stk env sigma c t stk | _ -> diff --git a/printing/printer.ml b/printing/printer.ml index 81c0a36f53..c2f73715f0 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -989,4 +989,5 @@ let print_and_diff oldp newp = let pr_typing_flags flags = str "check_guarded: " ++ bool flags.check_guarded ++ fnl () ++ str "check_positive: " ++ bool flags.check_positive ++ fnl () - ++ str "check_universes: " ++ bool flags.check_universes + ++ str "check_universes: " ++ bool flags.check_universes ++ fnl () + ++ str "cumulative sprop: " ++ bool flags.cumulative_sprop diff --git a/proofs/goal.ml b/proofs/goal.ml index b1f8fd3e97..53d3047bc7 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -69,7 +69,7 @@ module V82 = struct let (evars, evk) = Evarutil.new_pure_evar_full evars ~typeclass_candidate:false evi in let evars = Evd.restore_future_goals evars prev_future_goals in let ctxt = Environ.named_context_of_val hyps in - let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in + let inst = List.map (NamedDecl.get_id %> EConstr.mkVar) ctxt in let ev = EConstr.mkEvar (evk,inst) in (evk, ev, evars) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 57eab7ddf8..a51fc8b347 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1188,7 +1188,7 @@ let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique = with Refiner.FailError _ -> raise Not_found in let evd = sig_sig gls' in - let t' = mkEvar (ev, Array.of_list subst) in + let t' = mkEvar (ev, subst) in let term = Evarutil.nf_evar evd t' in term, evd end in diff --git a/tactics/eauto.ml b/tactics/eauto.ml index a89e5ef19a..28b5ed5811 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -430,29 +430,39 @@ let make_dimension n = function | None -> (true,make_depth n) | Some d -> (false,d) +let autounfolds ids csts gl cls = + let hyps = Tacmach.New.pf_ids_of_hyps gl in + let env = Tacmach.New.pf_env gl in + let ids = List.filter (fun id -> List.mem id hyps && Tacred.is_evaluable env (EvalVarRef id)) ids in + let csts = List.filter (fun cst -> Tacred.is_evaluable env (EvalConstRef cst)) csts in + let flags = + List.fold_left (fun flags cst -> CClosure.RedFlags.(red_add flags (fCONST cst))) + (List.fold_left (fun flags id -> CClosure.RedFlags.(red_add flags (fVAR id))) + CClosure.betaiotazeta ids) csts + in reduct_option ~check:false (Reductionops.clos_norm_flags flags, DEFAULTcast) cls + let cons a l = a :: l -let autounfolds db occs cls gl = - let unfolds = List.concat (List.map (fun dbname -> - let db = try searchtable_map dbname - with Not_found -> user_err ~hdr:"autounfold" (str "Unknown database " ++ str dbname) - in - let (ids, csts) = Hint_db.unfolds db in - let hyps = pf_ids_of_hyps gl in - let ids = Id.Set.filter (fun id -> List.mem id hyps) ids in - Cset.fold (fun cst -> cons (AllOccurrences, EvalConstRef cst)) csts - (Id.Set.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db) - in Proofview.V82.of_tactic (unfold_option unfolds cls) gl +exception UnknownDatabase of string let autounfold db cls = - Proofview.V82.tactic begin fun gl -> - let cls = concrete_clause_of (fun () -> pf_ids_of_hyps gl) cls in - let tac = autounfolds db in - tclMAP (function - | OnHyp (id,occs,where) -> tac occs (Some (id,where)) - | OnConcl occs -> tac occs None) - cls gl - end + if not (Locusops.clause_with_generic_occurrences cls) then + user_err ~hdr:"autounfold" (str "\"at\" clause not supported"); + match List.fold_left (fun (ids, csts) dbname -> + let db = try searchtable_map dbname + with Not_found -> raise (UnknownDatabase dbname) + in + let (db_ids, db_csts) = Hint_db.unfolds db in + (Id.Set.fold cons db_ids ids, Cset.fold cons db_csts csts)) ([], []) db + with + | (ids, csts) -> Proofview.Goal.enter begin fun gl -> + let cls = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cls in + let tac = autounfolds ids csts gl in + Tacticals.New.tclMAP (function + | OnHyp (id, _, where) -> tac (Some (id, where)) + | OnConcl _ -> tac None) cls + end + | exception UnknownDatabase dbname -> Tacticals.New.tclZEROMSG (str "Unknown database " ++ str dbname) let autounfold_tac db cls = Proofview.tclUNIT () >>= fun () -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c79aca3d3c..0df4f5b207 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2763,8 +2763,8 @@ let pose_tac na c = let id = make_annot id Sorts.Relevant in let nhyps = EConstr.push_named_context_val (NamedDecl.LocalDef (id, c, t)) hyps in let (sigma, ev) = Evarutil.new_pure_evar nhyps sigma concl in - let inst = Array.map_of_list (fun d -> mkVar (get_id d)) (named_context env) in - let body = mkEvar (ev, Array.append [|mkRel 1|] inst) in + let inst = List.map (fun d -> mkVar (get_id d)) (named_context env) in + let body = mkEvar (ev, mkRel 1 :: inst) in (sigma, mkLetIn (map_annot Name.mk_name id, c, t, body)) end end @@ -4499,7 +4499,7 @@ let check_expected_type env sigma (elimc,bl) elimt = if n == 0 then error "Scheme cannot be applied."; let sigma,cl = make_evar_clause env sigma ~len:(n - 1) elimt in let sigma = solve_evar_clause env sigma true cl bl in - let (_,u,_) = destProd sigma cl.cl_concl in + let (_,u,_) = destProd sigma (whd_all env sigma cl.cl_concl) in fun t -> match Evarconv.unify_leq_delay env sigma t u with | _sigma -> true | exception Evarconv.UnableToUnify _ -> false diff --git a/test-suite/Makefile b/test-suite/Makefile index 954a922c8c..dece21885c 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -62,6 +62,10 @@ coqtopbyte := $(BIN)coqtop.byte -q coqc_interactive := $(coqc) -test-mode -async-proofs-cache force coqdep := $(BIN)coqdep +# This is the convention for coq_makefile +OPT=-$(BEST) +export OPT + VERBOSE?= SHOW := $(if $(VERBOSE),@true,@echo) HIDE := $(if $(VERBOSE),,@) diff --git a/test-suite/bugs/closed/HoTT_coq_107.v b/test-suite/bugs/closed/HoTT_coq_107.v index fa4072a8f6..91f5c423a5 100644 --- a/test-suite/bugs/closed/HoTT_coq_107.v +++ b/test-suite/bugs/closed/HoTT_coq_107.v @@ -2,6 +2,7 @@ (* File reduced by coq-bug-finder from 4897 lines to 2605 lines, then from 2297 lines to 236 lines, then from 239 lines to 137 lines, then from 118 lines to 67 lines, then from 520 lines to 76 lines. *) (** Note: The bug here is the same as the #113, that is, HoTT_coq_113.v *) Require Import Coq.Init.Logic. +Require Import Coq.Init.Ltac. Global Set Universe Polymorphism. Global Set Asymmetric Patterns. Set Implicit Arguments. diff --git a/test-suite/bugs/closed/bug_12045.v b/test-suite/bugs/closed/bug_12045.v new file mode 100644 index 0000000000..4e416778a9 --- /dev/null +++ b/test-suite/bugs/closed/bug_12045.v @@ -0,0 +1,19 @@ +(* Check enough reduction happens in the conclusion of an induction scheme *) + +Lemma foo : + forall (P : nat -> Prop), + (forall n, P (S n)) -> + forall n, + (fun e => + IsSucc e -> + P e) n. +Proof. +Admitted. + +Theorem bar : forall n, + IsSucc n -> + True. +Proof. + intros. + Fail induction n using foo. (* was an anomaly *) +Admitted. diff --git a/test-suite/bugs/closed/bug_3881.v b/test-suite/bugs/closed/bug_3881.v index d7e097e326..50e9de60e5 100644 --- a/test-suite/bugs/closed/bug_3881.v +++ b/test-suite/bugs/closed/bug_3881.v @@ -4,6 +4,7 @@ coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (90ed6636dea41486ddf2cc0daead83f9f0788163) *) Generalizable All Variables. Require Import Coq.Init.Notations. +Require Import Coq.Init.Ltac. Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). Notation "A -> B" := (forall (_ : A), B) : type_scope. Axiom admit : forall {T}, T. diff --git a/test-suite/bugs/closed/bug_4527.v b/test-suite/bugs/closed/bug_4527.v index dfb07520f1..cf802eb89b 100644 --- a/test-suite/bugs/closed/bug_4527.v +++ b/test-suite/bugs/closed/bug_4527.v @@ -5,7 +5,7 @@ then from 269 lines to 255 lines *) (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0 coqtop version 8.5 (January 2016) *) -Declare ML Module "ltac_plugin". +Require Import Coq.Init.Ltac. Inductive False := . Axiom proof_admitted : False. Tactic Notation "admit" := case proof_admitted. diff --git a/test-suite/bugs/closed/bug_4533.v b/test-suite/bugs/closed/bug_4533.v index d2f9fb9099..2d628f414d 100644 --- a/test-suite/bugs/closed/bug_4533.v +++ b/test-suite/bugs/closed/bug_4533.v @@ -5,7 +5,7 @@ then from 285 lines to 271 lines *) (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0 coqtop version 8.5 (January 2016) *) -Declare ML Module "ltac_plugin". +Require Import Coq.Init.Ltac. Inductive False := . Axiom proof_admitted : False. Tactic Notation "admit" := case proof_admitted. diff --git a/test-suite/bugs/closed/bug_4544.v b/test-suite/bugs/closed/bug_4544.v index e9e9c552f6..213c91bfa0 100644 --- a/test-suite/bugs/closed/bug_4544.v +++ b/test-suite/bugs/closed/bug_4544.v @@ -2,7 +2,7 @@ (* File reduced by coq-bug-finder from original input, then from 2553 lines to 1932 lines, then from 1946 lines to 1932 lines, then from 2467 lines to 1002 lines, then from 1016 lines to 1002 lines *) (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0 coqtop version 8.5 (January 2016) *) -Declare ML Module "ltac_plugin". +Require Import Coq.Init.Ltac. Inductive False := . Axiom proof_admitted : False. Tactic Notation "admit" := case proof_admitted. diff --git a/test-suite/bugs/closed/bug_6661.v b/test-suite/bugs/closed/bug_6661.v index 28a9ffc7bd..0f4ae2b4c5 100644 --- a/test-suite/bugs/closed/bug_6661.v +++ b/test-suite/bugs/closed/bug_6661.v @@ -7,6 +7,7 @@ Require Export Coq.Init.Notations. +Require Export Coq.Init.Ltac. Notation "'∏' x .. y , P" := (forall x, .. (forall y, P) ..) (at level 200, x binder, y binder, right associativity) : type_scope. Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..) diff --git a/test-suite/bugs/closed/bug_7812.v b/test-suite/bugs/closed/bug_7812.v new file mode 100644 index 0000000000..a714eea81d --- /dev/null +++ b/test-suite/bugs/closed/bug_7812.v @@ -0,0 +1,30 @@ +Module Foo. + Definition binary A := A -> A -> Prop. + + Definition inter A (R1 R2 : binary A): binary A := + fun (x y:A) => R1 x y /\ R2 x y. +End Foo. + +Module Simple_sparse_proof. + Parameter node : Type. + Parameter graph : Type. + Parameter has_edge : graph -> node -> node -> Prop. + Implicit Types x y z : node. + Implicit Types G : graph. + + Parameter mem : forall A, A -> list A -> Prop. + Hypothesis mem_nil : forall x, mem node x nil = False. + + Definition notin (l: list node): node -> node -> Prop := + fun x y => ~ mem node x l /\ ~ mem node y l. + + Definition edge_notin G l : node -> node -> Prop := + Foo.inter node (has_edge G) (notin l). + + Hint Unfold Foo.inter notin edge_notin : rel_crush. + + Lemma edge_notin_nil G : forall x y, edge_notin G nil x y <-> has_edge G x y. + Proof. + intros. autounfold with rel_crush. rewrite !mem_nil. tauto. + Qed. +End Simple_sparse_proof. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index e121b5e86c..f48eaac4c9 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -14,6 +14,10 @@ Entry constr:myconstr is : nat [<< # 0 >>] : option nat +[b + c] + : nat +fun a : nat => [a + a] + : nat -> nat [1 {f 1}] : Expr fun (x : nat) (y z : Expr) => [1 + y z + {f x}] @@ -81,18 +85,18 @@ fun x : nat => [x] : nat -> nat ∀ x : nat, x = x : Prop -File "stdin", line 219, characters 0-160: +File "stdin", line 226, characters 0-160: Warning: Notation "∀ _ .. _ , _" was already defined with a different format in scope type_scope. [notation-incompatible-format,parsing] ∀x : nat,x = x : Prop -File "stdin", line 232, characters 0-60: +File "stdin", line 239, characters 0-60: Warning: Notation "_ %%% _" was already defined with a different format. [notation-incompatible-format,parsing] -File "stdin", line 236, characters 0-64: +File "stdin", line 243, characters 0-64: Warning: Notation "_ %%% _" was already defined with a different format. [notation-incompatible-format,parsing] -File "stdin", line 241, characters 0-62: +File "stdin", line 248, characters 0-62: Warning: Lonely notation "_ %%%% _" was already defined with a different format. [notation-incompatible-format,parsing] 3 %% 4 @@ -101,9 +105,9 @@ format. [notation-incompatible-format,parsing] : nat 3 %% 4 : nat -File "stdin", line 269, characters 0-61: +File "stdin", line 276, characters 0-61: Warning: The format modifier is irrelevant for only parsing rules. [irrelevant-format-only-parsing,parsing] -File "stdin", line 273, characters 0-63: +File "stdin", line 280, characters 0-63: Warning: The only parsing modifier has no effect in Reserved Notation. [irrelevant-reserved-notation-only-parsing,parsing] diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 1cf0d919b1..4d4b37a8b2 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -22,6 +22,13 @@ Notation "<< x >>" := x (in custom myconstr at level 3, x custom anotherconstr a Notation "# x" := (Some x) (in custom anotherconstr at level 8, x constr at level 9). Check [ << # 0 >> ]. +(* Now check with global *) + +Axiom c : nat. +Notation "x" := x (in custom myconstr at level 0, x global). +Check [ b + c ]. +Check fun a => [ a + a ]. + End A. Module B. diff --git a/theories/Init/Byte.v b/theories/Init/Byte.v index 33eabb20d9..7449b52d76 100644 --- a/theories/Init/Byte.v +++ b/theories/Init/Byte.v @@ -10,6 +10,7 @@ (** * Bytes *) +Require Import Coq.Init.Ltac. Require Import Coq.Init.Datatypes. Require Import Coq.Init.Logic. Require Import Coq.Init.Specif. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 50d4314a6b..0f2717beef 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -11,6 +11,7 @@ Set Implicit Arguments. Require Import Notations. +Require Import Ltac. Require Import Logic. (********************************************************************) diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index ae48febc49..8f9f68a292 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -11,6 +11,7 @@ Set Implicit Arguments. Require Export Notations. +Require Import Ltac. Notation "A -> B" := (forall (_ : A), B) : type_scope. diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index d07fe68715..3d9937ae89 100644 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -13,6 +13,7 @@ Set Implicit Arguments. +Require Import Ltac. Require Import Datatypes. Require Export Logic. diff --git a/theories/Init/Ltac.v b/theories/Init/Ltac.v new file mode 100644 index 0000000000..ac5a69a38a --- /dev/null +++ b/theories/Init/Ltac.v @@ -0,0 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Declare ML Module "ltac_plugin". + +Export Set Default Proof Mode "Classic". diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index a5e4178b93..da540cb099 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -129,9 +129,3 @@ Bind Scope type_scope with Sortclass. Open Scope core_scope. Open Scope function_scope. Open Scope type_scope. - -(** ML Tactic Notations *) - -Declare ML Module "ltac_plugin". - -Global Set Default Proof Mode "Classic". diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 394fa879c4..02903643d4 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -26,6 +26,7 @@ *) Require Import Notations. +Require Import Ltac. Require Import Datatypes. Require Import Logic. Require Coq.Init.Nat. diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 71ba3e645d..6a81517d7e 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -18,10 +18,11 @@ Require Coq.Init.Decimal. Require Coq.Init.Nat. Require Export Peano. Require Export Coq.Init.Wf. +Require Export Coq.Init.Ltac. Require Export Coq.Init.Tactics. Require Export Coq.Init.Tauto. (* Some initially available plugins. See also: - - ltac_plugin (in Notations) + - ltac_plugin (in Ltac) - tauto_plugin (in Tauto). *) Declare ML Module "cc_plugin". diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 59ee252d35..4ff007570e 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -14,6 +14,7 @@ Set Implicit Arguments. Set Reversible Pattern Implicit. Require Import Notations. +Require Import Ltac. Require Import Datatypes. Require Import Logic. diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index a4347bbe62..b13206db94 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -9,6 +9,7 @@ (************************************************************************) Require Import Notations. +Require Import Ltac. Require Import Logic. Require Import Specif. diff --git a/theories/Init/Tauto.v b/theories/Init/Tauto.v index 87b7a9a3be..2fc6f3cfa6 100644 --- a/theories/Init/Tauto.v +++ b/theories/Init/Tauto.v @@ -1,4 +1,17 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** * The tauto and intuition tactics *) + Require Import Notations. +Require Import Ltac. Require Import Datatypes. Require Import Logic. diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 06afd9bac0..a305626eb3 100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -16,6 +16,7 @@ Set Implicit Arguments. Require Import Notations. +Require Import Ltac. Require Import Logic. Require Import Datatypes. diff --git a/theories/Sorting/CPermutation.v b/theories/Sorting/CPermutation.v new file mode 100644 index 0000000000..fac9cd1d6d --- /dev/null +++ b/theories/Sorting/CPermutation.v @@ -0,0 +1,283 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** * Circular Shifts (aka Cyclic Permutations) *) + +(** The main inductive [CPermutation] relates lists up to circular shifts of their elements. + +For example: [CPermutation [a1;a2;a3;a4;a5] [a4;a5;a1;a2;a3]] + +Note: Terminology does not seem to be strongly fixed in English. For the record, it is "permutations circulaires" in French. +*) + +Require Import List Permutation Morphisms PeanoNat. +Import ListNotations. (* For notations [] and [a;b;c] *) +Set Implicit Arguments. + +Section CPermutation. + +Variable A:Type. + +(** Definition *) + +Inductive CPermutation : list A -> list A -> Prop := +| cperm : forall l1 l2, CPermutation (l1 ++ l2) (l2 ++ l1). + +Instance CPermutation_Permutation : Proper (CPermutation ==> (@Permutation A)) id. +Proof. intros ? ? [? ?]; apply Permutation_app_comm. Qed. + +(** Some facts about [CPermutation] *) + +Theorem CPermutation_nil : forall l, CPermutation [] l -> l = []. +Proof. +intros l HC; inversion HC as [l1 l2 Heq]; subst. +now apply app_eq_nil in Heq; destruct Heq; subst. +Qed. + +Theorem CPermutation_nil_cons : forall l a, ~ CPermutation [] (a :: l). +Proof. intros l a HC; apply CPermutation_nil in HC; inversion HC. Qed. + +Theorem CPermutation_nil_app_cons : forall l1 l2 a, + ~ CPermutation [] (l1 ++ a ::l2). +Proof. +intros l1 l2 a HC; apply CPermutation_nil in HC; destruct l1; inversion HC. +Qed. + +Lemma CPermutation_split : forall l1 l2, + CPermutation l1 l2 <-> exists n, l2 = skipn n l1 ++ firstn n l1. +Proof. +intros l1 l2; split. +- intros [l1' l2']. + exists (length l1'). + rewrite skipn_app, skipn_all, Nat.sub_diag; simpl; f_equal. + now rewrite firstn_app, firstn_all, Nat.sub_diag; simpl; rewrite app_nil_r. +- now intros [n ->]; rewrite <- (firstn_skipn n) at 1. +Qed. + + +(** Equivalence relation *) + +Theorem CPermutation_refl : forall l, CPermutation l l. +Proof. +intros l; now rewrite <- (app_nil_l l) at 1; rewrite <- (app_nil_r l) at 2. +Qed. + +Instance CPermutation_refl' : Proper (Logic.eq ==> CPermutation) id. +Proof. intros ? ? ->; apply CPermutation_refl. Qed. + +Theorem CPermutation_sym : forall l l', CPermutation l l' -> CPermutation l' l. +Proof. now intros ? ? [? ?]. Qed. + +Theorem CPermutation_trans : forall l l' l'', + CPermutation l l' -> CPermutation l' l'' -> CPermutation l l''. +Proof. +intros l l' l'' HC1 HC2. +inversion HC1 as [l1 l2]; inversion HC2 as [l3 l4 Heq Heq']; subst. +clear - Heq; revert l1 l2 l4 Heq; clear; induction l3; simpl; intros. +- now subst; rewrite app_nil_r. +- destruct l2 as [| b]. + + simpl in Heq; subst. + now rewrite app_nil_r, app_comm_cons. + + inversion Heq as [[Heqb Heq']]; subst. + replace (l1 ++ b :: l2) with ((l1 ++ b :: nil) ++ l2) + by now rewrite <- app_assoc, <- app_comm_cons. + replace (l4 ++ b :: l3) with ((l4 ++ b :: nil) ++ l3) + by now rewrite <- app_assoc, <- app_comm_cons. + apply IHl3. + now rewrite 2 app_assoc, Heq'. +Qed. + +End CPermutation. + +Hint Resolve CPermutation_refl : core. + +(* These hints do not reduce the size of the problem to solve and they + must be used with care to avoid combinatoric explosions *) + +Local Hint Resolve cperm CPermutation_sym CPermutation_trans : core. + +Instance CPermutation_Equivalence A : Equivalence (@CPermutation A) | 10 := { + Equivalence_Reflexive := @CPermutation_refl A ; + Equivalence_Symmetric := @CPermutation_sym A ; + Equivalence_Transitive := @CPermutation_trans A }. + + +Section CPermutation_properties. + +Variable A B:Type. + +Implicit Types a b : A. +Implicit Types l : list A. + +(** Compatibility with others operations on lists *) + +Lemma CPermutation_app : forall l1 l2 l3, + CPermutation (l1 ++ l2) l3 -> CPermutation (l2 ++ l1) l3. +Proof. intros l1 l2 l3 HC; now transitivity (l1 ++ l2). Qed. + +Theorem CPermutation_app_comm : forall l1 l2, CPermutation (l1 ++ l2) (l2 ++ l1). +Proof. apply cperm. Qed. + +Lemma CPermutation_app_rot : forall l1 l2 l3, + CPermutation (l1 ++ l2 ++ l3) (l2 ++ l3 ++ l1). +Proof. intros l1 l2 l3; now rewrite (app_assoc l2). Qed. + +Lemma CPermutation_cons_append : forall l a, + CPermutation (a :: l) (l ++ [a]). +Proof. intros l a; now rewrite <- (app_nil_l l), app_comm_cons. Qed. + +Lemma CPermutation_morph_cons : forall P : list A -> Prop, + (forall a l, P (l ++ [a]) -> P (a :: l)) -> + Proper (@CPermutation A ==> iff) P. +Proof. +enough (forall P : list A -> Prop, + (forall a l, P (l ++ [a]) -> P (a :: l)) -> + forall l1 l2, CPermutation l1 l2 -> P l1 -> P l2) + as Himp + by now intros P HP l1 l2 HC; split; [ | symmetry in HC ]; apply Himp. +intros P HP l1 l2 [l1' l2']. +revert l1'; induction l2' using rev_ind; intros l1' HPl. +- now rewrite app_nil_r in HPl. +- rewrite app_assoc in HPl. + apply HP in HPl. + rewrite <- app_assoc, <- app_comm_cons, app_nil_l. + now apply IHl2'. +Qed. + +Lemma CPermutation_length_1 : forall a b, CPermutation [a] [b] -> a = b. +Proof. intros; now apply Permutation_length_1, CPermutation_Permutation. Qed. + +Lemma CPermutation_length_1_inv : forall l a, CPermutation [a] l -> l = [a]. +Proof. intros; now apply Permutation_length_1_inv, CPermutation_Permutation. Qed. + +Lemma CPermutation_swap : forall a b, CPermutation [a; b] [b; a]. +Proof. +intros; now change [a; b] with ([a] ++ [b]); change [b; a] with ([b] ++ [a]). +Qed. + +Lemma CPermutation_length_2 : forall a1 a2 b1 b2, + CPermutation [a1; a2] [b1; b2] -> + a1 = b1 /\ a2 = b2 \/ a1 = b2 /\ a2 = b1. +Proof. intros; now apply Permutation_length_2, CPermutation_Permutation. Qed. + +Lemma CPermutation_length_2_inv : forall a b l, + CPermutation [a; b] l -> l = [a; b] \/ l = [b; a]. +Proof. intros; now apply Permutation_length_2_inv, CPermutation_Permutation. Qed. + +Lemma CPermutation_vs_elt_inv : forall l l1 l2 a, + CPermutation l (l1 ++ a :: l2) -> + exists l' l'', l2 ++ l1 = l'' ++ l' /\ l = l' ++ a :: l''. +Proof. +intros l l1 l2 a HC. +inversion HC as [l1' l2' Heq' Heq]; clear HC; subst. +enough (exists l3, (l2' ++ l3 = l1 /\ l1' = l3 ++ a :: l2) + \/ (l2' = l1 ++ a :: l3 /\ l3 ++ l1' = l2)) + as [l3 [[<- ->]|[-> <-]]]. +- exists l3, (l2 ++ l2'); rewrite app_comm_cons; intuition. +- exists (l1' ++ l1), l3; intuition. +- revert l1' l2' l2 Heq; induction l1; simpl; intros l1' l2' l2 Heq. + + destruct l2'; inversion Heq; subst. + * exists nil; intuition. + * exists l2'; intuition. + + destruct l2'; inversion Heq; subst. + * exists (a0 :: l1); intuition. + * apply IHl1 in H1 as [l3 [[<- ->]|[-> <-]]]; exists l3; intuition. +Qed. + +Lemma CPermutation_vs_cons_inv : forall l l0 a, + CPermutation l (a :: l0) -> exists l' l'', l0 = l'' ++ l' /\ l = l' ++ a :: l''. +Proof. intros; rewrite <- (app_nil_r l0); now apply CPermutation_vs_elt_inv. Qed. + +End CPermutation_properties. + + +(** [rev], [in], [map], [Forall], [Exists], etc. *) + +Global Instance CPermutation_rev A : + Proper (@CPermutation A ==> @CPermutation A) (@rev A) | 10. +Proof. +intro l; induction l; intros l' HC. +- now apply CPermutation_nil in HC; subst. +- symmetry in HC. + destruct (CPermutation_vs_cons_inv HC) as [l1 [l2 [-> ->]]]. + simpl; rewrite ? rev_app_distr; simpl. + now rewrite <- app_assoc. +Qed. + +Global Instance CPermutation_in A a : + Proper (@CPermutation A ==> Basics.impl) (In a). +Proof. +intros l l' HC Hin. +now apply Permutation_in with l; [ apply CPermutation_Permutation | ]. +Qed. + +Global Instance CPermutation_in' A : + Proper (Logic.eq ==> @CPermutation A ==> iff) (@In A) | 10. +Proof. intros a a' <- l l' HC; split; now apply CPermutation_in. Qed. + +Global Instance CPermutation_map A B (f : A -> B) : + Proper (@CPermutation A ==> @CPermutation B) (map f) | 10. +Proof. now intros ? ? [l1 l2]; rewrite 2 map_app. Qed. + +Lemma CPermutation_map_inv A B : forall (f : A -> B) m l, + CPermutation m (map f l) -> exists l', m = map f l' /\ CPermutation l l'. +Proof. +induction m as [| b m]; intros l HC. +- exists nil; split; auto. + destruct l; auto. + apply CPermutation_nil in HC; inversion HC. +- symmetry in HC. + destruct (CPermutation_vs_cons_inv HC) as [m1 [m2 [-> Heq]]]. + apply map_eq_app in Heq as [l1 [l1' [-> [-> Heq]]]]. + symmetry in Heq. + apply map_eq_cons in Heq as [a [l1'' [-> [-> ->]]]]. + exists (a :: l1'' ++ l1); split. + + now simpl; rewrite map_app. + + now rewrite app_comm_cons. +Qed. + +Lemma CPermutation_image A B : forall (f : A -> B) a l l', + CPermutation (a :: l) (map f l') -> exists a', a = f a'. +Proof. +intros f a l l' HP. +now apply CPermutation_Permutation, Permutation_image in HP. +Qed. + +Instance CPermutation_Forall A (P : A -> Prop) : + Proper (@CPermutation A ==> Basics.impl) (Forall P). +Proof. +intros ? ? [? ?] HF. +now apply Forall_app in HF; apply Forall_app. +Qed. + +Instance CPermutation_Exists A (P : A -> Prop) : + Proper (@CPermutation A ==> Basics.impl) (Exists P). +Proof. +intros ? ? [? ?] HE. +apply Exists_app in HE; apply Exists_app; intuition. +Qed. + +Lemma CPermutation_Forall2 A B (P : A -> B -> Prop) : + forall l1 l1' l2, CPermutation l1 l1' -> Forall2 P l1 l2 -> exists l2', + CPermutation l2 l2' /\ Forall2 P l1' l2'. +Proof. +intros ? ? ? [? ?] HF. +apply Forall2_app_inv_l in HF as (l2' & l2'' & HF' & HF'' & ->). +exists (l2'' ++ l2'); intuition. +now apply Forall2_app. +Qed. + + +(** As an equivalence relation compatible with some operations, +[CPermutation] can be used through [rewrite]. *) +Example CPermutation_rewrite_rev A (l1 l2 l3: list A) : + CPermutation l1 l2 -> + CPermutation (rev l1) l3 -> CPermutation l3 (rev l2). +Proof. intros HP1 HP2; rewrite <- HP1, HP2; reflexivity. Qed. diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v index 466e2bf994..443931e5bb 100644 --- a/theories/Vectors/VectorSpec.v +++ b/theories/Vectors/VectorSpec.v @@ -15,7 +15,7 @@ *) Require Fin. -Require Import VectorDef. +Require Import VectorDef PeanoNat Eqdep_dec. Import VectorNotations. Definition cons_inj {A} {a1 a2} {n} {v1 v2 : t A n} @@ -32,6 +32,8 @@ Defined. (** Lemmas are done for functions that use [Fin.t] but thanks to [Peano_dec.le_unique], all is true for the one that use [lt] *) +(** ** Properties of [nth] and [nth_order] *) + Lemma eq_nth_iff A n (v1 v2: t A n): (forall p1 p2, p1 = p2 -> v1 [@ p1 ] = v2 [@ p2 ]) <-> v1 = v2. Proof. @@ -44,12 +46,35 @@ split. - intros; now f_equal. Qed. +Lemma nth_order_hd A: forall n (v : t A (S n)) (H : 0 < S n), + nth_order v H = hd v. +Proof. intros; now rewrite (eta v). Qed. + +Lemma nth_order_tl A: forall n k (v : t A (S n)) (H : k < n) (HS : S k < S n), + nth_order (tl v) H = nth_order v HS. +Proof. +induction n; intros. +- inversion H. +- rewrite (eta v). + unfold nth_order; simpl. + now rewrite (Fin.of_nat_ext H (Lt.lt_S_n _ _ HS)). +Qed. + Lemma nth_order_last A: forall n (v: t A (S n)) (H: n < S n), nth_order v H = last v. Proof. unfold nth_order; refine (@rectS _ _ _ _); now simpl. Qed. +Lemma nth_order_ext A: forall n k (v : t A n) (H1 H2 : k < n), + nth_order v H1 = nth_order v H2. +Proof. +intros; unfold nth_order. +now rewrite (Fin.of_nat_ext H1 H2). +Qed. + +(** ** Properties of [shiftin] and [shiftrepeat] *) + Lemma shiftin_nth A a n (v: t A n) k1 k2 (eq: k1 = k2): nth (shiftin a v) (Fin.L_R 1 k1) = nth v k2. Proof. @@ -82,11 +107,99 @@ Proof. refine (@rectS _ _ _ _); now simpl. Qed. +(** ** Properties of [replace] *) + +Lemma nth_order_replace_eq A: forall n k (v : t A n) a (H1 : k < n) (H2 : k < n), + nth_order (replace v (Fin.of_nat_lt H2) a) H1 = a. +Proof. +intros n k; revert n; induction k; intros; + (destruct n; [ inversion H1 | subst ]). +- now rewrite nth_order_hd, (eta v). +- rewrite <- (nth_order_tl _ _ _ _ (proj2 (Nat.succ_lt_mono _ _) H1)), (eta v). + apply IHk. +Qed. + +Lemma nth_order_replace_neq A: forall n k1 k2, k1 <> k2 -> + forall (v : t A n) a (H1 : k1 < n) (H2 : k2 < n), + nth_order (replace v (Fin.of_nat_lt H2) a) H1 = nth_order v H1. +Proof. +intros n k1; revert n; induction k1; intros; + (destruct n ; [ inversion H1 | subst ]). +- rewrite 2 nth_order_hd. + destruct k2; intuition. + now rewrite 2 (eta v). +- rewrite <- 2 (nth_order_tl _ _ _ _ (proj2 (Nat.succ_lt_mono _ _) H1)), (eta v). + destruct k2; auto. + apply IHk1. + intros Hk; apply H; now subst. +Qed. + +Lemma replace_id A: forall n p (v : t A n), + replace v p (nth v p) = v. +Proof. +induction p; intros; rewrite 2 (eta v); simpl; auto. +now rewrite IHp. +Qed. + +Lemma replace_replace_eq A: forall n p (v : t A n) a b, + replace (replace v p a) p b = replace v p b. +Proof. +intros. +induction p; rewrite 2 (eta v); simpl; auto. +now rewrite IHp. +Qed. + +Lemma replace_replace_neq A: forall n p1 p2 (v : t A n) a b, p1 <> p2 -> + replace (replace v p1 a) p2 b = replace (replace v p2 b) p1 a. +Proof. +apply (Fin.rect2 (fun n p1 p2 => forall v a b, + p1 <> p2 -> replace (replace v p1 a) p2 b = replace (replace v p2 b) p1 a)). +- intros n v a b Hneq. + now contradiction Hneq. +- intros n p2 v; revert n v p2. + refine (@rectS _ _ _ _); auto. +- intros n p1 v; revert n v p1. + refine (@rectS _ _ _ _); auto. +- intros n p1 p2 IH v; revert n v p1 p2 IH. + refine (@rectS _ _ _ _); simpl; do 6 intro; [ | do 3 intro ]; intro Hneq; + f_equal; apply IH; intros Heq; apply Hneq; now subst. +Qed. + +(** ** Properties of [const] *) + Lemma const_nth A (a: A) n (p: Fin.t n): (const a n)[@ p] = a. Proof. now induction p. Qed. +(** ** Properties of [map] *) + +Lemma map_id A: forall n (v : t A n), + map (fun x => x) v = v. +Proof. +induction v; simpl; [ | rewrite IHv ]; auto. +Qed. + +Lemma map_map A B C: forall (f:A->B) (g:B->C) n (v : t A n), + map g (map f v) = map (fun x => g (f x)) v. +Proof. +induction v; simpl; [ | rewrite IHv ]; auto. +Qed. + +Lemma map_ext_in A B: forall (f g:A->B) n (v : t A n), + (forall a, In a v -> f a = g a) -> map f v = map g v. +Proof. +induction v; simpl; auto. +intros; rewrite H by constructor; rewrite IHv; intuition. +apply H; now constructor. +Qed. + +Lemma map_ext A B: forall (f g:A->B), (forall a, f a = g a) -> + forall n (v : t A n), map f v = map g v. +Proof. +intros; apply map_ext_in; auto. +Qed. + Lemma nth_map {A B} (f: A -> B) {n} v (p1 p2: Fin.t n) (eq: p1 = p2): (map f v) [@ p1] = f (v [@ p2]). Proof. @@ -105,6 +218,8 @@ refine (@rect2 _ _ _ _ _); simpl. now simpl. Qed. +(** ** Properties of [fold_left] *) + Lemma fold_left_right_assoc_eq {A B} {f: A -> B -> A} (assoc: forall a b c, f (f a b) c = f (f a c) b) {n} (v: t B n): forall a, fold_left f a v = fold_right (fun x y => f y x) v a. @@ -118,6 +233,8 @@ assert (forall n h (v: t B n) a, fold_left f (f a h) v = f (fold_left f a v) h). + simpl. intros; now rewrite<- (IHv). Qed. +(** ** Properties of [to_list] *) + Lemma to_list_of_list_opp {A} (l: list A): to_list (of_list l) = l. Proof. induction l. @@ -125,6 +242,8 @@ induction l. - unfold to_list; simpl. now f_equal. Qed. +(** ** Properties of [take] *) + Lemma take_O : forall {A} {n} le (v:t A n), take 0 le v = []. Proof. reflexivity. @@ -153,10 +272,14 @@ Proof. - destruct v. inversion le. simpl. apply f_equal. apply IHp. Qed. +(** ** Properties of [uncons] and [splitat] *) + Lemma uncons_cons {A} : forall {n : nat} (a : A) (v : t A n), uncons (a::v) = (a,v). Proof. reflexivity. Qed. +(* [append] *) + Lemma append_comm_cons {A} : forall {n m : nat} (v : t A n) (w : t A m) (a : A), a :: (v ++ w) = (a :: v) ++ w. Proof. reflexivity. Qed. @@ -187,3 +310,80 @@ Proof with auto. f_equal... apply IHv... Qed. + +(** ** Properties of [Forall] and [Forall2] *) + +Lemma Forall_impl A: forall (P Q : A -> Prop), (forall a, P a -> Q a) -> + forall n (v : t A n), Forall P v -> Forall Q v. +Proof. +induction v; intros HP; constructor; inversion HP as [| ? ? ? ? ? Heq1 [Heq2 He]]; + apply (inj_pair2_eq_dec _ Nat.eq_dec) in He; subst; intuition. +Qed. + +Lemma Forall_forall A: forall P n (v : t A n), + Forall P v <-> forall a, In a v -> P a. +Proof. +intros P n v; split. +- intros HP a Hin. + revert HP; induction Hin; intros HP; + inversion HP as [| ? ? ? ? ? Heq1 [Heq2 He]]; subst; auto. + apply (inj_pair2_eq_dec _ Nat.eq_dec) in He; subst; auto. +- induction v; intros Hin; constructor. + + apply Hin; constructor. + + apply IHv; intros a Ha. + apply Hin; now constructor. +Qed. + +Lemma Forall_nth_order A: forall P n (v : t A n), + Forall P v <-> forall i (Hi : i < n), P (nth_order v Hi). +Proof. +split; induction n. +- intros HF i Hi; inversion Hi. +- intros HF i Hi. + rewrite (eta v). + rewrite (eta v) in HF. + inversion HF as [| ? ? ? ? ? Heq1 [Heq2 He]]; subst. + apply (inj_pair2_eq_dec _ Nat.eq_dec) in He ; subst. + destruct i. + + now rewrite nth_order_hd. + + rewrite <- (nth_order_tl _ _ _ _ (proj2 (Nat.succ_lt_mono _ _) Hi) Hi). + now apply IHn. +- intros HP; apply case0; constructor. +- intros HP. + rewrite (eta v) in HP. + rewrite (eta v); constructor. + + specialize HP with 0 (Nat.lt_0_succ n). + now rewrite nth_order_hd in HP. + + apply IHn; intros. + specialize HP with (S i) (proj1 (Nat.succ_lt_mono _ _) Hi). + now rewrite <- (nth_order_tl _ _ _ _ Hi) in HP. +Qed. + +Lemma Forall2_nth_order A: forall P n (v1 v2 : t A n), + Forall2 P v1 v2 + <-> forall i (Hi1 : i < n) (Hi2 : i < n), P (nth_order v1 Hi1) (nth_order v2 Hi2). +Proof. +split; induction n. +- intros HF i Hi1 Hi2; inversion Hi1. +- intros HF i Hi1 Hi2. + rewrite (eta v1), (eta v2). + rewrite (eta v1), (eta v2) in HF. + inversion HF as [| ? ? ? ? ? ? ? Heq [Heq1 He1] [Heq2 He2]]. + apply (inj_pair2_eq_dec _ Nat.eq_dec) in He1. + apply (inj_pair2_eq_dec _ Nat.eq_dec) in He2; subst. + destruct i. + + now rewrite nth_order_hd. + + rewrite <- (nth_order_tl _ _ _ _ (proj2 (Nat.succ_lt_mono _ _) Hi1) Hi1). + rewrite <- (nth_order_tl _ _ _ _ (proj2 (Nat.succ_lt_mono _ _) Hi2) Hi2). + now apply IHn. +- intros _; revert v1; apply case0; revert v2; apply case0; constructor. +- intros HP. + rewrite (eta v1), (eta v2) in HP. + rewrite (eta v1), (eta v2); constructor. + + specialize HP with 0 (Nat.lt_0_succ _) (Nat.lt_0_succ _). + now rewrite nth_order_hd in HP. + + apply IHn; intros. + specialize HP with (S i) (proj1 (Nat.succ_lt_mono _ _) Hi1) + (proj1 (Nat.succ_lt_mono _ _) Hi2). + now rewrite <- (nth_order_tl _ _ _ _ Hi1), <- (nth_order_tl _ _ _ _ Hi2) in HP. +Qed. diff --git a/theories/ltac/Ltac.v b/theories/ltac/Ltac.v deleted file mode 100644 index e69de29bb2..0000000000 --- a/theories/ltac/Ltac.v +++ /dev/null diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index d6f51d7b78..def1cbbcf8 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -821,7 +821,7 @@ module Html = struct | Some n -> if lev <= n then add_toc_entry (Toc_section (lev, f, r)) else ()); stop_item (); - printf "<a name=\"%s\"></a><h%d class=\"section\">" lab lev; + printf "<a id=\"%s\"></a><h%d class=\"section\">" lab lev; f (); printf "</h%d>\n" lev @@ -835,7 +835,7 @@ module Html = struct let letter_index category idx (c,l) = if l <> [] then begin let cat = if category && idx <> "global" then "(" ^ idx ^ ")" else "" in - printf "<a name=\"%s_%c\"></a><h2>%s %s</h2>\n" idx c (display_letter c) cat; + printf "<a id=\"%s_%c\"></a><h2>%s %s</h2>\n" idx c (display_letter c) cat; List.iter (fun (id,(text,link,t)) -> let id' = prepare_entry id t in diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index cfc89782a1..17435c051e 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -44,7 +44,6 @@ type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; indices_matter : bool; toplevel_name : Stm.interactive_top; - cumulative_sprop : bool; } type coqargs_config = { @@ -110,7 +109,6 @@ let default_logic_config = { impredicative_set = Declarations.PredicativeSet; indices_matter = false; toplevel_name = Stm.TopLogical default_toplevel; - cumulative_sprop = false; } let default_config = { @@ -198,6 +196,10 @@ let set_query opts q = | Queries queries -> Queries (queries@[q]) } +let warn_deprecated_sprop_cumul = + CWarnings.create ~name:"deprecated-spropcumul" ~category:"deprecated" + (fun () -> Pp.strbrk "Use the \"Cumulative StrictProp\" flag instead.") + let warn_deprecated_inputstate = CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.") @@ -520,7 +522,9 @@ let parse_args ~help ~init arglist : t * string list = add_set_option oval Vernacentries.allow_sprop_opt_name (OptionSet None) |"-disallow-sprop" -> add_set_option oval Vernacentries.allow_sprop_opt_name OptionUnset - |"-sprop-cumulative" -> set_logic (fun o -> { o with cumulative_sprop = true }) oval + |"-sprop-cumulative" -> + warn_deprecated_sprop_cumul(); + add_set_option oval Vernacentries.cumul_sprop_opt_name (OptionSet None) |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }} |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }} diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index 8723d21bb4..a51ed6766a 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -20,7 +20,6 @@ type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; indices_matter : bool; toplevel_name : Stm.interactive_top; - cumulative_sprop : bool; } type coqargs_config = { diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 1175494bad..7aad856d0a 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -199,7 +199,6 @@ let init_execution opts custom_init = Global.set_VM opts.config.enable_VM; Flags.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true); Global.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true); - if opts.config.logic.cumulative_sprop then Global.make_sprop_cumulative (); (* Native output dir *) Nativelib.output_dir := opts.config.native_output_dir; diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index 57d59fc2ef..13c4d667a0 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -145,10 +145,10 @@ GRAMMAR EXTEND Gram { CAst.make ~loc @@ CTacCse (e, bl) } ] | "4" LEFTA [ ] - | [ e0 = SELF; ","; el = LIST1 NEXT SEP "," -> + | "3" [ e0 = SELF; ","; el = LIST1 NEXT SEP "," -> { let el = e0 :: el in CAst.make ~loc @@ CTacApp (CAst.make ~loc @@ CTacCst (AbsKn (Tuple (List.length el))), el) } ] - | "::" RIGHTA + | "2" RIGHTA [ e1 = tac2expr; "::"; e2 = tac2expr -> { CAst.make ~loc @@ CTacApp (CAst.make ~loc @@ CTacCst (AbsKn (Other Tac2core.Core.c_cons)), [e1; e2]) } ] diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 2102cd1172..e77040a8db 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -375,7 +375,7 @@ let () = define1 "constr_kind" constr begin fun c -> | Evar (evk, args) -> v_blk 3 [| Value.of_int (Evar.repr evk); - Value.of_array Value.of_constr args; + Value.of_array Value.of_constr (Array.of_list args); |] | Sort s -> v_blk 4 [|Value.of_ext Value.val_sort s|] @@ -469,7 +469,7 @@ let () = define1 "constr_make" valexpr begin fun knd -> | (3, [|evk; args|]) -> let evk = Evar.unsafe_of_int (Value.to_int evk) in let args = Value.to_array Value.to_constr args in - EConstr.mkEvar (evk, args) + EConstr.mkEvar (evk, Array.to_list args) | (4, [|s|]) -> let s = Value.to_ext Value.val_sort s in EConstr.mkSort (EConstr.Unsafe.to_sorts s) @@ -603,7 +603,7 @@ let () = define3 "constr_in_context" ident constr closure begin fun id t c -> thaw c >>= fun _ -> Proofview.Unsafe.tclSETGOALS [Proofview.with_empty_state (Proofview.Goal.goal gl)] >>= fun () -> let args = List.map (fun d -> EConstr.mkVar (get_id d)) (EConstr.named_context env) in - let args = Array.of_list (EConstr.mkRel 1 :: args) in + let args = EConstr.mkRel 1 :: args in let ans = EConstr.mkEvar (evk, args) in let ans = EConstr.mkLambda (Context.make_annot (Name id) Sorts.Relevant, t, ans) in return (Value.of_constr ans) diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 5555a2c68e..fddc84b398 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -57,16 +57,16 @@ let contract3 env sigma a b c = match contract env sigma [a;b;c] with let contract4 env sigma a b c d = match contract env sigma [a;b;c;d] with | env, [a;b;c;d] -> (env,a,b,c),d | _ -> assert false -let contract1_vect env sigma a v = - match contract env sigma (a :: Array.to_list v) with - | env, a::l -> env,a,Array.of_list l +let contract1 env sigma a v = + match contract env sigma (a :: v) with + | env, a::l -> env,a,l | _ -> assert false let rec contract3' env sigma a b c = function | OccurCheck (evk,d) -> let x,d = contract4 env sigma a b c d in x,OccurCheck(evk, d) | NotClean ((evk,args),env',d) -> - let env',d,args = contract1_vect env' sigma d args in + let env',d,args = contract1 env' sigma d args in contract3 env sigma a b c,NotClean((evk,args),env',d) | ConversionFailed (env',t1,t2) -> let (env',t1,t2) = contract2 env' sigma t1 t2 in @@ -299,9 +299,9 @@ let explain_unification_error env sigma p1 p2 = function [str "cannot instantiate " ++ quote (pr_existential_key sigma evk) ++ strbrk " because " ++ pr_leconstr_env env sigma c ++ strbrk " is not in its scope" ++ - (if Array.is_empty args then mt() else + (if List.is_empty args then mt() else strbrk ": available arguments are " ++ - pr_sequence (pr_leconstr_env env sigma) (List.rev (Array.to_list args)))] + pr_sequence (pr_leconstr_env env sigma) (List.rev args))] | NotSameArgSize | NotSameHead | NoCanonicalStructure -> (* Error speaks from itself *) [] | ConversionFailed (env,t1,t2) -> diff --git a/vernac/retrieveObl.ml b/vernac/retrieveObl.ml index c529972b8d..b8564037e0 100644 --- a/vernac/retrieveObl.ml +++ b/vernac/retrieveObl.ml @@ -72,7 +72,7 @@ let subst_evar_constr evm evs n idf t = *) let args = let n = match chop with None -> 0 | Some c -> c in - let l, r = CList.chop n (List.rev (Array.to_list args)) in + let l, r = CList.chop n (List.rev args) in List.rev r in let args = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4958d0116e..df39c617d3 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1302,6 +1302,7 @@ let vernac_generalizable ~local = Implicit_quantifiers.declare_generalizable ~local let allow_sprop_opt_name = ["Allow";"StrictProp"] +let cumul_sprop_opt_name = ["Cumulative";"StrictProp"] let () = declare_bool_option @@ -1313,6 +1314,13 @@ let () = let () = declare_bool_option { optdepr = false; + optkey = cumul_sprop_opt_name; + optread = Global.is_cumulative_sprop; + optwrite = Global.set_cumulative_sprop } + +let () = + declare_bool_option + { optdepr = false; optkey = ["Silent"]; optread = (fun () -> !Flags.quiet); optwrite = ((:=) Flags.quiet) } @@ -1487,21 +1495,21 @@ let () = optread = CWarnings.get_flags; optwrite = CWarnings.set_flags } -let _ = +let () = declare_bool_option { optdepr = false; optkey = ["Guard"; "Checking"]; optread = (fun () -> (Global.typing_flags ()).Declarations.check_guarded); optwrite = (fun b -> Global.set_check_guarded b) } -let _ = +let () = declare_bool_option { optdepr = false; optkey = ["Positivity"; "Checking"]; optread = (fun () -> (Global.typing_flags ()).Declarations.check_positive); optwrite = (fun b -> Global.set_check_positive b) } -let _ = +let () = declare_bool_option { optdepr = false; optkey = ["Universe"; "Checking"]; diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 2ac8458ad5..cf233248d7 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -26,3 +26,4 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr val command_focus : unit Proof.focus_kind val allow_sprop_opt_name : string list +val cumul_sprop_opt_name : string list |