diff options
64 files changed, 695 insertions, 250 deletions
diff --git a/META.coq.in b/META.coq.in index 29b3ecbcb3..68ab0733ee 100644 --- a/META.coq.in +++ b/META.coq.in @@ -1,7 +1,7 @@ # TODO: Generate automatically with Dune description = "The Coq Proof Assistant Plugin API" -version = "8.13" +version = "8.14" directory = "" requires = "" @@ -9,7 +9,7 @@ requires = "" package "config" ( description = "Coq Configuration Variables" - version = "8.13" + version = "8.14" directory = "config" @@ -19,7 +19,7 @@ package "config" ( package "clib" ( description = "Base General Coq Library" - version = "8.13" + version = "8.14" directory = "clib" requires = "str, unix, threads" @@ -31,7 +31,7 @@ package "clib" ( package "lib" ( description = "Base Coq-Specific Library" - version = "8.13" + version = "8.14" directory = "lib" @@ -45,7 +45,7 @@ package "lib" ( package "vm" ( description = "Coq VM" - version = "8.13" + version = "8.14" directory = "kernel/byterun" @@ -64,7 +64,7 @@ package "vm" ( package "kernel" ( description = "Coq's Kernel" - version = "8.13" + version = "8.14" directory = "kernel" @@ -78,7 +78,7 @@ package "kernel" ( package "library" ( description = "Coq Libraries (vo) support" - version = "8.13" + version = "8.14" requires = "coq.kernel" @@ -92,7 +92,7 @@ package "library" ( package "engine" ( description = "Coq Tactic Engine" - version = "8.13" + version = "8.14" requires = "coq.library" directory = "engine" @@ -105,7 +105,7 @@ package "engine" ( package "pretyping" ( description = "Coq Pretyper" - version = "8.13" + version = "8.14" requires = "coq.engine" directory = "pretyping" @@ -118,7 +118,7 @@ package "pretyping" ( package "interp" ( description = "Coq Term Interpretation" - version = "8.13" + version = "8.14" requires = "zarith, coq.pretyping" directory = "interp" @@ -131,7 +131,7 @@ package "interp" ( package "proofs" ( description = "Coq Proof Engine" - version = "8.13" + version = "8.14" requires = "coq.interp" directory = "proofs" @@ -144,7 +144,7 @@ package "proofs" ( package "gramlib" ( description = "Coq Grammar Engine" - version = "8.13" + version = "8.14" requires = "coq.lib" directory = "gramlib/.pack" @@ -156,7 +156,7 @@ package "gramlib" ( package "parsing" ( description = "Coq Parsing Engine" - version = "8.13" + version = "8.14" requires = "coq.gramlib, coq.proofs" directory = "parsing" @@ -169,7 +169,7 @@ package "parsing" ( package "printing" ( description = "Coq Printing Engine" - version = "8.13" + version = "8.14" requires = "coq.parsing" directory = "printing" @@ -182,7 +182,7 @@ package "printing" ( package "tactics" ( description = "Coq Basic Tactics" - version = "8.13" + version = "8.14" requires = "coq.printing" directory = "tactics" @@ -195,7 +195,7 @@ package "tactics" ( package "vernac" ( description = "Coq Vernacular Interpreter" - version = "8.13" + version = "8.14" requires = "coq.tactics" directory = "vernac" @@ -208,7 +208,7 @@ package "vernac" ( package "stm" ( description = "Coq State Transactional Machine" - version = "8.13" + version = "8.14" requires = "coq.vernac" directory = "stm" @@ -221,7 +221,7 @@ package "stm" ( package "toplevel" ( description = "Coq Toplevel" - version = "8.13" + version = "8.14" requires = "coq.stm" directory = "toplevel" @@ -234,7 +234,7 @@ package "toplevel" ( package "idetop" ( description = "Coq IDE Libraries" - version = "8.13" + version = "8.14" requires = "coq.toplevel" directory = "ide" @@ -247,7 +247,7 @@ package "idetop" ( package "ide" ( description = "Coq IDE Libraries" - version = "8.13" + version = "8.14" requires = "coq.lib, coq.ideprotocol, lablgtk3, lablgtk3-sourceview3" directory = "ide" @@ -260,7 +260,7 @@ package "ide" ( package "ideprotocol" ( description = "Coq IDE protocol" - version = "8.13" + version = "8.14" requires = "coq.toplevel" directory = "ide/protocol" @@ -273,14 +273,14 @@ package "ideprotocol" ( package "plugins" ( description = "Coq built-in plugins" - version = "8.13" + version = "8.14" directory = "plugins" package "ltac" ( description = "Coq LTAC Plugin" - version = "8.13" + version = "8.14" requires = "coq.stm" directory = "ltac" @@ -295,7 +295,7 @@ package "plugins" ( package "tauto" ( description = "Coq tauto plugin" - version = "8.13" + version = "8.14" requires = "coq.plugins.ltac" directory = "ltac" @@ -310,7 +310,7 @@ package "plugins" ( package "omega" ( description = "Coq omega plugin" - version = "8.13" + version = "8.14" requires = "coq.plugins.ltac" directory = "omega" @@ -325,7 +325,7 @@ package "plugins" ( package "micromega" ( description = "Coq micromega plugin" - version = "8.13" + version = "8.14" requires = "coq.plugins.ltac" directory = "micromega" @@ -340,7 +340,7 @@ package "plugins" ( package "zify" ( description = "Coq Zify plugin" - version = "8.13" + version = "8.14" requires = "coq.plugins.ltac" directory = "micromega" @@ -355,7 +355,7 @@ package "plugins" ( package "ring" ( description = "Coq ring plugin" - version = "8.13" + version = "8.14" requires = "" directory = "ring" @@ -370,7 +370,7 @@ package "plugins" ( package "extraction" ( description = "Coq extraction plugin" - version = "8.13" + version = "8.14" requires = "coq.plugins.ltac" directory = "extraction" @@ -385,7 +385,7 @@ package "plugins" ( package "cc" ( description = "Coq cc plugin" - version = "8.13" + version = "8.14" requires = "coq.plugins.ltac" directory = "cc" @@ -400,7 +400,7 @@ package "plugins" ( package "firstorder" ( description = "Coq ground plugin" - version = "8.13" + version = "8.14" requires = "coq.plugins.ltac" directory = "firstorder" @@ -415,7 +415,7 @@ package "plugins" ( package "rtauto" ( description = "Coq rtauto plugin" - version = "8.13" + version = "8.14" requires = "coq.plugins.ltac" directory = "rtauto" @@ -430,7 +430,7 @@ package "plugins" ( package "btauto" ( description = "Coq btauto plugin" - version = "8.13" + version = "8.14" requires = "coq.plugins.ltac" directory = "btauto" @@ -445,7 +445,7 @@ package "plugins" ( package "funind" ( description = "Coq recdef plugin" - version = "8.13" + version = "8.14" requires = "coq.plugins.extraction" directory = "funind" @@ -460,7 +460,7 @@ package "plugins" ( package "nsatz" ( description = "Coq nsatz plugin" - version = "8.13" + version = "8.14" requires = "zarith, coq.plugins.ltac" directory = "nsatz" @@ -475,7 +475,7 @@ package "plugins" ( package "rsyntax" ( description = "Coq rsyntax plugin" - version = "8.13" + version = "8.14" requires = "" directory = "syntax" @@ -490,7 +490,7 @@ package "plugins" ( package "int63syntax" ( description = "Coq int63syntax plugin" - version = "8.13" + version = "8.14" requires = "" directory = "syntax" @@ -505,7 +505,7 @@ package "plugins" ( package "string_notation" ( description = "Coq string_notation plugin" - version = "8.13" + version = "8.14" requires = "coq.vernac" directory = "syntax" @@ -519,7 +519,7 @@ package "plugins" ( package "numeral_notation" ( description = "Coq numeral notation plugin" - version = "8.13" + version = "8.14" requires = "coq.vernac" directory = "numeral_notation" @@ -534,7 +534,7 @@ package "plugins" ( package "derive" ( description = "Coq derive plugin" - version = "8.13" + version = "8.14" requires = "" directory = "derive" @@ -549,7 +549,7 @@ package "plugins" ( package "ssrmatching" ( description = "Coq ssrmatching plugin" - version = "8.13" + version = "8.14" requires = "coq.plugins.ltac" directory = "ssrmatching" @@ -564,7 +564,7 @@ package "plugins" ( package "ssreflect" ( description = "Coq ssreflect plugin" - version = "8.13" + version = "8.14" requires = "coq.plugins.ssrmatching" directory = "ssr" @@ -579,7 +579,7 @@ package "plugins" ( package "ltac2" ( description = "Coq Ltac2 Plugin" - version = "8.13" + version = "8.14" requires = "coq.plugins.ltac" directory = "../user-contrib/Ltac2" diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 809b6f87a9..11f225bdb6 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -90,11 +90,11 @@ jobs: make -j "$NJOBS" displayName: 'Build Coq' -# - script: | -# eval $(opam env) -# export OCAMLPATH=$(pwd):"$OCAMLPATH" -# make -j "$NJOBS" test-suite PRINT_LOGS=1 -# displayName: 'Run Coq Test Suite' + - script: | + eval $(opam env) + export OCAMLPATH=$(pwd):"$OCAMLPATH" + make -j "$NJOBS" test-suite PRINT_LOGS=1 + displayName: 'Run Coq Test Suite' - script: | make install diff --git a/configure.ml b/configure.ml index e32f780a3d..40d77ed109 100644 --- a/configure.ml +++ b/configure.ml @@ -12,11 +12,11 @@ #load "str.cma" open Printf -let coq_version = "8.13+alpha" -let coq_macos_version = "8.12.90" (** "[...] should be a string comprised of +let coq_version = "8.14+alpha" +let coq_macos_version = "8.13.90" (** "[...] should be a string comprised of three non-negative, period-separated integers [...]" *) -let vo_magic = 81291 -let state_magic = 581291 +let vo_magic = 81391 +let state_magic = 581391 let is_a_released_version = false let distributed_exec = ["coqtop.opt"; "coqidetop.opt"; "coqqueryworker.opt"; "coqproofworker.opt"; "coqtacticworker.opt"; diff --git a/default.nix b/default.nix index 7f9e62b28c..0b23bdb48c 100644 --- a/default.nix +++ b/default.nix @@ -29,7 +29,7 @@ , shell ? false # We don't use lib.inNixShell because that would also apply # when in a nix-shell of some package depending on this one. -, coq-version ? "8.13-git" +, coq-version ? "8.14-git" }: with pkgs; diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index da9f37f666..9b43bddd86 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -80,6 +80,9 @@ in time. exists, a branch dedicated to compatibility with the corresponding Coq branch). You can use the `dev/tools/pin-ci.sh` script to do this semi-automatically. + - [ ] Notify upstream authors about the pinning, see + `dev/tools/notify-upstream-pins.sh`. As of today there is no automated + way to track these issues. - [ ] Remove all remaining unmerged feature PRs from the beta milestone. - [ ] Start a new project to track PR backporting. The project should have a "Request X.X+beta1 inclusion" column for the PRs that were diff --git a/dev/tools/notify-upstream-pins.sh b/dev/tools/notify-upstream-pins.sh new file mode 100755 index 0000000000..37fe0cbcbf --- /dev/null +++ b/dev/tools/notify-upstream-pins.sh @@ -0,0 +1,116 @@ + +#!/usr/bin/env bash + +# Script to notify upstreams that we need a tag to put in a platform/installer + +VERSION="8.13" +DATEBETA="December 7, 2020" +DATEFINAL="January 7, 2020" +CC="CC: https://github.com/coq/coq/issues/12334" +#CC="\n@coqbot column:...." +REASON="bundled in the Windows installer" +#REASON="bundled in the Coq platform" + +git show master:dev/ci/ci-basic-overlay.sh > /tmp/master-ci-basic-overlay.sh +git show v${VERSION}:dev/ci/ci-basic-overlay.sh > /tmp/branch-ci-basic-overlay.sh + +# caveats: +# - dev/ci/gitlab.bat has \r (windows) +# - aactactics, gappa, HB, extlib have different names in ci +# - menhir is not pinned but figures as an addon +# - unicoq is not an addon +WINDOWS_ADDONS=$(grep addon= dev/ci/gitlab.bat \ + | cut -d = -f 2 \ + | cut -d ' ' -f 1 \ + | tr -d '\r' \ + | sed -e 's/^aactactics$/aac_tactics/' \ + -e 's/^gappa$/gappa_plugin/' \ + -e 's/^HB$/elpi_hb/' \ + -e 's/^extlib$/ext_lib/' \ + \ + -e '/^menhir$/d' \ + ) \ +WINDOWS_ADDONS="$WINDOWS_ADDONS unicoq" + +# reads a variable value from a ci-basic-overlay.sh file +function read_from() { + ( . $1; varname="$2"; echo ${!varname} ) +} + +# https://gist.github.com/cdown/1163649 +function urlencode() { + # urlencode <string> + + old_lc_collate=$LC_COLLATE + LC_COLLATE=C + + local length="${#1}" + for (( i = 0; i < length; i++ )); do + local c="${1:$i:1}" + case $c in + [a-zA-Z0-9.~_-]) printf '%s' "$c" ;; + *) printf '%%%02X' "'$c" ;; + esac + done + + LC_COLLATE=$old_lc_collate +} + +function template { + TITLE="Please create a tag for the upcoming release of Coq $VERSION" + BODY="The Coq team is planning to release Coq $VERSION-beta1 on $DATEBETA, +and Coq $VERSION.0 on $DATEFINAL. + +Your project is currently scheduled for being $REASON. + +We are currently testing commit $3 +on branch $1/tree/$2 +but we would like to ship a released version instead (a tag in git's slang). + +Could you please tag that commit, or communicate us any other tag +that works with the Coq branch v$VERSION at the *latest* 15 days before the +date of the final release? + +Thanks! +$CC +" + UUTITLE=$(urlencode "$TITLE") + UUBODY=$(urlencode "$BODY") + + case $1 in + ( http*github.com* ) + echo "$1/issues/new?title=$UUTITLE&body=$UUBODY" + ;; + ( http*gitlab* ) + echo "$1/-/issues/new" + echo + echo -e "$TITLE" + echo + echo -e "$BODY" + ;; + ( * ) + echo "$1" + echo + echo -e "$TITLE" + echo + echo -e "$BODY" + + ;; + esac +} + +for addon in $WINDOWS_ADDONS; do + URL=`read_from /tmp/master-ci-basic-overlay.sh "${addon}_CI_GITURL"` + REF=`read_from /tmp/master-ci-basic-overlay.sh "${addon}_CI_REF"` + PIN=`read_from /tmp/branch-ci-basic-overlay.sh "${addon}_CI_REF"` + if [ "${#PIN}" = "40" ]; then + echo -e "Addon $addon is pinned to a hash, to open an issue open the following url:\n" + template $URL $REF $PIN + elif [ "${#PIN}" = "0" ]; then + echo "Addon $addon has no pin!" + exit 1 + else + echo "Addon $addon is already pinned to version $PIN" + fi + echo -e "\n----------------------------------------------" +done diff --git a/doc/changelog/04-tactics/12993-remove-cutrewrite.rst b/doc/changelog/04-tactics/12993-remove-cutrewrite.rst deleted file mode 100644 index b719c5618e..0000000000 --- a/doc/changelog/04-tactics/12993-remove-cutrewrite.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Removed:** - Deprecated ``cutrewrite`` tactic. Use :tacn:`replace` instead - (`#12993 <https://github.com/coq/coq/pull/12993>`_, - by Théo Zimmermann). diff --git a/doc/changelog/06-ssreflect/13473-test_pred.rst b/doc/changelog/06-ssreflect/13473-test_pred.rst new file mode 100644 index 0000000000..3c7df11540 --- /dev/null +++ b/doc/changelog/06-ssreflect/13473-test_pred.rst @@ -0,0 +1,4 @@ +- **Added:** + Adding a test that the notations `{in _, _}` and `{pred _}` from `ssrbool.v` are displayed correctly. + (`#13473 <https://github.com/coq/coq/pull/13473>`_, + by Cyril Cohen). diff --git a/doc/changelog/12-misc/12586-declare+typing_flags.rst b/doc/changelog/12-misc/12586-declare+typing_flags.rst new file mode 100644 index 0000000000..52915ceee9 --- /dev/null +++ b/doc/changelog/12-misc/12586-declare+typing_flags.rst @@ -0,0 +1,6 @@ +- **Added:** + Typing flags can now be specified per-constant / inductive, this + allows to fine-grain specify them from plugins or attributes. See + :ref:`controlling-typing-flags` for details on attribute syntax. + (`#12586 <https://github.com/coq/coq/pull/12586>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst index 43bbc8b40d..cf46580bdb 100644 --- a/doc/sphinx/language/core/coinductive.rst +++ b/doc/sphinx/language/core/coinductive.rst @@ -27,7 +27,8 @@ More information on co-inductive definitions can be found in This command supports the :attr:`universes(polymorphic)`, :attr:`universes(template)`, :attr:`universes(cumulative)`, - :attr:`private(matching)`, and :attr:`using` attributes. + :attr:`private(matching)`, :attr:`bypass_check(universes)`, + :attr:`bypass_check(positivity)`, and :attr:`using` attributes. .. example:: diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index 57771c9036..ec5b896dab 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -90,8 +90,9 @@ Section :ref:`typing-rules`. computation on :n:`@term`. These commands also support the :attr:`universes(polymorphic)`, - :attr:`program` (see :ref:`program_definition`), - :attr:`canonical` and :attr:`using` attributes. + :attr:`program` (see :ref:`program_definition`), :attr:`canonical`, + :attr:`bypass_check(universes)`, :attr:`bypass_check(guard)`, and + :attr:`using` attributes. If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. @@ -162,7 +163,8 @@ Chapter :ref:`Tactics`. The basic assertion command is: correct at some time of the interactive development of a proof, use the command :cmd:`Guarded`. - This command accepts the :attr:`using` attribute. + This command accepts the :attr:`bypass_check(universes)`, + :attr:`bypass_check(guard)`, and :attr:`using` attributes. .. exn:: The term @term has type @type which should be Set, Prop or Type. :undocumented: @@ -173,7 +175,8 @@ Chapter :ref:`Tactics`. The basic assertion command is: The name you provided is already defined. You have then to choose another name. - .. exn:: Nested proofs are not allowed unless you turn the Nested Proofs Allowed flag on. + .. exn:: Nested proofs are discouraged and not allowed by default. This error probably means that you forgot to close the last "Proof." with "Qed." or "Defined.". \ + If you really intended to use nested proofs, you can do so by turning the "Nested Proofs Allowed" flag on. You are asserting a new statement while already being in proof editing mode. This feature, called nested proofs, is disabled by default. diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 9fda2ab1fa..4bee7cc1b1 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -31,7 +31,8 @@ Inductive types proposition). This command supports the :attr:`universes(polymorphic)`, - :attr:`universes(template)`, :attr:`universes(cumulative)`, and + :attr:`universes(template)`, :attr:`universes(cumulative)`, + :attr:`bypass_check(positivity)`, :attr:`bypass_check(universes)`, and :attr:`private(matching)` attributes. Mutually inductive types can be defined by including multiple :n:`@inductive_definition`\s. @@ -49,10 +50,12 @@ Inductive types .. exn:: Non strictly positive occurrence of @ident in @type. - The types of the constructors have to satisfy a *positivity condition* - (see Section :ref:`positivity`). This condition ensures the soundness of - the inductive definition. The positivity checking can be disabled using - the :flag:`Positivity Checking` flag (see :ref:`controlling-typing-flags`). + The types of the constructors have to satisfy a *positivity + condition* (see Section :ref:`positivity`). This condition + ensures the soundness of the inductive definition. + Positivity checking can be disabled using the :flag:`Positivity + Checking` flag or the :attr:`bypass_check(positivity)` attribute (see + :ref:`controlling-typing-flags`). .. exn:: The conclusion of @type is not valid; it must be built from @ident. @@ -390,7 +393,8 @@ constructions. consequently :n:`forall {* @binder }, @type` and its value is equivalent to :n:`fun {* @binder } => @term`. - This command accepts the :attr:`program` attribute. + This command accepts the :attr:`program`, + :attr:`bypass_check(universes)`, and :attr:`bypass_check(guard)` attributes. To be accepted, a :cmd:`Fixpoint` definition has to satisfy syntactical constraints on a special argument called the decreasing argument. They @@ -848,9 +852,7 @@ between universes for inductive types in the Type hierarchy. .. coqtop:: none - Unset Positivity Checking. - Inductive I : Prop := not_I_I (not_I : I -> False) : I. - Set Positivity Checking. + #[bypass_check(positivity)] Inductive I : Prop := not_I_I (not_I : I -> False) : I. .. coqtop:: all @@ -884,9 +886,7 @@ between universes for inductive types in the Type hierarchy. .. coqtop:: none - Unset Positivity Checking. - Inductive Lam := lam (_ : Lam -> Lam). - Set Positivity Checking. + #[bypass_check(positivity)] Inductive Lam := lam (_ : Lam -> Lam). .. coqtop:: all @@ -915,9 +915,7 @@ between universes for inductive types in the Type hierarchy. .. coqtop:: none - Unset Positivity Checking. - Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A. - Set Positivity Checking. + #[bypass_check(positivity)] Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A. .. coqtop:: all diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst index 2460461ede..95c5914e47 100644 --- a/doc/sphinx/language/extensions/arguments-command.rst +++ b/doc/sphinx/language/extensions/arguments-command.rst @@ -89,11 +89,25 @@ Setting properties of a function's arguments The construct :n:`@name {? % @scope }` declares :n:`@name` as non-implicit if `clear implicits` is specified or at least one other name is declared implicit in the same list of :n:`@name`\s. :token:`scope` can be either a scope name or its delimiting key. See :ref:`binding_to_scope`. + .. exn:: To rename arguments the 'rename' flag must be specified. + :undocumented: + + .. exn:: Flag 'rename' expected to rename @name into @name. + :undocumented: + `clear implicits` makes all implicit arguments into explicit arguments + + .. exn:: The 'clear implicits' flag must be omitted if implicit annotations are given. + :undocumented: + `default implicits` automatically determine the implicit arguments of the object. See :ref:`auto_decl_implicit_args`. + + .. exn:: The 'default implicits' flag is incompatible with implicit annotations. + :undocumented: + `rename` rename implicit arguments for the object. See the example :ref:`here <renaming_implicit_arguments>`. `assert` diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index e7db9cfaca..e866e4c624 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1152,6 +1152,12 @@ Controlling Typing Flags anymore but it still affects the reduction of the term. Unchecked fixpoints are printed by :cmd:`Print Assumptions`. +.. attr:: bypass_check(guard{? = {| yes | no } }) + :name: bypass_check(guard) + + Similar to :flag:`Guard Checking`, but on a per-declaration + basis. Disable guard checking locally with ``bypass_check(guard)``. + .. flag:: Positivity Checking This flag can be used to enable/disable the positivity checking of inductive @@ -1159,6 +1165,12 @@ Controlling Typing Flags break the consistency of the system, use at your own risk. Unchecked (co)inductive types are printed by :cmd:`Print Assumptions`. +.. attr:: bypass_check(positivity{? = {| yes | no } }) + :name: bypass_check(positivity) + + Similar to :flag:`Positivity Checking`, but on a per-declaration basis. + Disable positivity checking locally with ``bypass_check(positivity)``. + .. flag:: Universe Checking This flag can be used to enable/disable the checking of universes, providing a @@ -1167,6 +1179,12 @@ Controlling Typing Flags :cmd:`Print Assumptions`. It has the same effect as `-type-in-type` command line argument (see :ref:`command-line-options`). +.. attr:: bypass_check(universes{? = {| yes | no } }) + :name: bypass_check(universes) + + Similar to :flag:`Universe Checking`, but on a per-declaration basis. + Disable universe checking locally with ``bypass_check(universes)``. + .. cmd:: Print Typing Flags Print the status of the three typing flags: guard checking, positivity checking diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index 2de6b2a18c..b7f2927000 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -146,6 +146,13 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. only in the conclusion of the goal. The clause argument must not contain any ``type of`` nor ``value of``. + .. tacv:: cutrewrite {? {| <- | -> } } (@term__1 = @term__2) {? in @ident } + :name: cutrewrite + + .. deprecated:: 8.5 + + Use :tacn:`replace` instead. + .. tacn:: subst @ident :name: subst diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 7201dc6a0e..8ab4265b15 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -709,6 +709,7 @@ through the <tt>Require Import</tt> command.</p> theories/Compat/Coq811.v theories/Compat/Coq812.v theories/Compat/Coq813.v + theories/Compat/Coq814.v </dd> <dt> <b>Array</b>: diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 8efda825de..75b3260166 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1021,6 +1021,9 @@ simple_tactic: [ | DELETE "unify" constr constr | REPLACE "unify" constr constr "with" preident | WITH "unify" constr constr OPT ( "with" preident ) +| DELETE "cutrewrite" orient constr +| REPLACE "cutrewrite" orient constr "in" hyp +| WITH "cutrewrite" orient constr OPT ( "in" hyp ) | DELETE "destauto" | REPLACE "destauto" "in" hyp | WITH "destauto" OPT ( "in" hyp ) diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index cf90eea5a1..ccf38d2c15 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1583,6 +1583,8 @@ simple_tactic: [ | "simple" "injection" destruction_arg | "dependent" "rewrite" orient constr | "dependent" "rewrite" orient constr "in" hyp +| "cutrewrite" orient constr +| "cutrewrite" orient constr "in" hyp | "decompose" "sum" constr | "decompose" "record" constr | "absurd" constr diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 7c709baa48..d950b32160 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1685,6 +1685,7 @@ simple_tactic: [ | "einjection" OPT destruction_arg OPT ( "as" LIST0 simple_intropattern ) | "simple" "injection" OPT destruction_arg | "dependent" "rewrite" OPT [ "->" | "<-" ] one_term OPT ( "in" ident ) +| "cutrewrite" OPT [ "->" | "<-" ] one_term OPT ( "in" ident ) | "decompose" "sum" one_term | "decompose" "record" one_term | "absurd" one_term diff --git a/kernel/environ.ml b/kernel/environ.ml index 69edb1498c..a5f81d1e59 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -479,6 +479,9 @@ let set_typing_flags c env = let env = set_type_in_type (not c.check_universes) env in env +let update_typing_flags ?typing_flags env = + Option.cata (fun flags -> set_typing_flags flags env) env typing_flags + let set_cumulative_sprop b env = set_typing_flags {env.env_typing_flags with cumulative_sprop=b} env diff --git a/kernel/environ.mli b/kernel/environ.mli index 6a8ddce835..900e2128ea 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -351,6 +351,9 @@ val set_type_in_type : bool -> env -> env val set_allow_sprop : bool -> env -> env val sprop_allowed : env -> bool +(** [update_typing_flags ?typing_flags] may update env with optional typing flags *) +val update_typing_flags : ?typing_flags:typing_flags -> env -> env + val universes_of_global : env -> GlobRef.t -> AUContext.t (** {6 Sets of referred section variables } diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 6abd283f6c..a35f94e3ce 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -247,6 +247,15 @@ let set_native_compiler b senv = let set_allow_sprop b senv = { senv with env = Environ.set_allow_sprop b senv.env } +(* Temporary sets custom typing flags *) +let with_typing_flags ?typing_flags senv ~f = + match typing_flags with + | None -> f senv + | Some typing_flags -> + let orig_typing_flags = Environ.typing_flags senv.env in + let res, senv = f (set_typing_flags typing_flags senv) in + res, set_typing_flags orig_typing_flags senv + (** Check that the engagement [c] expected by a library matches the current (initial) one *) let check_engagement env expected_impredicative_set = @@ -928,6 +937,9 @@ let add_constant l decl senv = in kn, senv +let add_constant ?typing_flags l decl senv = + with_typing_flags ?typing_flags senv ~f:(add_constant l decl) + let add_private_constant l decl senv : (Constant.t * private_constants) * safe_environment = let kn = Constant.make2 senv.modpath l in let cb = @@ -983,6 +995,9 @@ let add_mind l mie senv = let mib = Indtypes.check_inductive senv.env ~sec_univs kn mie in kn, add_checked_mind kn mib senv +let add_mind ?typing_flags l mie senv = + with_typing_flags ?typing_flags senv ~f:(add_mind l mie) + (** Insertion of module types *) let add_modtype l params_mte inl senv = diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 6fa9022906..287274e39a 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -93,6 +93,7 @@ val export_private_constants : (** returns the main constant *) val add_constant : + ?typing_flags:Declarations.typing_flags -> Label.t -> global_declaration -> Constant.t safe_transformer (** Similar to add_constant but also returns a certificate *) @@ -102,6 +103,7 @@ val add_private_constant : (** Adding an inductive type *) val add_mind : + ?typing_flags:Declarations.typing_flags -> Label.t -> Entries.mutual_inductive_entry -> MutInd.t safe_transformer diff --git a/library/global.ml b/library/global.ml index 5c847fda96..71cadb3600 100644 --- a/library/global.ml +++ b/library/global.ml @@ -105,9 +105,9 @@ 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) -let add_constant id d = globalize (Safe_typing.add_constant (i2l id) d) +let add_constant ?typing_flags id d = globalize (Safe_typing.add_constant ?typing_flags (i2l id) d) let add_private_constant id d = globalize (Safe_typing.add_private_constant (i2l id) d) -let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie) +let add_mind ?typing_flags id mie = globalize (Safe_typing.add_mind ?typing_flags (i2l id) mie) let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl) let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl) diff --git a/library/global.mli b/library/global.mli index 5faf0e8bbd..c9b9d7f536 100644 --- a/library/global.mli +++ b/library/global.mli @@ -52,10 +52,12 @@ val export_private_constants : Safe_typing.exported_private_constant list val add_constant : + ?typing_flags:Declarations.typing_flags -> Id.t -> Safe_typing.global_declaration -> Constant.t val add_private_constant : Id.t -> Safe_typing.side_effect_declaration -> Constant.t * Safe_typing.private_constants val add_mind : + ?typing_flags:Declarations.typing_flags -> Id.t -> Entries.mutual_inductive_entry -> MutInd.t (** Extra universe constraints *) diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 6ab82b1253..0b5d36b845 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -41,7 +41,7 @@ DECLARE PLUGIN "ltac_plugin" (**********************************************************************) (* replace, discriminate, injection, simplify_eq *) -(* dependent rewrite *) +(* cutrewrite, dependent rewrite *) let with_delayed_uconstr ist c tac = let flags = { @@ -201,6 +201,12 @@ TACTIC EXTEND dependent_rewrite -> { rewriteInHyp b c id } END +TACTIC EXTEND cut_rewrite +| [ "cutrewrite" orient(b) constr(eqn) ] -> { cutRewriteInConcl b eqn } +| [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ] + -> { cutRewriteInHyp b eqn id } +END + (**********************************************************************) (* Decompose *) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index cdf2922516..d0b724b755 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -448,6 +448,58 @@ let compare_cumulative_instances evd variances u u' = Success evd | Inr p -> UnifFailure (evd, UnifUnivInconsistency p) +let compare_heads env evd ~nargs term term' = + let check_strict evd u u' = + let cstrs = Univ.enforce_eq_instances u u' Univ.Constraint.empty in + try Success (Evd.add_constraints evd cstrs) + with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p) + in + match EConstr.kind evd term, EConstr.kind evd term' with + | Const (c, u), Const (c', u') when QConstant.equal env c c' -> + if Int.equal nargs 1 && Environ.is_array_type env c + then + let u = EInstance.kind evd u and u' = EInstance.kind evd u' in + compare_cumulative_instances evd [|Univ.Variance.Irrelevant|] u u' + else + let u = EInstance.kind evd u and u' = EInstance.kind evd u' in + check_strict evd u u' + | Const _, Const _ -> UnifFailure (evd, NotSameHead) + | Ind ((mi,i) as ind , u), Ind (ind', u') when Names.Ind.CanOrd.equal ind ind' -> + if EInstance.is_empty u && EInstance.is_empty u' then Success evd + else + let u = EInstance.kind evd u and u' = EInstance.kind evd u' in + let mind = Environ.lookup_mind mi env in + let open Declarations in + begin match mind.mind_variance with + | None -> check_strict evd u u' + | Some variances -> + let needed = Reduction.inductive_cumulativity_arguments (mind,i) in + if not (Int.equal nargs needed) + then check_strict evd u u' + else + compare_cumulative_instances evd variances u u' + end + | Ind _, Ind _ -> UnifFailure (evd, NotSameHead) + | Construct (((mi,ind),ctor as cons), u), Construct (cons', u') + when Names.Construct.CanOrd.equal cons cons' -> + if EInstance.is_empty u && EInstance.is_empty u' then Success evd + else + let u = EInstance.kind evd u and u' = EInstance.kind evd u' in + let mind = Environ.lookup_mind mi env in + let open Declarations in + begin match mind.mind_variance with + | None -> check_strict evd u u' + | Some variances -> + let needed = Reduction.constructor_cumulativity_arguments (mind,ind,ctor) in + if not (Int.equal nargs needed) + then check_strict evd u u' + else + Success (compare_constructor_instances evd u u') + end + | Construct _, Construct _ -> UnifFailure (evd, NotSameHead) + | _, _ -> anomaly (Pp.str "") + + let conv_fun f flags on_types = let typefn env evd pbty term1 term2 = let flags = { (default_flags env) with @@ -556,65 +608,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty else evar_eqappr_x flags env' evd CONV out2 out1 in let rigids env evd sk term sk' term' = - let check_strict evd u u' = - let cstrs = Univ.enforce_eq_instances u u' Univ.Constraint.empty in - try Success (Evd.add_constraints evd cstrs) - with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p) - in - let compare_heads evd = - match EConstr.kind evd term, EConstr.kind evd term' with - | Const (c, u), Const (c', u') when QConstant.equal env c c' -> - if Int.equal (Stack.args_size sk) 1 && Environ.is_array_type env c - then - let u = EInstance.kind evd u and u' = EInstance.kind evd u' in - compare_cumulative_instances evd [|Univ.Variance.Irrelevant|] u u' - else - let u = EInstance.kind evd u and u' = EInstance.kind evd u' in - check_strict evd u u' - | Const _, Const _ -> UnifFailure (evd, NotSameHead) - | Ind ((mi,i) as ind , u), Ind (ind', u') when Names.Ind.CanOrd.equal ind ind' -> - if EInstance.is_empty u && EInstance.is_empty u' then Success evd - else - let u = EInstance.kind evd u and u' = EInstance.kind evd u' in - let mind = Environ.lookup_mind mi env in - let open Declarations in - begin match mind.mind_variance with - | None -> check_strict evd u u' - | Some variances -> - let nparamsaplied = Stack.args_size sk in - let nparamsaplied' = Stack.args_size sk' in - let needed = Reduction.inductive_cumulativity_arguments (mind,i) in - if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed) - then check_strict evd u u' - else - compare_cumulative_instances evd variances u u' - end - | Ind _, Ind _ -> UnifFailure (evd, NotSameHead) - | Construct (((mi,ind),ctor as cons), u), Construct (cons', u') - when Names.Construct.CanOrd.equal cons cons' -> - if EInstance.is_empty u && EInstance.is_empty u' then Success evd - else - let u = EInstance.kind evd u and u' = EInstance.kind evd u' in - let mind = Environ.lookup_mind mi env in - let open Declarations in - begin match mind.mind_variance with - | None -> check_strict evd u u' - | Some variances -> - let nparamsaplied = Stack.args_size sk in - let nparamsaplied' = Stack.args_size sk' in - let needed = Reduction.constructor_cumulativity_arguments (mind,ind,ctor) in - if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed) - then check_strict evd u u' - else - Success (compare_constructor_instances evd u u') - end - | Construct _, Construct _ -> UnifFailure (evd, NotSameHead) - | _, _ -> anomaly (Pp.str "") - in - ise_and evd [(fun i -> - try compare_heads i - with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); - (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk sk')] + let nargs = Stack.args_size sk in + let nargs' = Stack.args_size sk' in + if not (Int.equal nargs nargs') then UnifFailure (evd, NotSameArgSize) + else + ise_and evd [(fun i -> + try compare_heads env i ~nargs term term' + with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); + (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk sk')] in let consume on_left (_, skF as apprF) (_,skM as apprM) i = if not (Stack.is_empty skF && Stack.is_empty skM) then diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index a5a8d1f916..be03ced7eb 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -84,6 +84,12 @@ val check_conv_record : env -> evar_map -> (constr Stack.t * constr Stack.t) * constr * (int option * constr) +(** Compares two constants/inductives/constructors unifying their universes. + It required the number of arguments applied to the c/i/c in order to decided + the kind of check it must perform. *) +val compare_heads : env -> evar_map -> + nargs:int -> EConstr.t -> EConstr.t -> Evarsolve.unification_result + (** Try to solve problems of the form ?x[args] = c by second-order matching, using typing to select occurrences *) diff --git a/proofs/proof.ml b/proofs/proof.ml index 24f3ac3f29..50a0e63700 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -115,6 +115,7 @@ type t = (** the name of the theorem whose proof is being constructed *) ; poly : bool (** polymorphism *) + ; typing_flags : Declarations.typing_flags option } (*** General proof functions ***) @@ -278,7 +279,7 @@ let end_of_stack = CondEndStack end_of_stack_kind let unfocused = is_last_focus end_of_stack_kind -let start ~name ~poly sigma goals = +let start ~name ~poly ?typing_flags sigma goals = let entry, proofview = Proofview.init sigma goals in let pr = { proofview @@ -286,10 +287,11 @@ let start ~name ~poly sigma goals = ; focus_stack = [] ; name ; poly + ; typing_flags } in _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr -let dependent_start ~name ~poly goals = +let dependent_start ~name ~poly ?typing_flags goals = let entry, proofview = Proofview.dependent_init goals in let pr = { proofview @@ -297,6 +299,7 @@ let dependent_start ~name ~poly goals = ; focus_stack = [] ; name ; poly + ; typing_flags } in let number_of_goals = List.length (Proofview.initial_goals pr.entry) in _focus end_of_stack (Obj.repr ()) 1 number_of_goals pr @@ -560,6 +563,7 @@ let solve ?with_end_tac gi info_lvl tac pr = else tac in let env = Global.env () in + let env = Environ.update_typing_flags ?typing_flags:pr.typing_flags env in let (p,(status,info),()) = run_tactic env tac pr in let env = Global.env () in let sigma = Evd.from_env env in diff --git a/proofs/proof.mli b/proofs/proof.mli index f487595dac..a527820c7a 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -55,11 +55,13 @@ val data : t -> data val start : name:Names.Id.t -> poly:bool + -> ?typing_flags:Declarations.typing_flags -> Evd.evar_map -> (Environ.env * EConstr.types) list -> t val dependent_start : name:Names.Id.t -> poly:bool + -> ?typing_flags:Declarations.typing_flags -> Proofview.telescope -> t (* Returns [true] if the considered proof is completed, that is if no goal remain diff --git a/stm/stm.ml b/stm/stm.ml index f7d66b7b53..1c06c1efb7 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2681,8 +2681,10 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) | VtStartProof (guarantee, names) -> if not (get_allow_nested_proofs ()) && VCS.proof_nesting () > 0 then - "Nested proofs are not allowed unless you turn the Nested Proofs Allowed flag on." - |> Pp.str + "Nested proofs are discouraged and not allowed by default. \ + This error probably means that you forgot to close the last \"Proof.\" with \"Qed.\" or \"Defined.\". \ + If you really intended to use nested proofs, you can do so by turning the \"Nested Proofs Allowed\" flag on." + |> Pp.strbrk |> (fun s -> (UserError (None, s), Exninfo.null)) |> State.exn_on ~valid:Stateid.dummy newtip |> Exninfo.iraise diff --git a/tactics/equality.ml b/tactics/equality.ml index 486575d229..fcdd23a9c1 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1655,6 +1655,17 @@ let cutSubstClause l2r eqn cls = | None -> cutSubstInConcl l2r eqn | Some id -> cutSubstInHyp l2r eqn id +let warn_deprecated_cutrewrite = + CWarnings.create ~name:"deprecated-cutrewrite" ~category:"deprecated" + (fun () -> strbrk"\"cutrewrite\" is deprecated. Use \"replace\" instead.") + +let cutRewriteClause l2r eqn cls = + warn_deprecated_cutrewrite (); + try_rewrite (cutSubstClause l2r eqn cls) + +let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id) +let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None + let substClause l2r c cls = Proofview.Goal.enter begin fun gl -> let eq = pf_apply get_type_of gl c in diff --git a/tactics/equality.mli b/tactics/equality.mli index 5a4fe47cab..fdcbbc0e3c 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -107,6 +107,10 @@ val dEqThen : keep_proofs:(bool option) -> evars_flag -> (clear_flag -> constr - val make_iterated_tuple : env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr) +(* The family cutRewriteIn expect an equality statement *) +val cutRewriteInHyp : bool -> types -> Id.t -> unit Proofview.tactic +val cutRewriteInConcl : bool -> constr -> unit Proofview.tactic + (* The family rewriteIn expect the proof of an equality *) val rewriteInHyp : bool -> constr -> Id.t -> unit Proofview.tactic val rewriteInConcl : bool -> constr -> unit Proofview.tactic diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 24aa178ed2..68afd9a128 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -727,6 +727,32 @@ module New = struct let (loc,_) = evi.Evd.evar_source in Pretype_errors.error_unsolvable_implicit ?loc env sigma evk None + let tclMAPDELAYEDWITHHOLES accept_unresolved_holes l tac = + let rec aux = function + | [] -> tclUNIT () + | x :: l -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma_initial = Proofview.Goal.sigma gl in + let (sigma, x) = x env sigma_initial in + Proofview.Unsafe.tclEVARS sigma <*> tac x >>= fun () -> aux l >>= fun () -> + if accept_unresolved_holes then + tclUNIT () + else + tclEVARMAP >>= fun sigma_final -> + try + let () = check_evars env sigma_final sigma sigma_initial in + tclUNIT () + with e when CErrors.noncritical e -> + let e, info = Exninfo.capture e in + tclZERO ~info e + end in + aux l + + (* The following is basically + tclMAPDELAYEDWITHHOLES accept_unresolved_holes [fun _ _ -> (sigma,())] (fun () -> tac) + but with value not necessarily in unit *) + let tclWITHHOLES accept_unresolved_holes tac sigma = tclEVARMAP >>= fun sigma_initial -> if sigma == sigma_initial then tac diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index e97c5f3c1f..19d08dcc36 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -209,6 +209,10 @@ module New : sig val tclSELECT : Goal_select.t -> 'a tactic -> 'a tactic val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic + val tclMAPDELAYEDWITHHOLES : bool -> 'a delayed_open list -> ('a -> unit tactic) -> unit tactic + (* in [tclMAPDELAYEDWITHHOLES with_evars l tac] the delayed + argument of [l] are evaluated in the possibly-updated + environment and updated sigma of each new successive goals *) val tclTIMEOUT : int -> unit tactic -> unit tactic val tclTIME : string option -> 'a tactic -> 'a tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 8b38bc1b0a..5aa31092e9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2282,10 +2282,9 @@ let left_with_bindings with_evars = constructor_tac with_evars (Some 2) 1 let right_with_bindings with_evars = constructor_tac with_evars (Some 2) 2 let split_with_bindings with_evars l = Tacticals.New.tclMAP (constructor_tac with_evars (Some 1) 1) l -let split_with_delayed_bindings with_evars = - Tacticals.New.tclMAP (fun bl -> - Tacticals.New.tclDELAYEDWITHHOLES with_evars bl - (constructor_tac with_evars (Some 1) 1)) +let split_with_delayed_bindings with_evars bl = + Tacticals.New.tclMAPDELAYEDWITHHOLES with_evars bl + (constructor_tac with_evars (Some 1) 1) let left = left_with_bindings false let simplest_left = left NoBindings diff --git a/test-suite/bugs/closed/bug_13456.v b/test-suite/bugs/closed/bug_13456.v new file mode 100644 index 0000000000..b2e7fa7be5 --- /dev/null +++ b/test-suite/bugs/closed/bug_13456.v @@ -0,0 +1,5 @@ +Lemma minbug (n : nat) (P : nat -> Prop) (pn : P n) : exists (m : nat) (p : P m), True. +Proof. + exists _, pn. + exact I. +Qed. diff --git a/test-suite/output/ssr_pred.out b/test-suite/output/ssr_pred.out new file mode 100644 index 0000000000..f00111ff97 --- /dev/null +++ b/test-suite/output/ssr_pred.out @@ -0,0 +1,3 @@ +in1W + : forall (T1 : predArgType) (D1 : {pred T1}) (P1 : T1 -> Prop), + (forall x : T1, P1 x) -> {in D1, forall x : T1, P1 x} diff --git a/test-suite/output/ssr_pred.v b/test-suite/output/ssr_pred.v new file mode 100644 index 0000000000..bd88af80a3 --- /dev/null +++ b/test-suite/output/ssr_pred.v @@ -0,0 +1,3 @@ +Require Import ssreflect ssrfun ssrbool. + +Check @in1W. diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v index 97b4e39168..f1dad301fd 100644 --- a/test-suite/success/CompatCurrentFlag.v +++ b/test-suite/success/CompatCurrentFlag.v @@ -1,3 +1,3 @@ -(* -*- coq-prog-args: ("-compat" "8.13") -*- *) +(* -*- coq-prog-args: ("-compat" "8.14") -*- *) (** Check that the current compatibility flag actually requires the relevant modules. *) -Import Coq.Compat.Coq813. +Import Coq.Compat.Coq814. diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v index c06dd6e450..a737e0c98e 100644 --- a/test-suite/success/CompatOldFlag.v +++ b/test-suite/success/CompatOldFlag.v @@ -1,5 +1,5 @@ -(* -*- coq-prog-args: ("-compat" "8.11") -*- *) +(* -*- coq-prog-args: ("-compat" "8.12") -*- *) (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq814. Import Coq.Compat.Coq813. Import Coq.Compat.Coq812. -Import Coq.Compat.Coq811. diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v new file mode 100644 index 0000000000..f4cf703ec7 --- /dev/null +++ b/test-suite/success/CompatOldOldFlag.v @@ -0,0 +1,6 @@ +(* -*- coq-prog-args: ("-compat" "8.11") -*- *) +(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq814. +Import Coq.Compat.Coq813. +Import Coq.Compat.Coq812. +Import Coq.Compat.Coq811. diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v index 83010f2149..07d5fcd3ab 100644 --- a/test-suite/success/CompatPreviousFlag.v +++ b/test-suite/success/CompatPreviousFlag.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-compat" "8.12") -*- *) +(* -*- coq-prog-args: ("-compat" "8.13") -*- *) (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq814. Import Coq.Compat.Coq813. -Import Coq.Compat.Coq812. diff --git a/test-suite/success/typing_flags.v b/test-suite/success/typing_flags.v index bd20d9c804..4af2028e38 100644 --- a/test-suite/success/typing_flags.v +++ b/test-suite/success/typing_flags.v @@ -1,4 +1,51 @@ +From Coq Require Import Program.Tactics. +(* Part using attributes *) + +#[bypass_check(guard)] Fixpoint att_f' (n : nat) : nat := att_f' n. +#[bypass_check(guard)] Program Fixpoint p_att_f' (n : nat) : nat := p_att_f' n. + +#[bypass_check(universes)] Definition att_T := let t := Type in (t : t). +#[bypass_check(universes)] Program Definition p_att_T := let t := Type in (t : t). + +#[bypass_check(positivity)] +Inductive att_Cor := +| att_Over : att_Cor +| att_Next : ((att_Cor -> list nat) -> list nat) -> att_Cor. + +Fail #[bypass_check(guard=no)] Fixpoint f_att_f' (n : nat) : nat := f_att_f' n. +Fail #[bypass_check(universes=no)] Definition f_att_T := let t := Type in (t : t). + +Fail #[bypass_check(positivity=no)] +Inductive f_att_Cor := +| f_att_Over : f_att_Cor +| f_att_Next : ((f_att_Cor -> list nat) -> list nat) -> f_att_Cor. + +Print Assumptions att_f'. +Print Assumptions att_T. +Print Assumptions att_Cor. + +(* Interactive + atts *) +#[bypass_check(universes=yes)] Definition i_att_T' : Type. Proof. exact (let t := Type in (t : t)). Defined. +#[bypass_check(universes=yes)] Definition d_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed. +#[bypass_check(universes=yes)] Program Definition pi_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed. + +(* Note: be aware of tactics invoking [Global.env()] if this test fails. *) +#[bypass_check(guard=yes)] Fixpoint i_att_f' (n : nat) : nat. +Proof. exact (i_att_f' n). Defined. + +#[bypass_check(guard=yes)] Fixpoint d_att_f' (n : nat) : nat. +Proof. exact (d_att_f' n). Qed. + +(* check regular mode is still safe *) +Fail Fixpoint f_att_f' (n : nat) : nat := f_att_f' n. +Fail Definition f_att_T := let t := Type in (t : t). + +Fail Inductive f_att_Cor := +| f_att_Over : f_att_Cor +| f_att_Next : ((f_att_Cor -> list nat) -> list nat) -> f_att_Cor. + +(* Part using Set/Unset *) Print Typing Flags. Unset Guard Checking. Fixpoint f' (n : nat) : nat := f' n. diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh index 7ff5571ffb..61273c4f37 100755 --- a/test-suite/tools/update-compat/run.sh +++ b/test-suite/tools/update-compat/run.sh @@ -6,4 +6,4 @@ SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )" # we assume that the script lives in test-suite/tools/update-compat/, # and that update-compat.py lives in dev/tools/ cd "${SCRIPT_DIR}/../../.." -dev/tools/update-compat.py --assert-unchanged --release || exit $? +dev/tools/update-compat.py --assert-unchanged --master || exit $? diff --git a/theories/Compat/Coq813.v b/theories/Compat/Coq813.v index 92544c6ed9..fe7431dcd3 100644 --- a/theories/Compat/Coq813.v +++ b/theories/Compat/Coq813.v @@ -9,3 +9,5 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.13 *) + +Require Export Coq.Compat.Coq814. diff --git a/theories/Compat/Coq814.v b/theories/Compat/Coq814.v new file mode 100644 index 0000000000..94948dd280 --- /dev/null +++ b/theories/Compat/Coq814.v @@ -0,0 +1,11 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +(** Compatibility file for making Coq act similar to Coq v8.14 *) diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index ec339c69c6..fbf3b4873b 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -261,6 +261,7 @@ let get_native_name s = with _ -> "" let get_compat_file = function + | "8.14" -> "Coq.Compat.Coq814" | "8.13" -> "Coq.Compat.Coq813" | "8.12" -> "Coq.Compat.Coq812" | "8.11" -> "Coq.Compat.Coq811" diff --git a/vernac/attributes.ml b/vernac/attributes.ml index fdaeedef8c..37895d22f5 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -338,3 +338,47 @@ let uses_parser : string key_parser = fun orig args -> | _ -> CErrors.user_err (Pp.str "Ill formed \"using\" attribute") let using = attribute_of_list ["using",uses_parser] + +let process_typing_att ~typing_flags att disable = + let enable = not disable in + match att with + | "universes" -> + { typing_flags with + Declarations.check_universes = enable + } + | "guard" -> + { typing_flags with + Declarations.check_guarded = enable + } + | "positivity" -> + { typing_flags with + Declarations.check_positive = enable + } + | att -> + CErrors.user_err Pp.(str "Unknown “typing” attribute: " ++ str att) + +let process_typing_disable ~key = function + | VernacFlagEmpty | VernacFlagLeaf (FlagIdent "yes") -> + true + | VernacFlagLeaf (FlagIdent "no") -> + false + | _ -> + CErrors.user_err Pp.(str "Ill-formed attribute value, must be " ++ str key ++ str "={yes, no}") + +let typing_flags_parser : Declarations.typing_flags key_parser = fun orig args -> + let rec flag_parser typing_flags = function + | [] -> typing_flags + | (typing_att, enable) :: rest -> + let disable = process_typing_disable ~key:typing_att enable in + let typing_flags = process_typing_att ~typing_flags typing_att disable in + flag_parser typing_flags rest + in + match args with + | VernacFlagList atts -> + let typing_flags = Global.typing_flags () in + flag_parser typing_flags atts + | att -> + CErrors.user_err Pp.(str "Ill-formed “typing” attribute: " ++ pr_vernac_flag_value att) + +let typing_flags = + attribute_of_list ["bypass_check", typing_flags_parser] diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 03a14a03ff..584e13e781 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -59,6 +59,9 @@ val canonical_field : bool attribute val canonical_instance : bool attribute val using : string option attribute +(** Enable/Disable universe checking *) +val typing_flags : Declarations.typing_flags option attribute + val program_mode_option_name : string list (** For internal use when messing with the global option. *) diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml index adf1f42beb..a21af12785 100644 --- a/vernac/comArguments.ml +++ b/vernac/comArguments.ml @@ -223,10 +223,10 @@ let vernac_arguments ~section_local reference args more_implicits flags = | _ -> true in if implicits_specified && clear_implicits_flag then - CErrors.user_err Pp.(str "The \"clear implicits\" flag is incompatible with implicit annotations"); + CErrors.user_err Pp.(str "The \"clear implicits\" flag must be omitted if implicit annotations are given."); if implicits_specified && default_implicits_flag then - CErrors.user_err Pp.(str "The \"default implicits\" flag is incompatible with implicit annotations"); + CErrors.user_err Pp.(str "The \"default implicits\" flag is incompatible with implicit annotations."); let rargs = Util.List.map_filter (function (n, true) -> Some n | _ -> None) diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 81154bbea9..c54adb45f9 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -110,9 +110,10 @@ let interp_definition ~program_mode env evd impl_env bl red_option c ctypopt = let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in evd, (c, tyopt), imps -let do_definition ?hook ~name ~scope ~poly ~kind ?using udecl bl red_option c ctypopt = +let do_definition ?hook ~name ~scope ~poly ?typing_flags ~kind ?using udecl bl red_option c ctypopt = let program_mode = false in let env = Global.env() in + let env = Environ.update_typing_flags ?typing_flags env in (* Explicitly bound universes and constraints *) let evd, udecl = interp_univ_decl_opt env udecl in let evd, (body, types), impargs = @@ -125,14 +126,15 @@ let do_definition ?hook ~name ~scope ~poly ~kind ?using udecl bl red_option c ct in let kind = Decls.IsDefinition kind in let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types ?using () in - let info = Declare.Info.make ~scope ~kind ?hook ~udecl ~poly () in + let info = Declare.Info.make ~scope ~kind ?hook ~udecl ~poly ?typing_flags () in let _ : Names.GlobRef.t = Declare.declare_definition ~info ~cinfo ~opaque:false ~body evd in () -let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind ?using udecl bl red_option c ctypopt = +let do_definition_program ?hook ~pm ~name ~scope ~poly ?typing_flags ~kind ?using udecl bl red_option c ctypopt = let program_mode = true in let env = Global.env() in + let env = Environ.update_typing_flags ?typing_flags env in (* Explicitly bound universes and constraints *) let evd, udecl = interp_univ_decl_opt env udecl in let evd, (body, types), impargs = @@ -146,6 +148,6 @@ let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind ?using udecl bl red let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in let pm, _ = let cinfo = Declare.CInfo.make ~name ~typ ~impargs ?using () in - let info = Declare.Info.make ~udecl ~scope ~poly ~kind ?hook () in + let info = Declare.Info.make ~udecl ~scope ~poly ~kind ?hook ?typing_flags () in Declare.Obls.add_definition ~pm ~cinfo ~info ~term ~uctx obls in pm diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 5e1b705ae4..9962e44098 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -30,6 +30,7 @@ val do_definition -> name:Id.t -> scope:Locality.locality -> poly:bool + -> ?typing_flags:Declarations.typing_flags -> kind:Decls.definition_object_kind -> ?using:Vernacexpr.section_subset_expr -> universe_decl_expr option @@ -45,6 +46,7 @@ val do_definition_program -> name:Id.t -> scope:Locality.locality -> poly:bool + -> ?typing_flags:Declarations.typing_flags -> kind:Decls.logical_kind -> ?using:Vernacexpr.section_subset_expr -> universe_decl_expr option diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index dd6c985bf9..0cf0b07822 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -158,10 +158,9 @@ type ('constr, 'types) recursive_preentry = let fix_proto sigma = Evarutil.new_global sigma (Coqlib.lib_ref "program.tactic.fix_proto") -let interp_recursive ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen list) = +let interp_recursive env ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen list) = let open Context.Named.Declaration in let open EConstr in - let env = Global.env() in let fixnames = List.map (fun fix -> fix.Vernacexpr.fname.CAst.v) fixl in (* Interp arities allowing for unresolved types *) @@ -241,11 +240,13 @@ let ground_fixpoint env evd (fixnames,fixrs,fixdefs,fixtypes) = Evd.evar_universe_context evd, (fixnames,fixrs,fixdefs,fixtypes) (* XXX: Unify with interp_recursive *) -let interp_fixpoint ?(check_recursivity=true) ~cofix l : +let interp_fixpoint ?(check_recursivity=true) ?typing_flags ~cofix l : ( (Constr.t, Constr.types) recursive_preentry * UState.universe_decl * UState.t * (EConstr.rel_context * Impargs.manual_implicits * int option) list) = - let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l in + let env = Global.env () in + let env = Environ.update_typing_flags ?typing_flags env in + let (env,_,pl,evd),fix,info = interp_recursive env ~program_mode:false ~cofix l in if check_recursivity then check_recursive true env evd fix; let evd = Pretyping.(solve_remaining_evars all_no_fail_flags env evd) in let uctx,fix = ground_fixpoint env evd fix in @@ -271,12 +272,12 @@ let build_recthms ~indexes ?using fixnames fixtypes fiximps = in fix_kind, cofix, thms -let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns = +let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ?typing_flags ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns = let fix_kind, cofix, thms = build_recthms ~indexes fixnames fixtypes fiximps in let indexes = Option.default [] indexes in let init_terms = Some fixdefs in let evd = Evd.from_ctx ctx in - let info = Declare.Info.make ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl () in + let info = Declare.Info.make ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl ?typing_flags () in let lemma = Declare.Proof.start_mutual_with_initialization ~info evd ~mutual_info:(cofix,indexes,init_terms) ~cinfo:thms None in @@ -284,13 +285,13 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; lemma -let declare_fixpoint_generic ?indexes ~scope ~poly ?using ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns = +let declare_fixpoint_generic ?indexes ~scope ~poly ?typing_flags ?using ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns = (* We shortcut the proof process *) let fix_kind, cofix, fixitems = build_recthms ~indexes ?using fixnames fixtypes fiximps in let fixdefs = List.map Option.get fixdefs in let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in let fix_kind = Decls.IsDefinition fix_kind in - let info = Declare.Info.make ~scope ~kind:fix_kind ~poly ~udecl () in + let info = Declare.Info.make ~scope ~kind:fix_kind ~poly ~udecl ?typing_flags () in let cinfo = fixitems in let _ : GlobRef.t list = Declare.declare_mutually_recursive ~cinfo ~info ~opaque:false ~uctx @@ -322,22 +323,22 @@ let adjust_rec_order ~structonly binders rec_order = in Option.map (extract_decreasing_argument ~structonly) rec_order -let do_fixpoint_common (fixl : Vernacexpr.fixpoint_expr list) = +let do_fixpoint_common ?typing_flags (fixl : Vernacexpr.fixpoint_expr list) = let fixl = List.map (fun fix -> Vernacexpr.{ fix with rec_order = adjust_rec_order ~structonly:true fix.binders fix.rec_order }) fixl in let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in - let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl in + let (_, _, _, info as fix) = interp_fixpoint ~cofix:false ?typing_flags fixl in fixl, ntns, fix, List.map compute_possible_guardness_evidences info -let do_fixpoint_interactive ~scope ~poly l : Declare.Proof.t = - let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in - let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes ~scope ~poly fix ntns in +let do_fixpoint_interactive ~scope ~poly ?typing_flags l : Declare.Proof.t = + let fixl, ntns, fix, possible_indexes = do_fixpoint_common ?typing_flags l in + let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes ~scope ~poly ?typing_flags fix ntns in lemma -let do_fixpoint ~scope ~poly ?using l = - let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in - declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly ?using fix ntns +let do_fixpoint ~scope ~poly ?typing_flags ?using l = + let fixl, ntns, fix, possible_indexes = do_fixpoint_common ?typing_flags l in + declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly ?typing_flags ?using fix ntns let do_cofixpoint_common (fixl : Vernacexpr.cofixpoint_expr list) = let fixl = List.map (fun fix -> {fix with Vernacexpr.rec_order = None}) fixl in diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index a36aba7672..faa5fce375 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -15,11 +15,20 @@ open Vernacexpr (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) -val do_fixpoint_interactive : - scope:Locality.locality -> poly:bool -> fixpoint_expr list -> Declare.Proof.t +val do_fixpoint_interactive + : scope:Locality.locality + -> poly:bool + -> ?typing_flags:Declarations.typing_flags + -> fixpoint_expr list + -> Declare.Proof.t -val do_fixpoint : - scope:Locality.locality -> poly:bool -> ?using:Vernacexpr.section_subset_expr -> fixpoint_expr list -> unit +val do_fixpoint + : scope:Locality.locality + -> poly:bool + -> ?typing_flags:Declarations.typing_flags + -> ?using:Vernacexpr.section_subset_expr + -> fixpoint_expr list + -> unit val do_cofixpoint_interactive : scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> Declare.Proof.t @@ -44,6 +53,7 @@ type ('constr, 'types) recursive_preentry = Id.t list * Sorts.relevance list * ' (** Exported for Program *) val interp_recursive : + Environ.env -> (* Misc arguments *) program_mode:bool -> cofix:bool -> (* Notations of the fixpoint / should that be folded in the previous argument? *) @@ -58,8 +68,9 @@ val interp_recursive : (** Exported for Funind *) val interp_fixpoint - : ?check_recursivity:bool -> - cofix:bool + : ?check_recursivity:bool + -> ?typing_flags:Declarations.typing_flags + -> cofix:bool -> lident option fix_expr_gen list -> (Constr.t, Constr.types) recursive_preentry * UState.universe_decl * UState.t * diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 8cb077ca21..2be6097184 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -631,7 +631,7 @@ type uniform_inductive_flag = | UniformParameters | NonUniformParameters -let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uniform finite = +let do_mutual_inductive ~template udecl indl ~cumulative ~poly ?typing_flags ~private_ind ~uniform finite = let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in (* Interpret the types *) let indl = match params with @@ -640,9 +640,11 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uni | UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in - let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns ~cumulative ~poly ~private_ind finite in + let env = Global.env () in + let env = Environ.update_typing_flags ?typing_flags env in + let mie,pl,impls = interp_mutual_inductive_gen env ~template udecl indl ntns ~cumulative ~poly ~private_ind finite in (* Declare the mutual inductive block with its associated schemes *) - ignore (DeclareInd.declare_mutual_inductive_with_eliminations mie pl impls); + ignore (DeclareInd.declare_mutual_inductive_with_eliminations ?typing_flags mie pl impls); (* Declare the possible notations of inductive types *) List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns; (* Declare the coercions *) diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 8bce884ba4..e049bacb26 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -26,6 +26,7 @@ val do_mutual_inductive -> (one_inductive_expr * decl_notation list) list -> cumulative:bool -> poly:bool + -> ?typing_flags:Declarations.typing_flags -> private_ind:bool -> uniform:uniform_inductive_flag -> Declarations.recursivity_kind diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 31f91979d3..3c4a651cf5 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -109,7 +109,7 @@ let telescope env sigma l = let nf_evar_context sigma ctx = List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx -let build_wellfounded pm (recname,pl,bl,arityc,body) poly ?using r measure notation = +let build_wellfounded pm (recname,pl,bl,arityc,body) poly ?typing_flags ?using r measure notation = let open EConstr in let open Vars in let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in @@ -266,7 +266,7 @@ let build_wellfounded pm (recname,pl,bl,arityc,body) poly ?using r measure notat in let uctx = Evd.evar_universe_context sigma in let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ ?using () in - let info = Declare.Info.make ~udecl ~poly ~hook () in + let info = Declare.Info.make ~udecl ~poly ~hook ?typing_flags () in let pm, _ = Declare.Obls.add_definition ~pm ~cinfo ~info ~term:evars_def ~uctx evars in pm @@ -280,10 +280,12 @@ let collect_evars_of_term evd c ty = Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev)) evars (Evd.from_ctx (Evd.evar_universe_context evd)) -let do_program_recursive ~pm ~scope ~poly ?using fixkind fixl = +let do_program_recursive ~pm ~scope ~poly ?typing_flags ?using fixkind fixl = let cofix = fixkind = Declare.Obls.IsCoFixpoint in let (env, rec_sign, udecl, evd), fix, info = - interp_recursive ~cofix ~program_mode:true fixl + let env = Global.env () in + let env = Environ.update_typing_flags ?typing_flags env in + interp_recursive env ~cofix ~program_mode:true fixl in (* Program-specific code *) (* Get the interesting evars, those that were not instantiated *) @@ -320,10 +322,13 @@ let do_program_recursive ~pm ~scope ~poly ?using fixkind fixl = Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs) in let indexes = - Pretyping.search_guard (Global.env ()) possible_indexes fixdecls in + let env = Global.env () in + let env = Environ.update_typing_flags ?typing_flags env in + Pretyping.search_guard env possible_indexes fixdecls in + let env = Environ.update_typing_flags ?typing_flags env in List.iteri (fun i _ -> Inductive.check_fix env - ((indexes,i),fixdecls)) + ((indexes,i),fixdecls)) fixl end in let uctx = Evd.evar_universe_context evd in @@ -332,16 +337,16 @@ let do_program_recursive ~pm ~scope ~poly ?using fixkind fixl = | Declare.Obls.IsCoFixpoint -> Decls.(IsDefinition CoFixpoint) in let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in - let info = Declare.Info.make ~poly ~scope ~kind ~udecl () in + let info = Declare.Info.make ~poly ~scope ~kind ~udecl ?typing_flags () in Declare.Obls.add_mutual_definitions ~pm defs ~info ~uctx ~ntns fixkind -let do_fixpoint ~pm ~scope ~poly ?using l = +let do_fixpoint ~pm ~scope ~poly ?typing_flags ?using l = let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in match g, l with | [Some { CAst.v = CWfRec (n,r) }], [ Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations} ] -> let recarg = mkIdentC n.CAst.v in - build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly ?using r recarg notations + build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly ?typing_flags ?using r recarg notations | [Some { CAst.v = CMeasureRec (n, m, r) }], [Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations }] -> @@ -354,7 +359,7 @@ let do_fixpoint ~pm ~scope ~poly ?using l = user_err Pp.(str"Measure takes only two arguments in Program Fixpoint.") | _, _ -> r in - build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly ?using + build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly ?typing_flags ?using (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m notations | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g -> @@ -362,7 +367,7 @@ let do_fixpoint ~pm ~scope ~poly ?using l = Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in let fixkind = Declare.Obls.IsFixpoint annots in let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in - do_program_recursive ~pm ~scope ~poly ?using fixkind l + do_program_recursive ~pm ~scope ~poly ?typing_flags ?using fixkind l | _, _ -> CErrors.user_err ~hdr:"do_fixpoint" (str "Well-founded fixpoints not allowed in mutually recursive blocks") diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli index 30bf3ae8f8..0193be8683 100644 --- a/vernac/comProgramFixpoint.mli +++ b/vernac/comProgramFixpoint.mli @@ -15,6 +15,7 @@ val do_fixpoint : pm:Declare.OblState.t -> scope:Locality.locality -> poly:bool + -> ?typing_flags:Declarations.typing_flags -> ?using:Vernacexpr.section_subset_expr -> fixpoint_expr list -> Declare.OblState.t diff --git a/vernac/declare.ml b/vernac/declare.ml index 73ebca276d..fafee13bf6 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -83,14 +83,15 @@ module Info = struct ; udecl : UState.universe_decl ; scope : Locality.locality ; hook : Hook.t option + ; typing_flags : Declarations.typing_flags option } (** Note that [opaque] doesn't appear here as it is not known at the start of the proof in the interactive case. *) let make ?(poly=false) ?(inline=false) ?(kind=Decls.(IsDefinition Definition)) ?(udecl=UState.default_univ_decl) ?(scope=Locality.Global Locality.ImportDefaultBehavior) - ?hook () = - { poly; inline; kind; udecl; scope; hook } + ?hook ?typing_flags () = + { poly; inline; kind; udecl; scope; hook; typing_flags } end @@ -325,12 +326,12 @@ let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proo let feedback_axiom () = Feedback.(feedback AddedAxiom) -let is_unsafe_typing_flags () = +let is_unsafe_typing_flags flags = + let flags = Option.default (Global.typing_flags ()) flags in let open Declarations in - let flags = Environ.typing_flags (Global.env()) in not (flags.check_universes && flags.check_guarded && flags.check_positive) -let define_constant ~name cd = +let define_constant ~name ~typing_flags cd = (* Logically define the constant and its subproofs, no libobject tampering *) let decl, unsafe = match cd with | DefinitionEntry de -> @@ -354,13 +355,13 @@ let define_constant ~name cd = | PrimitiveEntry e -> ConstantEntry (Entries.PrimitiveEntry e), false in - let kn = Global.add_constant name decl in - if unsafe || is_unsafe_typing_flags() then feedback_axiom(); + let kn = Global.add_constant ?typing_flags name decl in + if unsafe || is_unsafe_typing_flags typing_flags then feedback_axiom(); kn -let declare_constant ?(local = Locality.ImportDefaultBehavior) ~name ~kind cd = +let declare_constant ?(local = Locality.ImportDefaultBehavior) ~name ~kind ~typing_flags cd = let () = check_exists name in - let kn = define_constant ~name cd in + let kn = define_constant ~typing_flags ~name cd in (* Register the libobjects attached to the constants *) let () = register_constant kn kind local in kn @@ -557,7 +558,7 @@ let declare_definition_scheme ~internal ~univs ~role ~name c = kn, eff (* Locality stuff *) -let declare_entry_core ~name ~scope ~kind ?hook ~obls ~impargs ~uctx entry = +let declare_entry_core ~name ~scope ~kind ~typing_flags ?hook ~obls ~impargs ~uctx entry = let should_suggest = entry.proof_entry_opaque && not (List.is_empty (Global.named_context())) @@ -570,7 +571,7 @@ let declare_entry_core ~name ~scope ~kind ?hook ~obls ~impargs ~uctx entry = if should_suggest then Proof_using.suggest_variable (Global.env ()) name; Names.GlobRef.VarRef name | Locality.Global local -> - let kn = declare_constant ~name ~local ~kind (DefinitionEntry entry) in + let kn = declare_constant ~name ~local ~kind ~typing_flags (DefinitionEntry entry) in let gr = Names.GlobRef.ConstRef kn in if should_suggest then Proof_using.suggest_constant (Global.env ()) kn; let () = DeclareUniv.declare_univ_binders gr ubind in @@ -583,10 +584,11 @@ let declare_entry_core ~name ~scope ~kind ?hook ~obls ~impargs ~uctx entry = let declare_entry = declare_entry_core ~obls:[] -let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes = +let mutual_make_bodies ~typing_flags ~fixitems ~rec_declaration ~possible_indexes = match possible_indexes with | Some possible_indexes -> let env = Global.env() in + let env = Environ.update_typing_flags ?typing_flags env in let indexes = Pretyping.search_guard env possible_indexes rec_declaration in let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),rec_declaration)) in let fixdecls = CList.map_i (fun i _ -> Constr.mkFix ((indexes,i),rec_declaration)) 0 fixitems in @@ -597,9 +599,9 @@ let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes = vars, fixdecls, None let declare_mutually_recursive_core ~info ~cinfo ~opaque ~ntns ~uctx ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) () = - let { Info.poly; udecl; scope; kind; _ } = info in + let { Info.poly; udecl; scope; kind; typing_flags; _ } = info in let vars, fixdecls, indexes = - mutual_make_bodies ~fixitems:cinfo ~rec_declaration ~possible_indexes in + mutual_make_bodies ~typing_flags ~fixitems:cinfo ~rec_declaration ~possible_indexes in let uctx, univs = (* XXX: Obligations don't do this, this seems like a bug? *) if restrict_ucontext @@ -614,7 +616,7 @@ let declare_mutually_recursive_core ~info ~cinfo ~opaque ~ntns ~uctx ~rec_declar let csts = CList.map2 (fun CInfo.{ name; typ; impargs; using } body -> let entry = definition_entry ~opaque ~types:typ ~univs ?using body in - declare_entry ~name ~scope ~kind ~impargs ~uctx entry) + declare_entry ~name ~scope ~kind ~impargs ~uctx ~typing_flags entry) cinfo fixdecls in let isfix = Option.has_some possible_indexes in @@ -637,7 +639,7 @@ let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe = in let kind = Decls.(IsAssumption Conjectural) in let decl = ParameterEntry pe in - let kn = declare_constant ~name ~local ~kind decl in + let kn = declare_constant ~name ~local ~kind ~typing_flags:None decl in let dref = Names.GlobRef.ConstRef kn in let () = Impargs.maybe_declare_manual_implicits false dref impargs in let () = assumption_message name in @@ -680,8 +682,8 @@ let prepare_definition ~info ~opaque ?using ~body ~typ sigma = let declare_definition_core ~info ~cinfo ~opaque ~obls ~body sigma = let { CInfo.name; impargs; typ; using; _ } = cinfo in let entry, uctx = prepare_definition ~info ~opaque ?using ~body ~typ sigma in - let { Info.scope; kind; hook; _ } = info in - declare_entry_core ~name ~scope ~kind ~impargs ~obls ?hook ~uctx entry, uctx + let { Info.scope; kind; hook; typing_flags; _ } = info in + declare_entry_core ~name ~scope ~kind ~impargs ~typing_flags ~obls ?hook ~uctx entry, uctx let declare_definition ~info ~cinfo ~opaque ~body sigma = declare_definition_core ~obls:[] ~info ~cinfo ~opaque ~body sigma |> fst @@ -913,6 +915,7 @@ let declare_obligation prg obl ~uctx ~types ~body = (* ppedrot: seems legit to have obligations as local *) let constant = declare_constant ~name:obl.obl_name + ~typing_flags:prg.prg_info.Info.typing_flags ~local:Locality.ImportNeedQualified ~kind:Decls.(IsProof Property) (DefinitionEntry ce) @@ -1425,9 +1428,9 @@ let start_proof_core ~name ~typ ~pinfo ?(sign=initialize_named_context_for_proof marked "opaque", this is a hack tho, see #10446, and build_constant_by_tactic uses a different method that would break program_inference_hook *) - let { Proof_info.info = { Info.poly; _ }; _ } = pinfo in + let { Proof_info.info = { Info.poly; typing_flags; _ }; _ } = pinfo in let goals = [Global.env_of_context sign, typ] in - let proof = Proof.start ~name ~poly sigma goals in + let proof = Proof.start ~name ~poly ?typing_flags sigma goals in let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in { proof ; endline_tactic = None @@ -1448,7 +1451,8 @@ let start_core ~info ~cinfo ?proof_ending sigma = let start = start_core ?proof_ending:None let start_dependent ~info ~name ~proof_ending goals = - let proof = Proof.dependent_start ~name ~poly:info.Info.poly goals in + let { Info.poly; typing_flags; _ } = info in + let proof = Proof.dependent_start ~name ~poly ?typing_flags goals in let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in let cinfo = [] in let pinfo = Proof_info.make ~info ~cinfo ~proof_ending () in @@ -1886,7 +1890,7 @@ end = struct let declare_mutdef ~uctx ~pinfo pe i CInfo.{ name; impargs; typ; _} = let { Proof_info.info; compute_guard; _ } = pinfo in - let { Info.hook; scope; kind; _ } = info in + let { Info.hook; scope; kind; typing_flags; _ } = info in (* if i = 0 , we don't touch the type; this is for compat but not clear it is the right thing to do. *) @@ -1903,7 +1907,7 @@ end = struct Internal.map_entry_body pe ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) in - declare_entry ~name ~scope ~kind ?hook ~impargs ~uctx pe + declare_entry ~name ~scope ~kind ?hook ~impargs ~typing_flags ~uctx pe let declare_mutdef ~pinfo ~uctx ~entry = let pe = match pinfo.Proof_info.compute_guard with @@ -1913,6 +1917,8 @@ end = struct | possible_indexes -> (* Try all combinations... not optimal *) let env = Global.env() in + let typing_flags = pinfo.Proof_info.info.Info.typing_flags in + let env = Environ.update_typing_flags ?typing_flags env in Internal.map_entry_body entry ~f:(guess_decreasing env possible_indexes) in @@ -1993,7 +1999,7 @@ let finish_derived ~f ~name ~entries = let f_def = Internal.set_opacity ~opaque:false f_def in let f_kind = Decls.(IsDefinition Definition) in let f_def = DefinitionEntry f_def in - let f_kn = declare_constant ~name:f ~kind:f_kind f_def in + let f_kn = declare_constant ~name:f ~kind:f_kind f_def ~typing_flags:None in let f_kn_term = Constr.mkConst f_kn in (* In the type and body of the proof of [suchthat] there can be references to the variable [f]. It needs to be replaced by @@ -2011,7 +2017,7 @@ let finish_derived ~f ~name ~entries = (* The same is done in the body of the proof. *) let lemma_def = Internal.map_entry_body lemma_def ~f:(fun ((b,ctx),fx) -> (substf b, ctx), fx) in let lemma_def = DefinitionEntry lemma_def in - let ct = declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in + let ct = declare_constant ~name ~typing_flags:None ~kind:Decls.(IsProof Proposition) lemma_def in [GlobRef.ConstRef f_kn; GlobRef.ConstRef ct] let finish_proved_equations ~pm ~kind ~hook i proof_obj types sigma0 = @@ -2025,7 +2031,7 @@ let finish_proved_equations ~pm ~kind ~hook i proof_obj types sigma0 = | None -> let n = !obls in incr obls; Nameops.add_suffix i ("_obligation_" ^ string_of_int n) in let entry, args = Internal.shrink_entry local_context entry in - let cst = declare_constant ~name:id ~kind (DefinitionEntry entry) in + let cst = declare_constant ~name:id ~kind ~typing_flags:None (DefinitionEntry entry) in let sigma, app = Evarutil.new_global sigma (GlobRef.ConstRef cst) in let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in sigma, cst) sigma0 @@ -2519,3 +2525,9 @@ type nonrec progress = progress = end module OblState = Obls_.State + +let declare_constant ?local ~name ~kind ?typing_flags = + declare_constant ?local ~name ~kind ~typing_flags + +let declare_entry ~name ~scope ~kind = + declare_entry ~name ~scope ~kind ~typing_flags:None diff --git a/vernac/declare.mli b/vernac/declare.mli index e4c77113af..37a61cc4f0 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -109,6 +109,7 @@ module Info : sig (** locality *) -> ?hook : Hook.t (** Callback to be executed after saving the constant *) + -> ?typing_flags:Declarations.typing_flags -> unit -> t @@ -387,6 +388,7 @@ val declare_constant : ?local:Locality.import_status -> name:Id.t -> kind:Decls.logical_kind + -> ?typing_flags:Declarations.typing_flags -> Evd.side_effects constant_entry -> Constant.t diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml index e22d63b811..7050ddc042 100644 --- a/vernac/declareInd.ml +++ b/vernac/declareInd.ml @@ -104,7 +104,7 @@ let is_unsafe_typing_flags () = not (flags.check_universes && flags.check_guarded && flags.check_positive) (* for initial declaration *) -let declare_mind mie = +let declare_mind ?typing_flags mie = let id = match mie.mind_entry_inds with | ind::_ -> ind.mind_entry_typename | [] -> CErrors.anomaly (Pp.str "cannot declare an empty list of inductives.") in @@ -113,7 +113,7 @@ let declare_mind mie = List.iter (fun (typ, cons) -> Declare.check_exists typ; List.iter Declare.check_exists cons) names; - let _kn' = Global.add_mind id mie in + let _kn' = Global.add_mind ?typing_flags id mie in let (sp,kn as oname) = Lib.add_leaf id (inInductive { ind_names = names }) in if is_unsafe_typing_flags() then feedback_axiom (); let mind = Global.mind_of_delta_kn kn in @@ -154,7 +154,7 @@ type one_inductive_impls = Impargs.manual_implicits (* for inds *) * Impargs.manual_implicits list (* for constrs *) -let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie pl impls = +let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) ?typing_flags mie pl impls = (* spiwack: raises an error if the structure is supposed to be non-recursive, but isn't *) begin match mie.mind_entry_finite with @@ -166,7 +166,7 @@ let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie p | _ -> () end; let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in - let (_, kn), prim = declare_mind mie in + let (_, kn), prim = declare_mind ?typing_flags mie in let mind = Global.mind_of_delta_kn kn in if primitive_expected && not prim then warn_non_primitive_record (mind,0); DeclareUniv.declare_univ_binders (GlobRef.IndRef (mind,0)) pl; diff --git a/vernac/declareInd.mli b/vernac/declareInd.mli index 05a1617329..eacf20e30c 100644 --- a/vernac/declareInd.mli +++ b/vernac/declareInd.mli @@ -17,6 +17,7 @@ type one_inductive_impls = val declare_mutual_inductive_with_eliminations : ?primitive_expected:bool + -> ?typing_flags:Declarations.typing_flags -> Entries.mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 57b264bbc2..a3726daf63 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -57,16 +57,17 @@ module DefAttributes = struct program : bool; deprecated : Deprecation.t option; canonical_instance : bool; + typing_flags : Declarations.typing_flags option; using : Vernacexpr.section_subset_expr option; } let parse f = let open Attributes in - let ((((locality, deprecated), polymorphic), program), canonical_instance), using = - parse Notations.(locality ++ deprecation ++ polymorphic ++ program ++ canonical_instance ++ using) f + let (((((locality, deprecated), polymorphic), program), canonical_instance), typing_flags), using = + parse Notations.(locality ++ deprecation ++ polymorphic ++ program ++ canonical_instance ++ typing_flags ++ using) f in let using = Option.map Proof_using.using_from_string using in - { polymorphic; program; locality; deprecated; canonical_instance; using } + { polymorphic; program; locality; deprecated; canonical_instance; typing_flags; using } end let module_locality = Attributes.Notations.(locality >>= fun l -> return (make_module_locality l)) @@ -512,6 +513,7 @@ let vernac_set_used_variables ~pstate e : Declare.Proof.t = l; let _, pstate = Declare.Proof.set_used_variables pstate l in pstate + let vernac_set_used_variables_opt ?using pstate = match using with | None -> pstate @@ -546,28 +548,29 @@ let post_check_evd ~udecl ~poly evd = else (* We fix the variables to ensure they won't be lowered to Set *) Evd.fix_undefined_variables evd -let start_lemma_com ~program_mode ~poly ~scope ~kind ?using ?hook thms = +let start_lemma_com ~typing_flags ~program_mode ~poly ~scope ~kind ?using ?hook thms = let env0 = Global.env () in + let env0 = Environ.update_typing_flags ?typing_flags env0 in let flags = Pretyping.{ all_no_fail_flags with program_mode } in let decl = fst (List.hd thms) in let evd, udecl = Constrintern.interp_univ_decl_opt env0 (snd decl) in let evd, thms = interp_lemma ~program_mode ~flags ~scope env0 evd thms in let mut_analysis = RecLemmas.look_for_possibly_mutual_statements evd thms in let evd = Evd.minimize_universes evd in - let pstate = + let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl ?typing_flags () in + begin match mut_analysis with | RecLemmas.NonMutual thm -> let thm = Declare.CInfo.to_constr evd thm in let evd = post_check_evd ~udecl ~poly evd in - let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in Declare.Proof.start_with_initialization ~info ~cinfo:thm evd | RecLemmas.Mutual { mutual_info; cinfo ; possible_guards } -> let cinfo = List.map (Declare.CInfo.to_constr evd) cinfo in let evd = post_check_evd ~udecl ~poly evd in - let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in Declare.Proof.start_mutual_with_initialization ~info ~cinfo evd ~mutual_info (Some possible_guards) - in - vernac_set_used_variables_opt ?using pstate + end + (* XXX: This should be handled in start_with_initialization, see duplicate using in declare.ml *) + |> vernac_set_used_variables_opt ?using let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in function | Coercion -> @@ -606,14 +609,16 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t = let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind in let program_mode = atts.program in let poly = atts.polymorphic in + let typing_flags = atts.typing_flags in let name = vernac_definition_name lid local in - start_lemma_com ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?using:atts.using ?hook [(name, pl), (bl, t)] + start_lemma_com ~typing_flags ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?using:atts.using ?hook [(name, pl), (bl, t)] let vernac_definition ~atts ~pm (discharge, kind) (lid, pl) bl red_option c typ_opt = let open DefAttributes in let scope = enforce_locality_exp atts.locality discharge in let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind in let program_mode = atts.program in + let typing_flags = atts.typing_flags in let name = vernac_definition_name lid scope in let red_option = match red_option with | None -> None @@ -624,11 +629,11 @@ let vernac_definition ~atts ~pm (discharge, kind) (lid, pl) bl red_option c typ_ if program_mode then let kind = Decls.IsDefinition kind in ComDefinition.do_definition_program ~pm ~name:name.v - ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook + ~poly:atts.polymorphic ?typing_flags ~scope ~kind pl bl red_option c typ_opt ?hook else let () = ComDefinition.do_definition ~name:name.v - ~poly:atts.polymorphic ~scope ~kind ?using:atts.using pl bl red_option c typ_opt ?hook in + ~poly:atts.polymorphic ?typing_flags ~scope ~kind ?using:atts.using pl bl red_option c typ_opt ?hook in pm (* NB: pstate argument to use combinators easily *) @@ -637,7 +642,11 @@ let vernac_start_proof ~atts kind l = let scope = enforce_locality_exp atts.locality NoDischarge in if Dumpglob.dump () then List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l; - start_lemma_com ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.IsProof kind) ?using:atts.using l + start_lemma_com + ~typing_flags:atts.typing_flags + ~program_mode:atts.program + ~poly:atts.polymorphic + ~scope ~kind:(Decls.IsProof kind) ?using:atts.using l let vernac_end_proof ~lemma ~pm = let open Vernacexpr in function | Admitted -> @@ -720,7 +729,7 @@ let should_treat_as_uniform () = then ComInductive.UniformParameters else ComInductive.NonUniformParameters -let vernac_record ~template udecl ~cumulative k ~poly finite records = +let vernac_record ~template udecl ~cumulative k ~poly ?typing_flags finite records = let map ((is_coercion, name), binders, sort, nameopt, cfs) = let idbuild = match nameopt with | None -> Nameops.add_prefix "Build_" name.v @@ -741,7 +750,13 @@ let vernac_record ~template udecl ~cumulative k ~poly finite records = Record.Ast.{ name; is_coercion; binders; cfs; idbuild; sort } in let records = List.map map records in - ignore(Record.definition_structure ~template udecl k ~cumulative ~poly finite records) + match typing_flags with + | Some _ -> + CErrors.user_err (Pp.str "typing flags are not yet supported for records") + | None -> + let _ : _ list = + Record.definition_structure ~template udecl k ~cumulative ~poly finite records in + () let extract_inductive_udecl (indl:(inductive_expr * decl_notation list) list) = match indl with @@ -773,8 +788,8 @@ let private_ind = | None -> return false let vernac_inductive ~atts kind indl = - let (template, (poly, cumulative)), private_ind = Attributes.( - parse Notations.(template ++ polymorphic_cumulative ++ private_ind) atts) in + let ((template, (poly, cumulative)), private_ind), typing_flags = Attributes.( + parse Notations.(template ++ polymorphic_cumulative ++ private_ind ++ typing_flags) atts) in let open Pp in let udecl, indl = extract_inductive_udecl indl in if Dumpglob.dump () then @@ -811,7 +826,7 @@ let vernac_inductive ~atts kind indl = let coe' = if coe then BackInstance else NoInstance in let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), [], ce), { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } in - vernac_record ~template udecl ~cumulative (Class true) ~poly finite [id, bl, c, None, [f]] + vernac_record ~template udecl ~cumulative (Class true) ~poly ?typing_flags finite [id, bl, c, None, [f]] else if List.for_all is_record indl then (* Mutual record case *) let () = match kind with @@ -836,7 +851,7 @@ let vernac_inductive ~atts kind indl = in let kind = match kind with Class _ -> Class false | _ -> kind in let recordl = List.map unpack indl in - vernac_record ~template udecl ~cumulative kind ~poly finite recordl + vernac_record ~template udecl ~cumulative kind ~poly ?typing_flags finite recordl else if List.for_all is_constructor indl then (* Mutual inductive case *) let () = match kind with @@ -860,7 +875,7 @@ let vernac_inductive ~atts kind indl = in let indl = List.map unpack indl in let uniform = should_treat_as_uniform () in - ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uniform finite + ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly ?typing_flags ~private_ind ~uniform finite else user_err (str "Mixed record-inductive definitions are not allowed") @@ -874,17 +889,19 @@ let vernac_fixpoint_interactive ~atts discharge l = let scope = vernac_fixpoint_common ~atts discharge l in if atts.program then CErrors.user_err Pp.(str"Program Fixpoint requires a body"); - vernac_set_used_variables_opt ?using:atts.using - (ComFixpoint.do_fixpoint_interactive ~scope ~poly:atts.polymorphic l) + let typing_flags = atts.typing_flags in + ComFixpoint.do_fixpoint_interactive ~scope ~poly:atts.polymorphic ?typing_flags l + |> vernac_set_used_variables_opt ?using:atts.using let vernac_fixpoint ~atts ~pm discharge l = let open DefAttributes in let scope = vernac_fixpoint_common ~atts discharge l in + let typing_flags = atts.typing_flags in if atts.program then (* XXX: Switch to the attribute system and match on ~atts *) - ComProgramFixpoint.do_fixpoint ~pm ~scope ~poly:atts.polymorphic ?using:atts.using l + ComProgramFixpoint.do_fixpoint ~pm ~scope ~poly:atts.polymorphic ?typing_flags ?using:atts.using l else - let () = ComFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic ?using:atts.using l in + let () = ComFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic ?typing_flags ?using:atts.using l in pm let vernac_cofixpoint_common ~atts discharge l = |