diff options
152 files changed, 1430 insertions, 668 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 99ae4c23ce..ddbace193a 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -19,7 +19,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2020-10-12-V89" + CACHEKEY: "bionic_coq-V2020-11-26-V92" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -711,7 +711,12 @@ library:ci-color: - plugin:ci-bignums library:ci-compcert: + stage: stage-3 extends: .ci-template-flambda + needs: + - build:edge+flambda + - library:ci-flocq + - library:ci-menhir library:ci-coq_performance_tests: extends: .ci-template @@ -733,7 +738,14 @@ library:ci-coqtail: extends: .ci-template library:ci-coquelicot: - extends: .ci-template + stage: stage-3 + extends: .ci-template-flambda + needs: + - build:edge+flambda + - library:ci-mathcomp + dependencies: + - build:edge+flambda + - library:ci-mathcomp library:ci-cross_crypto: extends: .ci-template @@ -784,6 +796,45 @@ library:ci-fiat_crypto_ocaml: library:ci-flocq: extends: .ci-template-flambda +library:ci-menhir: + extends: .ci-template-flambda + +library:ci-interval: + extends: .ci-template-flambda + stage: stage-4 + needs: + - build:edge+flambda + - library:ci-coquelicot + - library:ci-flocq + - library:ci-mathcomp + - plugin:ci-bignums + dependencies: + - build:edge+flambda + - library:ci-coquelicot + - library:ci-flocq + - library:ci-mathcomp + - plugin:ci-bignums + +library:ci-oddorder: + extends: .ci-template-flambda + stage: stage-3 + needs: + - build:edge+flambda + - library:ci-mathcomp + dependencies: + - build:edge+flambda + - library:ci-mathcomp + +library:ci-fourcolor: + extends: .ci-template-flambda + stage: stage-3 + needs: + - build:edge+flambda + - library:ci-mathcomp + dependencies: + - build:edge+flambda + - library:ci-mathcomp + library:ci-corn: extends: .ci-template-flambda stage: stage-4 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/Makefile.ci b/Makefile.ci index af78f252df..9f08de662f 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -34,14 +34,18 @@ CI_TARGETS= \ ci-fiat_crypto_ocaml \ ci-fiat_parsers \ ci-flocq \ + ci-fourcolor \ ci-geocoq \ ci-coqhammer \ ci-hott \ + ci-interval \ ci-iris \ ci-math_classes \ ci-mathcomp \ + ci-menhir \ ci-metacoq \ ci-mtac2 \ + ci-oddorder \ ci-paramcoq \ ci-perennial \ ci-quickchick \ @@ -68,7 +72,7 @@ ci-all: $(CI_TARGETS) ci-color: ci-bignums ci-coqprime: ci-bignums - +ci-coquelicot: ci-mathcomp ci-math_classes: ci-bignums ci-corn: ci-math_classes @@ -78,6 +82,10 @@ ci-mtac2: ci-unicoq ci-fiat_crypto: ci-coqprime ci-rewriter ci-fiat_crypto_ocaml: ci-fiat_crypto +ci-interval: ci-mathcomp ci-flocq ci-coquelicot ci-bignums +ci-fourcolor: ci-mathcomp +ci-oddorder: ci-mathcomp + ci-simple_io: ci-ext_lib ci-quickchick: ci-ext_lib ci-simple_io @@ -85,6 +93,8 @@ ci-metacoq: ci-equations ci-vst: ci-flocq +ci-compcert: ci-menhir ci-flocq + # Generic rule, we use make to ease CI integration $(CI_TARGETS): ci-%: +./dev/ci/ci-wrapper.sh $* diff --git a/Makefile.ide b/Makefile.ide index 789acee5ec..9964a474f8 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -262,7 +262,7 @@ $(COQIDEAPP)/Contents/Resources/loaders: $(COQIDEAPP)/Contents $(COQIDEAPP)/Contents/Resources/immodules: $(COQIDEAPP)/Contents $(MKDIR) $@ - $(INSTALLLIB) "$(GTKLIBS)/gtk-3.0/3.0.0/immodules/"*.dylib $@ + $(INSTALLLIB) "$(GTKLIBS)/gtk-3.0/3.0.0/immodules/"*.dylib $@ || $(INSTALLLIB) "$(GTKLIBS)/gtk-3.0/3.0.0/immodules/"*.so $@ $(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib @@ -271,8 +271,9 @@ $(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib { "$(PIXBUFBIN)/gdk-pixbuf-query-loaders" $@/../loaders/*.so |\ sed -e "s!/.*\(/loaders/.*.so\)!@executable_path/../Resources/\1!"; } \ > $@/gtk-3.0/gdk-pixbuf.loaders - { "$(GTKBIN)/gtk-query-immodules-3.0" $@/../immodules/*.dylib |\ + { "$(GTKBIN)/gtk-query-immodules-3.0" $@/../immodules/*.{dylib,so} |\ sed -e "s!/.*\(/immodules/.*.dylib\)!@executable_path/../Resources/\1!" |\ + sed -e "s!/.*\(/immodules/.*.so\)!@executable_path/../Resources/\1!" |\ sed -e "s!/.*\(/share/locale\)!@executable_path/../Resources/\1!"; } \ > $@/gtk-3.0/gtk-immodules.loaders $(MKDIR) $@/pango @@ -281,7 +282,7 @@ $(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib $(COQIDEAPP)/Contents/Resources/lib: $(COQIDEAPP)/Contents/Resources/immodules $(COQIDEAPP)/Contents/Resources/loaders $(COQIDEAPP)/Contents $(COQIDEINAPP) $(MKDIR) $@ macpack -d ../Resources/lib $(COQIDEINAPP) - for i in $@/../loaders/*.so $@/../immodules/*.dylib; \ + for i in $@/../loaders/*.so $@/../immodules/*.{dylib,so}; \ do \ macpack -d ../lib $$i; \ done diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 46bd4367a7..11f225bdb6 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -100,17 +100,17 @@ jobs: make install displayName: 'Install Coq' -# - script: | -# set -e -# eval $(opam env) -# export PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig -# ./dev/build/osx/make-macos-dmg.sh -# mv _build/*.dmg "$(Build.ArtifactStagingDirectory)/" -# displayName: 'Create the dmg bundle' -# env: -# OUTDIR: '$(Build.BinariesDirectory)' - -# - task: PublishBuildArtifacts@1 -# inputs: -# pathtoPublish: '$(Build.ArtifactStagingDirectory)' -# artifactName: coq-macOS-installer + - script: | + set -e + eval $(opam env) + export PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig + ./dev/build/osx/make-macos-dmg.sh + mv _build/*.dmg "$(Build.ArtifactStagingDirectory)/" + displayName: 'Create the dmg bundle' + env: + OUTDIR: '$(Build.BinariesDirectory)' + + - task: PublishBuildArtifacts@1 + inputs: + pathtoPublish: '$(Build.ArtifactStagingDirectory)' + artifactName: coq-macOS-installer 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/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 6f6b3cd6d2..ebbf10f548 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1200,7 +1200,7 @@ function make_elpi { make_dune make_re - if build_prep https://github.com/LPCIC/elpi/archive v1.11.4 tar.gz 1 elpi; then + if build_prep https://github.com/LPCIC/elpi/archive v1.12.0 tar.gz 1 elpi; then log2 dune build -p elpi log2 dune install elpi @@ -1749,7 +1749,7 @@ function make_addon_compcert { installer_addon_dependency_end if build_prep_overlay compcert; then installer_addon_section compcert "CompCert" "ATTENTION: THIS IS NOT OPEN SOURCE! CompCert verified C compiler and Clightgen (required for using VST for your own code)" "off" - logn configure ./configure -ignore-coq-version -clightgen -prefix "$PREFIXCOQ" -coqdevdir "$PREFIXCOQ/lib/coq/user-contrib/compcert" x86_32-cygwin + logn configure ./configure -ignore-coq-version -clightgen -prefix "$PREFIXCOQ" -coqdevdir "$PREFIXCOQ/lib/coq/user-contrib/compcert" x86_32-cygwin -use-external-MenhirLib -use-external-Flocq log1 make $MAKE_OPT log2 make install logn install-license-1 install -D -T "LICENSE" "$PREFIXCOQ/lib/coq/user-contrib/compcert/LICENSE" diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 75d9efaadc..18fdd83218 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -306,7 +306,7 @@ # menhirlib ######################################################################## # Note: menhirlib is now in subfolder coq-menhirlib of menhir -: "${menhirlib_CI_REF:=master}" +: "${menhirlib_CI_REF:=20201122}" : "${menhirlib_CI_GITURL:=https://gitlab.inria.fr/fpottier/menhir}" : "${menhirlib_CI_ARCHIVEURL:=${menhirlib_CI_GITURL}/-/archive}" diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index b85261d7fc..1a4ebc0e90 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -19,20 +19,20 @@ then elif [ -d "$PWD/_build/install/default/" ]; then # Dune build - export OCAMLPATH="$PWD/_build/install/default/lib/:$OCAMLPATH" + export OCAMLPATH="$PWD/_build/install/default/lib/:$PWD/_install_ci/lib:$OCAMLPATH" export COQBIN="$PWD/_build/install/default/bin" export COQLIB="$PWD/_build/install/default/lib/coq" CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" export CI_BRANCH else # We assume we are in `-profile devel` build, thus `-local` is set - export OCAMLPATH="$PWD:$OCAMLPATH" + export OCAMLPATH="$PWD:$PWD/_install_ci/lib:$OCAMLPATH" export COQBIN="$PWD/bin" CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" export CI_BRANCH fi -export PATH="$COQBIN:$PATH" +export PATH="$COQBIN:$PWD/_install_ci/bin:$PATH" # Coq's tools need an ending slash :S, we should fix them. export COQBIN="$COQBIN/" @@ -42,6 +42,9 @@ ls -l "$COQBIN" # Where we download and build external developments CI_BUILD_DIR="$PWD/_build_ci" +# Where we install external binaries and ocaml libraries +CI_INSTALL_DIR="$PWD/_install_ci" + ls -l "$CI_BUILD_DIR" || true declare -A overlays diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index 6b09726606..3c8d65f5c1 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -7,6 +7,6 @@ git_download compcert export COQCOPTS='-native-compiler no -w -undeclared-scope -w -omega-is-deprecated' ( cd "${CI_BUILD_DIR}/compcert" && \ - ./configure -ignore-coq-version x86_32-linux && \ + ./configure -ignore-coq-version x86_32-linux -use-external-MenhirLib -use-external-Flocq && \ make && \ make check-proof COQCHK='"$(COQBIN)coqchk" -silent -o $(COQINCLUDES)') diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh index ffe92dcecf..777d36a6d7 100755 --- a/dev/ci/ci-coquelicot.sh +++ b/dev/ci/ci-coquelicot.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -install_ssreflect - git_download coquelicot -( cd "${CI_BUILD_DIR}/coquelicot" && autoreconf -i -s && ./configure && ./remake "-j${NJOBS}" ) +( cd "${CI_BUILD_DIR}/coquelicot" && ( if [ ! -x ./configure ]; then autoreconf -i -s && ./configure; fi ) && ./remake "-j${NJOBS}" && ./remake install ) diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh index a3a704091b..cb6c3e6452 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")" git_download flocq -( cd "${CI_BUILD_DIR}/flocq" && autoconf && ./configure && ./remake "-j${NJOBS}" && ./remake install ) +( cd "${CI_BUILD_DIR}/flocq" && ( if [ ! -x ./configure ]; then autoconf && ./configure; fi ) && ./remake "-j${NJOBS}" && ./remake install ) diff --git a/dev/ci/ci-fourcolor.sh b/dev/ci/ci-fourcolor.sh new file mode 100755 index 0000000000..72a1567398 --- /dev/null +++ b/dev/ci/ci-fourcolor.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download fourcolor + +( cd "${CI_BUILD_DIR}/fourcolor" && make && make install ) diff --git a/dev/ci/ci-interval.sh b/dev/ci/ci-interval.sh new file mode 100755 index 0000000000..fe7b3f9fbe --- /dev/null +++ b/dev/ci/ci-interval.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download interval + +export COQEXTRAFLAGS='-native-compiler no' +( cd "${CI_BUILD_DIR}/interval" && ( if [ ! -x ./configure ]; then autoconf && ./configure; fi ) && ./remake "-j${NJOBS}" && ./remake install ) diff --git a/dev/ci/ci-mathcomp.sh b/dev/ci/ci-mathcomp.sh index b1aa56ec4e..f170b35327 100755 --- a/dev/ci/ci-mathcomp.sh +++ b/dev/ci/ci-mathcomp.sh @@ -7,11 +7,3 @@ ci_dir="$(dirname "$0")" git_download mathcomp ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && make && make test-suite && make install ) - -git_download fourcolor - -( cd "${CI_BUILD_DIR}/fourcolor" && make && make install ) - -git_download oddorder - -( cd "${CI_BUILD_DIR}/oddorder" && make ) diff --git a/dev/ci/ci-menhir.sh b/dev/ci/ci-menhir.sh new file mode 100755 index 0000000000..5ad78383d8 --- /dev/null +++ b/dev/ci/ci-menhir.sh @@ -0,0 +1,8 @@ +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download menhirlib + +( cd "${CI_BUILD_DIR}/menhirlib" && dune build @install -p menhirLib,menhirSdk,menhir && dune install -p menhirLib,menhirSdk,menhir menhir menhirSdk menhirLib --prefix=${CI_INSTALL_DIR} ) + +( cd "${CI_BUILD_DIR}/menhirlib" && make -C coq-menhirlib && make -C coq-menhirlib install ) diff --git a/dev/ci/ci-oddorder.sh b/dev/ci/ci-oddorder.sh new file mode 100755 index 0000000000..b2da32ad61 --- /dev/null +++ b/dev/ci/ci-oddorder.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download oddorder + +( cd "${CI_BUILD_DIR}/oddorder" && make && make install ) diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index c17ec502e7..85107780f1 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-10-12-V89" +# CACHEKEY: "bionic_coq-V2020-11-26-V92" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -42,8 +42,8 @@ ENV COMPILER="4.05.0" # Common OPAM packages ENV BASE_OPAM="zarith.1.10 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \ - CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \ - BASE_ONLY_OPAM="elpi.1.11.4" + CI_OPAM="ocamlgraph.1.8.8" \ + BASE_ONLY_OPAM="elpi.1.12.0" # BASE switch; CI_OPAM contains Coq's CI dependencies. ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0" @@ -62,7 +62,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ # EDGE switch ENV COMPILER_EDGE="4.11.1" \ - BASE_OPAM_EDGE="dune.2.5.1 dune-release.1.3.3 ocamlformat.0.15.0" + BASE_OPAM_EDGE="dune.2.5.1 dune-release.1.3.3" # EDGE+flambda switch, we install CI_OPAM as to be able to use # `ci-template-flambda` with everything. diff --git a/dev/ci/user-overlays/13415-SkySkimmer-intern-univs.sh b/dev/ci/user-overlays/13415-SkySkimmer-intern-univs.sh new file mode 100644 index 0000000000..0bf806085e --- /dev/null +++ b/dev/ci/user-overlays/13415-SkySkimmer-intern-univs.sh @@ -0,0 +1,8 @@ +if [ "$CI_PULL_REQUEST" = "13415" ] || [ "$CI_BRANCH" = "intern-univs" ]; then + + overlay equations https://github.com/SkySkimmer/Coq-Equations intern-univs + + overlay paramcoq https://github.com/SkySkimmer/paramcoq intern-univs + + overlay elpi https://github.com/SkySkimmer/coq-elpi intern-univs +fi diff --git a/dev/ci/user-overlays/13481-elpi-1.12.sh b/dev/ci/user-overlays/13481-elpi-1.12.sh new file mode 100644 index 0000000000..a6be2e3a1a --- /dev/null +++ b/dev/ci/user-overlays/13481-elpi-1.12.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "13481" ] || [ "$CI_BRANCH" = "elpi-1.12" ]; then + + elpi_CI_REF=coq-master+elpi.1.12 + elpi_hb_CI_REF=coq-master+coq-elpi-1.7.0+elpi-1.12 + +fi 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/dev/top_printers.ml b/dev/top_printers.ml index a9438c4aca..4faa12af79 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -27,6 +27,11 @@ let _ = Detyping.print_evar_arguments := true let _ = Detyping.print_universes := true let _ = Goptions.set_bool_option_value ["Printing";"Matching"] false +let with_env_evm f x = + let env = Global.env() in + let sigma = Evd.from_env env in + f env sigma x + (* std_ppcmds *) let pp x = Pp.pp_with !Topfmt.std_ft x @@ -75,7 +80,7 @@ let ppeconstr x = pp (pr_econstr x) let ppconstr_expr x = let sigma,env = get_current_context () in pp (Ppconstr.pr_constr_expr env sigma x) let ppsconstr x = ppconstr (Mod_subst.force_constr x) let ppconstr_univ x = Constrextern.with_universes ppconstr x -let ppglob_constr = (fun x -> pp(pr_lglob_constr_env (Global.env()) x)) +let ppglob_constr = (fun x -> pp(with_env_evm pr_lglob_constr_env x)) let pppattern = (fun x -> pp(envpp pr_constr_pattern_env x)) let pptype = (fun x -> try pp(envpp (fun env evm t -> pr_ltype_env env evm t) x) with e -> pp (str (Printexc.to_string e))) let ppfconstr c = ppconstr (CClosure.term_of_fconstr c) @@ -130,7 +135,7 @@ let rec pr_closure {idents=idents;typed=typed;untyped=untyped} = and pr_closed_glob_constr_idmap x = pridmap (fun _ -> pr_closed_glob_constr) x and pr_closed_glob_constr {closure=closure;term=term} = - pr_closure closure ++ (pr_lglob_constr_env Global.(env ())) term + pr_closure closure ++ with_env_evm pr_lglob_constr_env term let ppclosure x = pp (pr_closure x) let ppclosedglobconstr x = pp (pr_closed_glob_constr x) @@ -212,7 +217,7 @@ let pproof p = pp(Proof.pr_proof p) let ppuni u = pp(Universe.pr u) let ppuni_level u = pp (Level.pr u) -let prlev = UnivNames.pr_with_global_universes +let prlev = UnivNames.pr_with_global_universes Id.Map.empty let ppuniverse_set l = pp (LSet.pr prlev l) let ppuniverse_instance l = pp (Instance.pr prlev l) let ppuniverse_context l = pp (pr_universe_context prlev l) diff --git a/doc/changelog/03-notations/13415-intern-univs.rst b/doc/changelog/03-notations/13415-intern-univs.rst new file mode 100644 index 0000000000..e9f51461e5 --- /dev/null +++ b/doc/changelog/03-notations/13415-intern-univs.rst @@ -0,0 +1,5 @@ +- **Fixed:** Notations understand universe names without getting + confused by different imported modules between declaration and use + locations (`#13415 <https://github.com/coq/coq/pull/13415>`_, fixes + `#13303 <https://github.com/coq/coq/issues/13303>`_, by Gaëtan + Gilbert). 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/engine/evar_kinds.ml b/engine/evar_kinds.ml index 71d68f739e..fb41c4491e 100644 --- a/engine/evar_kinds.ml +++ b/engine/evar_kinds.ml @@ -40,6 +40,7 @@ type t = | ImplicitArg of GlobRef.t * (int * Id.t option) * bool (** Force inference *) | BinderType of Name.t + | EvarType of Id.t option * Evar.t (* type of an optionally named evar *) | NamedHole of Id.t (* coming from some ?[id] syntax *) | QuestionMark of question_mark | CasesType of bool (* true = a subterm of the type *) diff --git a/engine/evar_kinds.mli b/engine/evar_kinds.mli index ffc57cfd15..b2b39d49be 100644 --- a/engine/evar_kinds.mli +++ b/engine/evar_kinds.mli @@ -39,6 +39,7 @@ type t = | ImplicitArg of GlobRef.t * (int * Id.t option) * bool (** Force inference *) | BinderType of Name.t + | EvarType of Id.t option * Evar.t (* type of an optionally named evar *) | NamedHole of Id.t (* coming from some ?[id] syntax *) | QuestionMark of question_mark | CasesType of bool (* true = a subterm of the type *) diff --git a/engine/evd.ml b/engine/evd.ml index 498a9d9825..59eea97ce9 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1231,6 +1231,11 @@ let restrict evk filter ?candidates ?src evd = let evd = declare_future_goal evk' evd in (evd, evk') +let update_source evd evk src = + let evar_info = EvMap.find evk evd.undf_evars in + let evar_info' = { evar_info with evar_source = src } in + { evd with undf_evars = EvMap.add evk evar_info' evd.undf_evars } + (**********************************************************) (* Accessing metas *) diff --git a/engine/evd.mli b/engine/evd.mli index 1c5c65924c..911e00c23a 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -290,6 +290,10 @@ val restrict : Evar.t-> Filter.t -> ?candidates:econstr list -> possibly limiting the instances to a set of candidates (candidates are filtered according to the filter) *) +val update_source : evar_map -> Evar.t -> Evar_kinds.t located -> evar_map +(** To update the source a posteriori, e.g. when an evar type of + another evar has to refer to this other evar, with a mutual dependency *) + val get_aliased_evars : evar_map -> Evar.t Evar.Map.t (** The map of aliased evars *) diff --git a/engine/termops.ml b/engine/termops.ml index 693945d5ac..ccd49ca495 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -123,6 +123,13 @@ let pr_evar_source env sigma = function str "subterm of pattern-matching return predicate" | Evar_kinds.BinderType (Name id) -> str "type of " ++ Id.print id | Evar_kinds.BinderType Anonymous -> str "type of anonymous binder" + | Evar_kinds.EvarType (ido,evk) -> + let pp = match ido with + | Some id -> str "?" ++ Id.print id + | None -> + try pr_existential_key sigma evk + with (* defined *) Not_found -> str "an internal placeholder" in + str "type of " ++ pp | Evar_kinds.ImplicitArg (c,(n,ido),b) -> let open Globnames in let print_constr = print_kconstr in diff --git a/engine/uState.ml b/engine/uState.ml index 103b552d86..0c994dfea0 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -341,12 +341,16 @@ let constrain_variables diff uctx = in { uctx with local = (univs, local); univ_variables = vars } -let qualid_of_level uctx = +let id_of_level uctx l = + try Some (Option.get (LMap.find l (snd uctx.names)).uname) + with Not_found | Option.IsNone -> + None + +let qualid_of_level uctx l = let map, map_rev = uctx.names in - fun l -> - try Some (Libnames.qualid_of_ident (Option.get (LMap.find l map_rev).uname)) - with Not_found | Option.IsNone -> - UnivNames.qualid_of_level l + try Some (Libnames.qualid_of_ident (Option.get (LMap.find l map_rev).uname)) + with Not_found | Option.IsNone -> + UnivNames.qualid_of_level map l let pr_uctx_level uctx l = match qualid_of_level uctx l with diff --git a/engine/uState.mli b/engine/uState.mli index bd3aac0d8b..442c29180c 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -209,4 +209,7 @@ val update_sigma_univs : t -> UGraph.t -> t val pr_uctx_level : t -> Univ.Level.t -> Pp.t val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid option +(** Only looks in the local names, not in the nametab. *) +val id_of_level : t -> Univ.Level.t -> Id.t option + val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t diff --git a/engine/univNames.ml b/engine/univNames.ml index 2e15558db2..f5542cc0f7 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -12,15 +12,15 @@ open Names open Univ -let qualid_of_level l = +let qualid_of_level ctx l = match Level.name l with | Some qid -> - (try Some (Nametab.shortest_qualid_of_universe qid) + (try Some (Nametab.shortest_qualid_of_universe (Id.Map.domain ctx) qid) with Not_found -> None) | None -> None -let pr_with_global_universes l = - match qualid_of_level l with +let pr_with_global_universes ctx l = + match qualid_of_level ctx l with | Some qid -> Libnames.pr_qualid qid | None -> Level.pr l diff --git a/engine/univNames.mli b/engine/univNames.mli index 5f69d199b3..875c043032 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -10,9 +10,6 @@ open Univ -val pr_with_global_universes : Level.t -> Pp.t -val qualid_of_level : Level.t -> Libnames.qualid option - (** Local universe name <-> level mapping *) type universe_binders = Univ.Level.t Names.Id.Map.t @@ -20,3 +17,6 @@ type universe_binders = Univ.Level.t Names.Id.Map.t val empty_binders : universe_binders type univ_name_list = Names.lname list + +val pr_with_global_universes : universe_binders -> Level.t -> Pp.t +val qualid_of_level : universe_binders -> Level.t -> Libnames.qualid option diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index b3f06faa1c..b14c325f69 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -13,10 +13,23 @@ open Libnames (** {6 Concrete syntax for terms } *) -(** [constr_expr] is the abstract syntax tree produced by the parser *) -type universe_decl_expr = (lident list, Glob_term.glob_constraint list) UState.gen_universe_decl +(** Universes *) +type sort_name_expr = + | CSProp | CProp | CSet + | CType of qualid + | CRawType of Univ.Level.t (** Universes like "foo.1" have no qualid form *) + +type univ_level_expr = sort_name_expr Glob_term.glob_sort_gen +type sort_expr = (sort_name_expr * int) list Glob_term.glob_sort_gen + +type instance_expr = univ_level_expr list + +(** Constraints don't have anonymous universes *) +type univ_constraint_expr = sort_name_expr * Univ.constraint_type * sort_name_expr + +type universe_decl_expr = (lident list, univ_constraint_expr list) UState.gen_universe_decl type cumul_univ_decl_expr = - ((lident * Univ.Variance.t option) list, Glob_term.glob_constraint list) UState.gen_universe_decl + ((lident * Univ.Variance.t option) list, univ_constraint_expr list) UState.gen_universe_decl type ident_decl = lident * universe_decl_expr option type cumul_ident_decl = lident * cumul_univ_decl_expr option @@ -64,8 +77,7 @@ type prim_token = | Number of NumTok.Signed.t | String of string -type instance_expr = Glob_term.glob_level list - +(** [constr_expr] is the abstract syntax tree produced by the parser *) type cases_pattern_expr_r = | CPatAlias of cases_pattern_expr * lname | CPatCstr of qualid @@ -114,7 +126,7 @@ and constr_expr_r = | CHole of Evar_kinds.t option * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option | CPatVar of Pattern.patvar | CEvar of Glob_term.existential_name CAst.t * (lident * constr_expr) list - | CSort of Glob_term.glob_sort + | CSort of sort_expr | CCast of constr_expr * constr_expr Glob_term.cast_type | CNotation of notation_with_optional_scope option * notation * constr_notation_substitution | CGeneralization of Glob_term.binding_kind * abstraction_kind option * constr_expr diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index a60dc11b57..f02874253e 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -18,6 +18,25 @@ open Glob_term open Notation open Constrexpr +(***********) +(* Universes *) + +let sort_name_expr_eq c1 c2 = match c1, c2 with + | CSProp, CSProp + | CProp, CProp + | CSet, CSet -> true + | CType q1, CType q2 -> Libnames.qualid_eq q1 q2 + | CRawType u1, CRawType u2 -> Univ.Level.equal u1 u2 + | (CSProp|CProp|CSet|CType _|CRawType _), _ -> false + +let univ_level_expr_eq u1 u2 = + Glob_ops.glob_sort_gen_eq sort_name_expr_eq u1 u2 + +let sort_expr_eq u1 u2 = + Glob_ops.glob_sort_gen_eq + (List.equal (fun (x,m) (y,n) -> sort_name_expr_eq x y && Int.equal m n)) + u1 u2 + (***********************) (* For binders parsing *) @@ -59,13 +78,11 @@ let explicitation_eq ex1 ex2 = match ex1, ex2 with Id.equal id1 id2 | _ -> false -let eq_ast f { CAst.v = x } { CAst.v = y } = f x y - let rec cases_pattern_expr_eq p1 p2 = if CAst.(p1.v == p2.v) then true else match CAst.(p1.v, p2.v) with | CPatAlias(a1,i1), CPatAlias(a2,i2) -> - eq_ast Name.equal i1 i2 && cases_pattern_expr_eq a1 a2 + CAst.eq Name.equal i1 i2 && cases_pattern_expr_eq a1 a2 | CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) -> qualid_eq c1 c2 && Option.equal (List.equal cases_pattern_expr_eq) a1 a2 && @@ -108,10 +125,10 @@ let rec constr_expr_eq e1 e2 = else match CAst.(e1.v, e2.v) with | CRef (r1,u1), CRef (r2,u2) -> qualid_eq r1 r2 && eq_universes u1 u2 | CFix(id1,fl1), CFix(id2,fl2) -> - eq_ast Id.equal id1 id2 && + lident_eq id1 id2 && List.equal fix_expr_eq fl1 fl2 | CCoFix(id1,fl1), CCoFix(id2,fl2) -> - eq_ast Id.equal id1 id2 && + lident_eq id1 id2 && List.equal cofix_expr_eq fl1 fl2 | CProdN(bl1,a1), CProdN(bl2,a2) -> List.equal local_binder_eq bl1 bl2 && @@ -120,7 +137,7 @@ let rec constr_expr_eq e1 e2 = List.equal local_binder_eq bl1 bl2 && constr_expr_eq a1 a2 | CLetIn(na1,a1,t1,b1), CLetIn(na2,a2,t2,b2) -> - eq_ast Name.equal na1 na2 && + CAst.eq Name.equal na1 na2 && constr_expr_eq a1 a2 && Option.equal constr_expr_eq t1 t2 && constr_expr_eq b1 b2 @@ -144,14 +161,14 @@ let rec constr_expr_eq e1 e2 = List.equal case_expr_eq a1 a2 && List.equal branch_expr_eq brl1 brl2 | CLetTuple (n1, (m1, e1), t1, b1), CLetTuple (n2, (m2, e2), t2, b2) -> - List.equal (eq_ast Name.equal) n1 n2 && - Option.equal (eq_ast Name.equal) m1 m2 && + List.equal (CAst.eq Name.equal) n1 n2 && + Option.equal (CAst.eq Name.equal) m1 m2 && Option.equal constr_expr_eq e1 e2 && constr_expr_eq t1 t2 && constr_expr_eq b1 b2 | CIf (e1, (n1, r1), t1, f1), CIf (e2, (n2, r2), t2, f2) -> constr_expr_eq e1 e2 && - Option.equal (eq_ast Name.equal) n1 n2 && + Option.equal (CAst.eq Name.equal) n1 n2 && Option.equal constr_expr_eq r1 r2 && constr_expr_eq t1 t2 && constr_expr_eq f1 f2 @@ -161,7 +178,7 @@ let rec constr_expr_eq e1 e2 = | CEvar (id1, c1), CEvar (id2, c2) -> Id.equal id1.CAst.v id2.CAst.v && List.equal instance_eq c1 c2 | CSort s1, CSort s2 -> - Glob_ops.glob_sort_eq s1 s2 + sort_expr_eq s1 s2 | CCast(t1,c1), CCast(t2,c2) -> constr_expr_eq t1 t2 && cast_expr_eq c1 c2 | CNotation(inscope1, n1, s1), CNotation(inscope2, n2, s2) -> @@ -187,12 +204,12 @@ let rec constr_expr_eq e1 e2 = | CGeneralization _ | CDelimiters _ | CArray _), _ -> false and args_eq (a1,e1) (a2,e2) = - Option.equal (eq_ast explicitation_eq) e1 e2 && + Option.equal (CAst.eq explicitation_eq) e1 e2 && constr_expr_eq a1 a2 and case_expr_eq (e1, n1, p1) (e2, n2, p2) = constr_expr_eq e1 e2 && - Option.equal (eq_ast Name.equal) n1 n2 && + Option.equal (CAst.eq Name.equal) n1 n2 && Option.equal cases_pattern_expr_eq p1 p2 and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} = @@ -200,35 +217,35 @@ and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} = constr_expr_eq e1 e2 and fix_expr_eq (id1,r1,bl1,a1,b1) (id2,r2,bl2,a2,b2) = - (eq_ast Id.equal id1 id2) && + (lident_eq id1 id2) && Option.equal recursion_order_expr_eq r1 r2 && List.equal local_binder_eq bl1 bl2 && constr_expr_eq a1 a2 && constr_expr_eq b1 b2 and cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) = - (eq_ast Id.equal id1 id2) && + (lident_eq id1 id2) && List.equal local_binder_eq bl1 bl2 && constr_expr_eq a1 a2 && constr_expr_eq b1 b2 and recursion_order_expr_eq_r r1 r2 = match r1, r2 with - | CStructRec i1, CStructRec i2 -> eq_ast Id.equal i1 i2 + | CStructRec i1, CStructRec i2 -> lident_eq i1 i2 | CWfRec (i1,e1), CWfRec (i2,e2) -> constr_expr_eq e1 e2 | CMeasureRec (i1, e1, o1), CMeasureRec (i2, e2, o2) -> - Option.equal (eq_ast Id.equal) i1 i2 && + Option.equal lident_eq i1 i2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq o1 o2 | _ -> false -and recursion_order_expr_eq r1 r2 = eq_ast recursion_order_expr_eq_r r1 r2 +and recursion_order_expr_eq r1 r2 = CAst.eq recursion_order_expr_eq_r r1 r2 and local_binder_eq l1 l2 = match l1, l2 with | CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) -> - eq_ast Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 + CAst.eq Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 | CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) -> (* Don't care about the [binder_kind] *) - List.equal (eq_ast Name.equal) n1 n2 && constr_expr_eq e1 e2 + List.equal (CAst.eq Name.equal) n1 n2 && constr_expr_eq e1 e2 | _ -> false and constr_notation_substitution_eq (e1, el1, b1, bl1) (e2, el2, b2, bl2) = diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index dfa51918d1..ffa7c8ec10 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -16,6 +16,10 @@ open Constrexpr (** {6 Equalities on [constr_expr] related types} *) +val sort_name_expr_eq : sort_name_expr -> sort_name_expr -> bool +val univ_level_expr_eq : univ_level_expr -> univ_level_expr -> bool +val sort_expr_eq : sort_expr -> sort_expr -> bool + val explicitation_eq : explicitation -> explicitation -> bool (** Equality on [explicitation]. *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 378adb566c..3969c7ea1f 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -923,22 +923,44 @@ let extern_float f scopes = (**********************************************************************) (* mapping glob_constr to constr_expr *) -let extern_glob_sort = function +type extern_env = Id.Set.t * UnivNames.universe_binders +let extern_env env sigma = vars_of_env env, Evd.universe_binders sigma +let empty_extern_env = Id.Set.empty, Id.Map.empty + +let extern_glob_sort_name uvars = function + | GSProp -> CSProp + | GProp -> CProp + | GSet -> CSet + | GLocalUniv u -> CType (qualid_of_lident u) + | GRawUniv u -> CRawType u + | GUniv u -> begin match UnivNames.qualid_of_level uvars u with + | Some qid -> CType qid + | None -> CRawType u + end + +let extern_glob_sort uvars = + map_glob_sort_gen (List.map (on_fst (extern_glob_sort_name uvars))) + +(** wrapper to handle print_universes: don't forget small univs *) +let extern_glob_sort uvars = function (* In case we print a glob_constr w/o having passed through detyping *) - | UNamed [(GSProp,0) | (GProp,0) | (GSet,0)] as u -> u + | UNamed [(GSProp,0) | (GProp,0) | (GSet,0)] as u -> extern_glob_sort uvars u | UNamed _ when not !print_universes -> UAnonymous {rigid=true} - | UNamed _ | UAnonymous _ as u -> u + | UNamed _ | UAnonymous _ as u -> extern_glob_sort uvars u -let extern_universes = function - | Some _ as l when !print_universes -> l +let extern_instance uvars = function + | Some l when !print_universes -> + Some (List.map (map_glob_sort_gen (extern_glob_sort_name uvars)) l) | _ -> None -let extern_ref vars ref us = +let extern_ref (vars,uvars) ref us = extern_global (select_stronger_impargs (implicits_of_global ref)) - (extern_reference vars ref) (extern_universes us) + (extern_reference vars ref) (extern_instance uvars us) let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None) +let add_vname (vars,uvars) na = add_vname vars na, uvars + let rec extern inctx ?impargs scopes vars r = match remove_one_coercion inctx (flatten_application r) with | Some (nargs,inctx,r') -> @@ -995,7 +1017,7 @@ let rec extern inctx ?impargs scopes vars r = (* Otherwise... *) extern_applied_ref inctx (select_stronger_impargs (implicits_of_global ref)) - (ref,extern_reference ?loc vars ref) (extern_universes us) args) + (ref,extern_reference ?loc (fst vars) ref) (extern_instance (snd vars) us) args) | _ -> let args = List.map (fun c -> (sub_extern true scopes vars c,None)) args in let head = sub_extern false scopes vars f in @@ -1015,7 +1037,8 @@ let rec extern inctx ?impargs scopes vars r = | GCases (sty,rtntypopt,tml,eqns) -> let vars' = List.fold_right (Name.fold_right Id.Set.add) - (cases_predicate_names tml) vars in + (cases_predicate_names tml) (fst vars) in + let vars' = vars', snd vars in let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in let tml = List.map (fun (tm,(na,x)) -> let na' = match na, DAst.get tm with @@ -1035,7 +1058,7 @@ let rec extern inctx ?impargs scopes vars r = Option.map (fun {CAst.loc;v=(ind,nal)} -> let args = List.map (fun x -> DAst.make @@ PatVar x) nal in let fullargs = add_cpatt_for_params ind args in - extern_ind_pattern_in_scope scopes vars ind fullargs + extern_ind_pattern_in_scope scopes (fst vars) ind fullargs ) x)) tml in @@ -1058,7 +1081,7 @@ let rec extern inctx ?impargs scopes vars r = sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2) | GRec (fk,idv,blv,tyv,bv) -> - let vars' = Array.fold_right Id.Set.add idv vars in + let vars' = on_fst (Array.fold_right Id.Set.add idv) vars in (match fk with | GFix (nv,n) -> let listdecl = @@ -1066,8 +1089,8 @@ let rec extern inctx ?impargs scopes vars r = let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in let bl = List.map (extended_glob_local_binder_of_decl ?loc) bl in let (assums,ids,bl) = extern_local_binder scopes vars bl in - let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in - let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in + let vars0 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars in + let vars1 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars' in let n = match nv.(i) with | None -> None @@ -1082,14 +1105,14 @@ let rec extern inctx ?impargs scopes vars r = Array.mapi (fun i fi -> let bl = List.map (extended_glob_local_binder_of_decl ?loc) blv.(i) in let (_,ids,bl) = extern_local_binder scopes vars bl in - let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in - let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in + let vars0 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars in + let vars1 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars' in ((CAst.make fi),bl,extern_typ scopes vars0 tyv.(i), sub_extern true scopes vars1 bv.(i))) idv in CCoFix (CAst.(make ?loc idv.(n)),Array.to_list listdecl)) - | GSort s -> CSort (extern_glob_sort s) + | GSort s -> CSort (extern_glob_sort (snd vars) s) | GHole (e,naming,_) -> CHole (Some e, naming, None) (* TODO: extern tactics. *) @@ -1105,7 +1128,7 @@ let rec extern inctx ?impargs scopes vars r = | GFloat f -> extern_float f (snd scopes) | GArray(u,t,def,ty) -> - CArray(extern_universes u,Array.map (extern inctx scopes vars) t, extern inctx scopes vars def, extern_typ scopes vars ty) + CArray(extern_instance (snd vars) u,Array.map (extern inctx scopes vars) t, extern inctx scopes vars def, extern_typ scopes vars ty) in insert_entry_coercion coercion (CAst.make ?loc c) @@ -1127,7 +1150,7 @@ and factorize_prod ?impargs scopes vars na bk t c = let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in let b = extern_typ scopes vars b in - let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in + let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes (fst vars)) disjpat) in let binder = CLocalPattern p in (match b.v with | CProdN (bl,b) -> CProdN (binder::bl,b) @@ -1168,7 +1191,7 @@ and factorize_lambda inctx scopes vars na bk t c = let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in let b = sub_extern inctx scopes vars b in - let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in + let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes (fst vars)) disjpat) in let binder = CLocalPattern p in (match b.v with | CLambdaN (bl,b) -> CLambdaN (binder::bl,b) @@ -1196,7 +1219,7 @@ and extern_local_binder scopes vars = function match DAst.get b with | GLocalDef (na,bk,bd,ty) -> let (assums,ids,l) = - extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l in + extern_local_binder scopes (on_fst (Name.fold_right Id.Set.add na) vars) l in (assums,na::ids, CLocalDef(CAst.make na, extern false scopes vars bd, Option.map (extern_typ scopes vars) ty) :: l) @@ -1204,7 +1227,7 @@ and extern_local_binder scopes vars = function | GLocalAssum (na,bk,ty) -> let implicit_type = is_reserved_type na ty in let ty = extern_typ scopes vars ty in - (match extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l with + (match extern_local_binder scopes (on_fst (Name.fold_right Id.Set.add na) vars) l with (assums,ids,CLocalAssum(nal,k,ty')::l) when (constr_expr_eq ty ty' || implicit_type && constr_expr_eq ty' hole) && match na with Name id -> not (occur_var_constr_expr id ty') @@ -1219,7 +1242,7 @@ and extern_local_binder scopes vars = function | GLocalPattern ((p,_),_,bk,ty) -> let ty = if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in - let p = mkCPatOr (List.map (extern_cases_pattern vars) p) in + let p = mkCPatOr (List.map (extern_cases_pattern (fst vars)) p) in let (assums,ids,l) = extern_local_binder scopes vars l in let p = match ty with | None -> p @@ -1227,7 +1250,7 @@ and extern_local_binder scopes vars = function (assums,ids, CLocalPattern p :: l) and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} = - let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in + let pll = List.map (List.map (extern_cases_pattern_in_scope scopes (fst vars))) pll in make ?loc (pll,extern inctx scopes vars c) and extern_notations inctx scopes vars nargs t = @@ -1277,6 +1300,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules = end | AppBoundedNotation _ -> raise No_match in (* Try matching ... *) + let vars, uvars = vars in let terms,termlists,binders,binderlists = match_notation_constr ~print_univ:(!print_universes) t ~vars pat in (* Try availability of interpretation ... *) @@ -1300,35 +1324,43 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules = let l = List.map (fun ((vars,c),(subentry,(scopt,scl))) -> extern (* assuming no overloading: *) true - (subentry,(scopt,scl@scopes')) vars c) - terms in + (subentry,(scopt,scl@scopes')) (vars,uvars) c) + terms + in let ll = List.map (fun ((vars,l),(subentry,(scopt,scl))) -> - List.map (extern true (subentry,(scopt,scl@scopes')) vars) l) - termlists in + List.map (extern true (subentry,(scopt,scl@scopes')) (vars,uvars)) l) + termlists + in let bl = List.map (fun ((vars,bl),(subentry,(scopt,scl))) -> - (mkCPatOr (List.map (extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars) bl)), - Explicit) - binders in + (mkCPatOr (List.map + (extern_cases_pattern_in_scope + (subentry,(scopt,scl@scopes')) vars) + bl)), + Explicit) + binders + in let bll = List.map (fun ((vars,bl),(subentry,(scopt,scl))) -> - pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl)) - binderlists in + pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) (vars,uvars) bl)) + binderlists + in let c = make_notation loc specific_ntn (l,ll,bl,bll) in let c = insert_entry_coercion coercion (insert_delimiters c key) in let args = fill_arg_scopes args argsscopes allscopes in - let args = extern_args (extern true) vars args in + let args = extern_args (extern true) (vars,uvars) args in CAst.make ?loc @@ extern_applied_notation inctx nallargs argsimpls c args) | SynDefRule kn -> let l = List.map (fun ((vars,c),(subentry,(scopt,scl))) -> - extern true (subentry,(scopt,scl@snd scopes)) vars c) - terms in + extern true (subentry,(scopt,scl@snd scopes)) (vars,uvars) c) + terms + in let cf = Nametab.shortest_qualid_of_syndef ?loc vars kn in let a = CRef (cf,None) in let args = fill_arg_scopes args argsscopes allscopes in - let args = extern_args (extern true) vars args in + let args = extern_args (extern true) (vars,uvars) args in let c = CAst.make ?loc @@ extern_applied_syntactic_definition inctx nallargs argsimpls (a,cf) l args in if isCRef_no_univ c.CAst.v && entry_has_global custom then c else match availability_of_entry_coercion custom InConstrEntrySomeLevel with @@ -1348,7 +1380,7 @@ let extern_glob_type ?impargs vars c = let extern_constr ?lax ?(inctx=false) ?scope env sigma t = let r = Detyping.detype Detyping.Later ?lax false Id.Set.empty env sigma t in - let vars = vars_of_env env in + let vars = extern_env env sigma in extern inctx (InConstrEntrySomeLevel,(scope,[])) vars r let extern_constr_in_scope ?lax ?inctx scope env sigma t = @@ -1364,16 +1396,16 @@ let extern_type ?lax ?(goal_concl_style=false) env sigma ?impargs t = (* consideration; see namegen.ml for further details *) let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in let r = Detyping.detype Detyping.Later ?lax goal_concl_style avoid env sigma t in - extern_glob_type ?impargs (vars_of_env env) r + extern_glob_type ?impargs (extern_env env sigma) r -let extern_sort sigma s = extern_glob_sort (detype_sort sigma s) +let extern_sort sigma s = extern_glob_sort (Evd.universe_binders sigma) (detype_sort sigma s) let extern_closed_glob ?lax ?(goal_concl_style=false) ?(inctx=false) ?scope env sigma t = let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in let r = Detyping.detype_closed_glob ?lax goal_concl_style avoid env sigma t in - let vars = vars_of_env env in + let vars = extern_env env sigma in extern inctx (InConstrEntrySomeLevel,(scope,[])) vars r (******************************************************************) @@ -1491,10 +1523,13 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with GArray (None, Array.map glob_of t, glob_of def, glob_of ty) let extern_constr_pattern env sigma pat = - extern true (InConstrEntrySomeLevel,(None,[])) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat) + extern true (InConstrEntrySomeLevel,(None,[])) + (* XXX no vars? *) + (Id.Set.empty, Evd.universe_binders sigma) + (glob_of_pat Id.Set.empty env sigma pat) let extern_rel_context where env sigma sign = let a = detype_rel_context Detyping.Later where Id.Set.empty (names_of_rel_context env,env) sigma sign in - let vars = vars_of_env env in + let vars = extern_env env sigma in let a = List.map (extended_glob_local_binder_of_decl) a in pi3 (extern_local_binder (InConstrEntrySomeLevel,(None,[])) vars a) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index f85e49d2df..298b52f0be 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -23,9 +23,12 @@ open Ltac_pretype (** Translation of pattern, cases pattern, glob_constr and term into syntax trees for printing *) +type extern_env = Id.Set.t * UnivNames.universe_binders +val extern_env : env -> Evd.evar_map -> extern_env + val extern_cases_pattern : Id.Set.t -> 'a cases_pattern_g -> cases_pattern_expr -val extern_glob_constr : Id.Set.t -> 'a glob_constr_g -> constr_expr -val extern_glob_type : ?impargs:Glob_term.binding_kind list -> Id.Set.t -> 'a glob_constr_g -> constr_expr +val extern_glob_constr : extern_env -> 'a glob_constr_g -> constr_expr +val extern_glob_type : ?impargs:Glob_term.binding_kind list -> extern_env -> 'a glob_constr_g -> constr_expr val extern_constr_pattern : names_context -> Evd.evar_map -> constr_pattern -> constr_expr val extern_closed_glob : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> @@ -43,7 +46,7 @@ val extern_constr_in_scope : ?lax:bool -> ?inctx:bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid val extern_type : ?lax:bool -> ?goal_concl_style:bool -> env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> types -> constr_expr -val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort +val extern_sort : Evd.evar_map -> Sorts.t -> sort_expr val extern_rel_context : constr option -> env -> Evd.evar_map -> rel_context -> local_binder_expr list @@ -96,3 +99,6 @@ val toggle_scope_printing : val toggle_notation_printing : ?scope:Notation_term.scope_name -> notation:Constrexpr.notation -> activate:bool -> unit + +(** Probably shouldn't be used *) +val empty_extern_env : extern_env diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 0645636255..cf2f333596 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -254,9 +254,12 @@ let contract_curly_brackets_pat ntn (l,ll) = (* side effect; don't inline *) (InConstrEntry,!ntn'),(l,ll) +type local_univs = { bound : Univ.Level.t Id.Map.t; unb_univs : bool } + type intern_env = { - ids: Names.Id.Set.t; + ids: Id.Set.t; unb: bool; + local_univs: local_univs; tmp_scope: Notation_term.tmp_scope_name option; scopes: Notation_term.scope_name list; impls: internalization_env; @@ -1160,6 +1163,32 @@ let glob_sort_of_level (level: glob_level) : glob_sort = | UAnonymous {rigid} -> UAnonymous {rigid} | UNamed id -> UNamed [id,0] +let intern_sort_name ~local_univs = function + | CSProp -> GSProp + | CProp -> GProp + | CSet -> GSet + | CRawType u -> GRawUniv u + | CType qid -> + let is_id = qualid_is_ident qid in + let local = if not is_id then None + else Id.Map.find_opt (qualid_basename qid) local_univs.bound + in + match local with + | Some u -> GUniv u + | None -> + try GUniv (Univ.Level.make (Nametab.locate_universe qid)) + with Not_found -> + if is_id && local_univs.unb_univs + then GLocalUniv (CAst.make ?loc:qid.loc (qualid_basename qid)) + else + CErrors.user_err Pp.(str "Undeclared universe " ++ pr_qualid qid ++ str".") + +let intern_sort ~local_univs s = + map_glob_sort_gen (List.map (on_fst (intern_sort_name ~local_univs))) s + +let intern_instance ~local_univs us = + Option.map (List.map (map_glob_sort_gen (intern_sort_name ~local_univs))) us + (* Is it a global reference or a syntactic definition? *) let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = let loc = qid.loc in @@ -1225,6 +1254,7 @@ let check_applied_projection isproj realref qid = let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us args qid = let loc = qid.CAst.loc in + let us = intern_instance ~local_univs:env.local_univs us in if qualid_is_ident qid then try let res = intern_var env lvar namedctx loc (qualid_basename qid) us in @@ -1256,7 +1286,8 @@ let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us let interp_reference vars r = let (r,_,_),_ = intern_applied_reference ~isproj:None (fun _ -> error_not_enough_arguments ?loc:None) - {ids = Id.Set.empty; unb = false ; + {ids = Id.Set.empty; unb = false; + local_univs = { bound=Id.Map.empty; unb_univs = false };(* <- doesn't matter here *) tmp_scope = None; scopes = []; impls = empty_internalization_env; binder_block_names = None} Environ.empty_named_context_val @@ -2269,12 +2300,12 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (* end *) | CSort s -> DAst.make ?loc @@ - GSort s + GSort (intern_sort ~local_univs:env.local_univs s) | CCast (c1, c2) -> DAst.make ?loc @@ GCast (intern env c1, map_cast_type (intern_type (slide_binders env)) c2) | CArray(u,t,def,ty) -> - DAst.make ?loc @@ GArray(u, Array.map (intern env) t, intern env def, intern env ty) + DAst.make ?loc @@ GArray(intern_instance ~local_univs:env.local_univs u, Array.map (intern env) t, intern env def, intern env ty) ) and intern_type env = intern (set_type_scope env) @@ -2446,6 +2477,8 @@ let extract_ids env = (Termops.ids_of_rel_context (Environ.rel_context env)) Id.Set.empty +let bound_univs sigma = Evd.universe_binders sigma + let scope_of_type_kind env sigma = function | IsType -> Notation.current_type_scope_name () | OfType typ -> compute_type_scope env sigma typ @@ -2468,8 +2501,9 @@ let intern_gen kind env sigma let tmp_scope = scope_of_type_kind env sigma kind in let k = allowed_binder_kind_of_type_kind kind in internalize env {ids = extract_ids env; unb = false; - tmp_scope = tmp_scope; scopes = []; - impls; binder_block_names = Some (k,Id.Map.domain impls)} + local_univs = { bound = bound_univs sigma; unb_univs = true }; + tmp_scope = tmp_scope; scopes = []; + impls; binder_block_names = Some (k,Id.Map.domain impls)} pattern_mode (ltacvars, Id.Map.empty) c let intern_constr env sigma c = intern_gen WithoutTypeConstraint env sigma c @@ -2558,7 +2592,9 @@ let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) let impls = empty_internalization_env in let k = allowed_binder_kind_of_type_kind kind in internalize env - {ids; unb = false; tmp_scope; scopes = []; impls; + {ids; unb = false; + local_univs = { bound = bound_univs sigma; unb_univs = true }; + tmp_scope; scopes = []; impls; binder_block_names = Some (k,Id.Set.empty)} pattern_mode (ltacvars, vl) c @@ -2568,8 +2604,11 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in let c = internalize env - {ids; unb = false; tmp_scope = None; scopes = []; impls; binder_block_names = None} - false (empty_ltac_sign, vl) a in + {ids; unb = false; + local_univs = { bound = Id.Map.empty; unb_univs = false }; + tmp_scope = None; scopes = []; impls; binder_block_names = None} + false (empty_ltac_sign, vl) a + in (* Splits variables into those that are binding, bound, or both *) (* Translate and check that [c] has all its free variables bound in [vars] *) let a, reversible = notation_constr_of_glob_constr nenv c in @@ -2596,7 +2635,7 @@ let interp_binder_evars env sigma na t = let my_intern_constr env lvar acc c = internalize env acc false lvar c -let intern_context env impl_env binders = +let intern_context env ~bound_univs impl_env binders = let lvar = (empty_ltac_sign, Id.Map.empty) in let ids = (* We assume all ids around are parts of the prefix of the current @@ -2607,6 +2646,7 @@ let intern_context env impl_env binders = let (env, bl) = intern_local_binder_aux (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in (env, bl)) ({ids; unb = false; + local_univs = { bound = bound_univs; unb_univs = true }; tmp_scope = None; scopes = []; impls = impl_env; binder_block_names = Some (Some AbsPi,ids)}, []) binders in (lenv.impls, List.map glob_local_binder_of_extended bl) @@ -2643,17 +2683,21 @@ let interp_glob_context_evars ?(program_mode=false) env sigma bl = sigma, ((env, par), List.rev impls) let interp_context_evars ?program_mode ?(impl_env=empty_internalization_env) env sigma params = - let int_env,bl = intern_context env impl_env params in + let int_env,bl = intern_context env ~bound_univs:(bound_univs sigma) impl_env params in let sigma, x = interp_glob_context_evars ?program_mode env sigma bl in sigma, (int_env, x) (** Local universe and constraint declarations. *) +let interp_known_level evd u = + let u = intern_sort_name ~local_univs:{bound = bound_univs evd; unb_univs=false} u in + Pretyping.known_glob_level evd u + let interp_univ_constraints env evd cstrs = let interp (evd,cstrs) (u, d, u') = - let ul = Pretyping.interp_known_glob_level evd u in - let u'l = Pretyping.interp_known_glob_level evd u' in + let ul = interp_known_level evd u in + let u'l = interp_known_level evd u' in let cstr = (ul,d,u'l) in let cstrs' = Univ.Constraint.add cstr cstrs in try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 0de6c3e89d..f92a54e23f 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -88,7 +88,8 @@ val intern_gen : typing_constraint -> env -> evar_map -> val intern_pattern : env -> cases_pattern_expr -> lident list * (Id.t Id.Map.t * cases_pattern) list -val intern_context : env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list +val intern_context : env -> bound_univs:UnivNames.universe_binders -> + internalization_env -> local_binder_expr list -> internalization_env * glob_decl list (** {6 Composing internalization with type inference (pretyping) } *) @@ -198,6 +199,8 @@ val check_duplicate : ?loc:Loc.t -> (qualid * constr_expr) list -> unit (** Check that a list of record field definitions doesn't contain duplicates. *) +val interp_known_level : Evd.evar_map -> sort_name_expr -> Univ.Level.t + (** Local universe and constraint declarations. *) val interp_univ_decl : Environ.env -> universe_decl_expr -> Evd.evar_map * UState.universe_decl 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/names.ml b/kernel/names.ml index 13761ca245..be65faf234 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -1115,3 +1115,5 @@ let eq_egr e1 e2 = match e1, e2 with type lident = Id.t CAst.t type lname = Name.t CAst.t type lstring = string CAst.t + +let lident_eq = CAst.eq Id.equal diff --git a/kernel/names.mli b/kernel/names.mli index 74a4e6f7d0..747299bb12 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -727,3 +727,5 @@ val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool type lident = Id.t CAst.t type lname = Name.t CAst.t type lstring = string CAst.t + +val lident_eq : lident -> lident -> bool 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/lib/cAst.ml b/lib/cAst.ml index 18fa1c9b0d..30b7fca587 100644 --- a/lib/cAst.ml +++ b/lib/cAst.ml @@ -24,3 +24,5 @@ let map_from_loc f l = let with_val f n = f n.v let with_loc_val f n = f ?loc:n.loc n.v + +let eq f x y = f x.v y.v diff --git a/lib/cAst.mli b/lib/cAst.mli index 2e07d1cd78..025bdf25ab 100644 --- a/lib/cAst.mli +++ b/lib/cAst.mli @@ -22,3 +22,5 @@ val map_from_loc : (?loc:Loc.t -> 'a -> 'b) -> 'a Loc.located -> 'b t val with_val : ('a -> 'b) -> 'a t -> 'b val with_loc_val : (?loc:Loc.t -> 'a -> 'b) -> 'a t -> 'b + +val eq : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool 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/library/libnames.ml b/library/libnames.ml index 88b2e41855..ba1ef1e2f9 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -145,6 +145,8 @@ let qualid_of_dirpath ?loc dir = let (l,a) = split_dirpath dir in make_qualid ?loc l a +let qualid_of_lident lid = qualid_of_ident ?loc:lid.CAst.loc lid.CAst.v + let qualid_is_ident qid = DirPath.is_empty qid.CAst.v.dirpath diff --git a/library/libnames.mli b/library/libnames.mli index a384510879..65aca0c87d 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -77,6 +77,7 @@ val qualid_of_string : ?loc:Loc.t -> string -> qualid val qualid_of_path : ?loc:Loc.t -> full_path -> qualid val qualid_of_dirpath : ?loc:Loc.t -> DirPath.t -> qualid val qualid_of_ident : ?loc:Loc.t -> Id.t -> qualid +val qualid_of_lident : lident -> qualid val qualid_is_ident : qualid -> bool val qualid_path : qualid -> DirPath.t diff --git a/library/nametab.ml b/library/nametab.ml index a51c281f2b..d5cc4f8ac5 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -562,9 +562,9 @@ let shortest_qualid_of_modtype ?loc kn = let sp = MPmap.find kn !the_modtyperevtab in MPTab.shortest_qualid ?loc Id.Set.empty sp !the_modtypetab -let shortest_qualid_of_universe ?loc kn = +let shortest_qualid_of_universe ?loc ctx kn = let sp = UnivIdMap.find kn !the_univrevtab in - UnivTab.shortest_qualid ?loc Id.Set.empty sp !the_univtab + UnivTab.shortest_qualid ?loc ctx sp !the_univtab let pr_global_env env ref = try pr_qualid (shortest_qualid_of_global env ref) diff --git a/library/nametab.mli b/library/nametab.mli index 8a8b59733c..fa27dcab9a 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -206,7 +206,7 @@ val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid val shortest_qualid_of_syndef : ?loc:Loc.t -> Id.Set.t -> syndef_name -> qualid val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid -val shortest_qualid_of_universe : ?loc:Loc.t -> Univ.Level.UGlobal.t -> qualid +val shortest_qualid_of_universe : ?loc:Loc.t -> Id.Set.t -> Univ.Level.UGlobal.t -> qualid (** {5 Generic name handling} *) diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 68530178f8..efe4bfd7f6 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -106,9 +106,9 @@ GRAMMAR EXTEND Gram [ [ c = lconstr -> { c } ] ] ; sort: - [ [ "Set" -> { UNamed [GSet,0] } - | "Prop" -> { UNamed [GProp,0] } - | "SProp" -> { UNamed [GSProp,0] } + [ [ "Set" -> { UNamed [CSet,0] } + | "Prop" -> { UNamed [CProp,0] } + | "SProp" -> { UNamed [CSProp,0] } | "Type" -> { UAnonymous {rigid=true} } | "Type"; "@{"; "_"; "}" -> { UAnonymous {rigid=false} } | "Type"; "@{"; u = universe; "}" -> { UNamed u } ] ] @@ -124,9 +124,9 @@ GRAMMAR EXTEND Gram | -> { 0 } ] ] ; universe_name: - [ [ id = global -> { GType id } - | "Set" -> { GSet } - | "Prop" -> { GProp } ] ] + [ [ id = global -> { CType id } + | "Set" -> { CSet } + | "Prop" -> { CProp } ] ] ; universe_expr: [ [ id = universe_name; n = universe_increment -> { (id,n) } ] ] @@ -282,12 +282,12 @@ GRAMMAR EXTEND Gram | -> { None } ] ] ; universe_level: - [ [ "Set" -> { UNamed GSet } + [ [ "Set" -> { UNamed CSet } (* no parsing SProp as a level *) - | "Prop" -> { UNamed GProp } + | "Prop" -> { UNamed CProp } | "Type" -> { UAnonymous {rigid=true} } | "_" -> { UAnonymous {rigid=false} } - | id = global -> { UNamed (GType id) } ] ] + | id = global -> { UNamed (CType id) } ] ] ; fix_decls: [ [ dcl = fix_decl -> { let (id,_,_,_,_) = dcl.CAst.v in (id,[dcl.CAst.v]) } diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index df9084ab76..8bff5cfd94 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -187,9 +187,9 @@ module Constr : [@@deprecated "Deprecated in 8.13; use 'term' instead"] val ident : Id.t Entry.t val global : qualid Entry.t - val universe_name : Glob_term.glob_sort_name Entry.t - val universe_level : Glob_term.glob_level Entry.t - val sort : Glob_term.glob_sort Entry.t + val universe_name : sort_name_expr Entry.t + val universe_level : univ_level_expr Entry.t + val sort : sort_expr Entry.t val sort_family : Sorts.family Entry.t val pattern : cases_pattern_expr Entry.t val constr_pattern : constr_expr Entry.t diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index c485c38009..23a7b89d2c 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -443,7 +443,7 @@ let cc_tactic depth additionnal_terms = let pr_missing (c, missing) = let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in let holes = List.init missing (fun _ -> hole) in - Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes)) + Printer.pr_glob_constr_env env sigma (DAst.make @@ GApp (c, holes)) in let msg = Pp.(str "Goal is solvable by congruence but some arguments are missing." ++ fnl () ++ diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 767a9ec39b..5bfb37f4cb 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -458,9 +458,11 @@ let rec pattern_to_term_and_type env typ = but only the value of the function *) +let pr_glob_constr_env env x = pr_glob_constr_env env (Evd.from_env env) x + let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_return = - observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt); + observe (str " Entering : " ++ pr_glob_constr_env env rt); let open CAst in match DAst.get rt with | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ @@ -638,9 +640,7 @@ let rec build_entry_lc env sigma funnames avoid rt : with Not_found -> user_err ( str "Cannot find the inductive associated to " - ++ Printer.pr_glob_constr_env env b - ++ str " in " - ++ Printer.pr_glob_constr_env env rt + ++ pr_glob_constr_env env b ++ str " in " ++ pr_glob_constr_env env rt ++ str ". try again with a cast" ) in let case_pats = build_constructors_of_type (fst ind) [] in @@ -662,9 +662,7 @@ let rec build_entry_lc env sigma funnames avoid rt : with Not_found -> user_err ( str "Cannot find the inductive associated to " - ++ Printer.pr_glob_constr_env env b - ++ str " in " - ++ Printer.pr_glob_constr_env env rt + ++ pr_glob_constr_env env b ++ str " in " ++ pr_glob_constr_env env rt ++ str ". try again with a cast" ) in let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in @@ -1321,11 +1319,11 @@ let do_build_inductive evd (funconstants : pconstant list) @@ Constrexpr.CLetIn ( CAst.make n , with_full_print - (Constrextern.extern_glob_constr Id.Set.empty) + Constrextern.(extern_glob_constr empty_extern_env) t , Some (with_full_print - (Constrextern.extern_glob_constr Id.Set.empty) + Constrextern.(extern_glob_constr empty_extern_env) typ) , acc ) | None -> @@ -1335,7 +1333,7 @@ let do_build_inductive evd (funconstants : pconstant list) ( [CAst.make n] , Constrexpr_ops.default_binder_kind , with_full_print - (Constrextern.extern_glob_constr Id.Set.empty) + Constrextern.(extern_glob_constr empty_extern_env) t ) ] , acc )) rel_first_args @@ -1410,11 +1408,11 @@ let do_build_inductive evd (funconstants : pconstant list) @@ Constrexpr.CLetIn ( CAst.make n , with_full_print - (Constrextern.extern_glob_constr Id.Set.empty) + Constrextern.(extern_glob_constr empty_extern_env) t , Some (with_full_print - (Constrextern.extern_glob_constr Id.Set.empty) + Constrextern.(extern_glob_constr empty_extern_env) typ) , acc ) | None -> @@ -1424,7 +1422,7 @@ let do_build_inductive evd (funconstants : pconstant list) ( [CAst.make n] , Constrexpr_ops.default_binder_kind , with_full_print - (Constrextern.extern_glob_constr Id.Set.empty) + Constrextern.(extern_glob_constr empty_extern_env) t ) ] , acc )) rel_first_args @@ -1448,16 +1446,16 @@ let do_build_inductive evd (funconstants : pconstant list) | Some typ -> Constrexpr.CLocalDef ( CAst.make n - , Constrextern.extern_glob_constr Id.Set.empty t + , Constrextern.(extern_glob_constr empty_extern_env) t , Some (with_full_print - (Constrextern.extern_glob_constr Id.Set.empty) + Constrextern.(extern_glob_constr empty_extern_env) typ) ) | None -> Constrexpr.CLocalAssum ( [CAst.make n] , Constrexpr_ops.default_binder_kind - , Constrextern.extern_glob_constr Id.Set.empty t )) + , Constrextern.(extern_glob_constr empty_extern_env) t )) rels_params in let ext_rels_constructors = @@ -1466,7 +1464,7 @@ let do_build_inductive evd (funconstants : pconstant list) ( false , ( CAst.make id , with_full_print - (Constrextern.extern_glob_type Id.Set.empty) + Constrextern.(extern_glob_type empty_extern_env) ((* zeta_normalize *) alpha_rt rel_params_ids t) ) ))) rel_constructors in diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index ff4a82f864..daed855600 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -150,7 +150,7 @@ let pr_occurrences = pr_occurrences () () () let pr_gen env sigma prc _prlc _prtac x = prc env sigma x let pr_globc env sigma _prc _prlc _prtac (_,glob) = - Printer.pr_glob_constr_env env glob + Printer.pr_glob_constr_env env sigma glob let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t) 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/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index eed9419946..069a342b2a 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -63,7 +63,7 @@ let eval_uconstrs ist cs = let pr_auto_using_raw env sigma _ _ _ = Pptactic.pr_auto_using @@ Ppconstr.pr_constr_expr env sigma let pr_auto_using_glob env sigma _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> - Printer.pr_glob_constr_env env c) + Printer.pr_glob_constr_env env sigma c) let pr_auto_using env sigma _ _ _ = Pptactic.pr_auto_using @@ Printer.pr_closed_glob_env env sigma diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index a3f03b5bb5..f12ca0685e 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -40,9 +40,9 @@ type glob_constr_with_bindings = glob_constr_and_expr with_bindings type glob_constr_with_bindings_sign = interp_sign * glob_constr_and_expr with_bindings let pr_glob_constr_with_bindings_sign env sigma _ _ _ (ge : glob_constr_with_bindings_sign) = - Printer.pr_glob_constr_env env (fst (fst (snd ge))) + Printer.pr_glob_constr_env env sigma (fst (fst (snd ge))) let pr_glob_constr_with_bindings env sigma _ _ _ (ge : glob_constr_with_bindings) = - Printer.pr_glob_constr_env env (fst (fst ge)) + Printer.pr_glob_constr_env env sigma (fst (fst ge)) let pr_constr_expr_with_bindings env sigma prc _ _ (ge : constr_expr_with_bindings) = prc env sigma (fst ge) let interp_glob_constr_with_bindings ist gl c = Tacmach.project gl , (ist, c) let glob_glob_constr_with_bindings ist l = Tacintern.intern_constr_with_bindings ist l diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index cd7b1f7f28..fa5bbf7676 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1130,12 +1130,12 @@ let pr_goal_selector ~toplevel s = let rec prtac n (t:glob_tactic_expr) = let pr = { pr_tactic = prtac; - pr_constr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env)); - pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env)); - pr_lconstr = (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env)); - pr_pattern = (fun env sigma -> pr_pat_and_constr_expr (pr_glob_constr_env env)); + pr_constr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env sigma)); + pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env sigma)); + pr_lconstr = (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env sigma)); + pr_pattern = (fun env sigma -> pr_pat_and_constr_expr (pr_glob_constr_env env sigma)); pr_constant = pr_or_var (pr_and_short_name (pr_evaluable_reference_env env)); - pr_lpattern = (fun env sigma -> pr_pat_and_constr_expr (pr_lglob_constr_env env)); + pr_lpattern = (fun env sigma -> pr_pat_and_constr_expr (pr_lglob_constr_env env sigma)); pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant); pr_name = pr_lident; pr_generic = Pputils.pr_glb_generic; @@ -1166,7 +1166,7 @@ let pr_goal_selector ~toplevel s = let pr = { pr_tactic = (fun _ _ -> str "<tactic>"); pr_constr = pr_econstr_env; - pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env)); + pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env sigma)); pr_lconstr = pr_leconstr_env; pr_pattern = pr_constr_pattern_env; pr_lpattern = pr_lconstr_pattern_env; @@ -1189,7 +1189,7 @@ let pr_goal_selector ~toplevel s = let pr_raw_extend env sigma = pr_raw_extend_rec @@ pr_raw_tactic_level env sigma - let pr_glob_extend env sigma = pr_glob_extend_rec (pr_glob_tactic_level env) + let pr_glob_extend env = pr_glob_extend_rec (pr_glob_tactic_level env) let pr_alias pr lev key args = pr_alias_gen (fun _ arg -> pr arg) lev key args @@ -1212,8 +1212,8 @@ let declare_extra_genarg_pprule wit f env sigma pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in let g x = Genprint.PrinterBasic (fun env sigma -> - g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env)) - (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env)) + g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env sigma)) + (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env sigma)) (fun env sigma -> pr_glob_tactic_level env) x) in let h x = @@ -1242,8 +1242,8 @@ let declare_extra_genarg_pprule_with_level wit default_already_surrounded = default_surrounded; default_ensure_surrounded = default_non_surrounded; printer = (fun env sigma n -> - g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env)) - (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env)) + g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env sigma)) + (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env sigma)) (fun env sigma -> pr_glob_tactic_level env) n x) } in let h x = @@ -1301,10 +1301,10 @@ let register_basic_print0 wit f g h = Genprint.register_print0 wit (lift f) (lift g) (lift_top h) let pr_glob_constr_pptac env sigma c = - pr_glob_constr_env env c + pr_glob_constr_env env sigma c let pr_lglob_constr_pptac env sigma c = - pr_lglob_constr_env env c + pr_lglob_constr_env env sigma c let pr_raw_intro_pattern = lift_env (fun env sigma -> Miscprint.pr_intro_pattern @@ pr_constr_expr env sigma) diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 5e199dad62..79e0adf9f7 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -124,7 +124,7 @@ val pr_glb_generic : env -> Evd.evar_map -> glevel generic_argument -> Pp.t val pr_raw_extend: env -> Evd.evar_map -> int -> ml_tactic_entry -> raw_tactic_arg list -> Pp.t -val pr_glob_extend: env -> Evd.evar_map -> int -> +val pr_glob_extend: env -> int -> ml_tactic_entry -> glob_tactic_arg list -> Pp.t val pr_extend : diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 9c15d24dd3..aa2449d962 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -244,7 +244,8 @@ let string_of_call ck = (Pptactic.pr_glob_tactic (Global.env ()) (Tacexpr.TacAtom (CAst.make te))) | Tacexpr.LtacConstrInterp (c, _) -> - pr_glob_constr_env (Global.env ()) c + let env = Global.env () in + pr_glob_constr_env env (Evd.from_env env) c | Tacexpr.LtacMLCall te -> (Pptactic.pr_glob_tactic (Global.env ()) te) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 00ac155f0e..f2241e78d2 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -773,7 +773,7 @@ let interp_may_eval f ist env sigma = function function already use effect, I call [run] hoping it doesn't mess up with any assumption. *) Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () -> - str"interpretation of term " ++ pr_glob_constr_env env (fst c))); + str"interpretation of term " ++ pr_glob_constr_env env sigma (fst c))); Exninfo.iraise reraise (* Interprets a constr expression possibly to first evaluate *) diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 5fbea4eeef..c4c528d373 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -16,11 +16,12 @@ open Tacexpr let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make () let prtac x = - Pptactic.pr_glob_tactic (Global.env()) x + let env = Global.env () in + Pptactic.pr_glob_tactic env x let prmatchpatt env sigma hyp = Pptactic.pr_match_pattern (Printer.pr_constr_pattern_env env sigma) hyp let prmatchrl env sigma rl = - Pptactic.pr_match_rule false (Pptactic.pr_glob_tactic (Global.env())) + Pptactic.pr_match_rule false prtac (fun (_,p) -> Printer.pr_constr_pattern_env env sigma p) rl (* This module intends to be a beginning of debugger for tactic expressions. @@ -366,24 +367,22 @@ let explain_ltac_call_trace last trace loc = | Tacexpr.LtacNotationCall kn -> quote (Pptactic.pr_alias_key kn) | Tacexpr.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst) | Tacexpr.LtacMLCall t -> - quote (Pptactic.pr_glob_tactic (Global.env()) t) + quote (prtac t) | Tacexpr.LtacVarCall (id,t) -> quote (Id.print id) ++ strbrk " (bound to " ++ - Pptactic.pr_glob_tactic (Global.env()) t ++ str ")" + prtac t ++ str ")" | Tacexpr.LtacAtomCall te -> - quote (Pptactic.pr_glob_tactic (Global.env()) - (Tacexpr.TacAtom (CAst.make te))) + quote (prtac (Tacexpr.TacAtom (CAst.make te))) | Tacexpr.LtacConstrInterp (c, { Ltac_pretype.ltac_constrs = vars }) -> - quote (Printer.pr_glob_constr_env (Global.env()) c) ++ + (* XXX: This hooks into the CErrors's additional error info API so + it is tricky to provide the right env for now. *) + let env = Global.env() in + let sigma = Evd.from_env env in + quote (Printer.pr_glob_constr_env env sigma c) ++ (if not (Id.Map.is_empty vars) then strbrk " (with " ++ prlist_with_sep pr_comma (fun (id,c) -> - (* XXX: This hooks into the CErrors's additional error - info API so it is tricky to provide the right env for - now. *) - let env = Global.env () in - let sigma = Evd.from_env env in Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders_env env sigma c) (List.rev (Id.Map.bindings vars)) ++ str ")" else mt()) diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml index 42b9248979..61643c2aa3 100644 --- a/plugins/ssr/ssrbwd.ml +++ b/plugins/ssr/ssrbwd.ml @@ -50,7 +50,7 @@ let interp_agen ist gl ((goclr, _), (k, gc as c)) (clr, rcs) = SsrHyp (Loc.tag ?loc id) :: clr', rcs' | _ -> clr', rcs' -let pf_pr_glob_constr gl = pr_glob_constr_env (pf_env gl) +let pf_pr_glob_constr gl = pr_glob_constr_env (pf_env gl) (project gl) let interp_nbargs ist gl rc = try diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index cb58b9bcb8..cd219838d5 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -895,7 +895,7 @@ open Constrexpr open Util (** Constructors for constr_expr *) -let mkCProp loc = CAst.make ?loc @@ CSort (UNamed [GProp,0]) +let mkCProp loc = CAst.make ?loc @@ CSort (UNamed [CProp,0]) let mkCType loc = CAst.make ?loc @@ CSort (UAnonymous {rigid=true}) let mkCVar ?loc id = CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None) let rec mkCHoles ?loc n = diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index a7ebd5f9f5..fdfba48024 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -84,7 +84,7 @@ let interp_congrarg_at ist gl n rf ty m = if i + n > m then None else try let rt = mkRApp congrn (args1 @ mkRApp rf (mkRHoles i) :: args2) in - ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) rt)); + ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) (project gl) rt)); Some (interp_refine ist gl rt) with _ -> loop (i + 1) in loop 0 diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index ab36d4fc7c..95c8024e89 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -57,17 +57,16 @@ let pr_guarded guard prc c = let s = Format.flush_str_formatter () ^ "$" in if guard s (skip_wschars s 0) then pr_paren prc c else prc c -let prl_constr_expr = +let with_global_env_evm f x = let env = Global.env () in let sigma = Evd.from_env env in - Ppconstr.pr_lconstr_expr env sigma -let pr_glob_constr c = Printer.pr_glob_constr_env (Global.env ()) c -let prl_glob_constr c = Printer.pr_lglob_constr_env (Global.env ()) c + f env sigma x + +let prl_constr_expr = with_global_env_evm Ppconstr.pr_lconstr_expr +let pr_glob_constr = with_global_env_evm Printer.pr_glob_constr_env +let prl_glob_constr = with_global_env_evm Printer.pr_lglob_constr_env let pr_glob_constr_and_expr = function - | _, Some c -> - let env = Global.env () in - let sigma = Evd.from_env env in - Ppconstr.pr_constr_expr env sigma c + | _, Some c -> with_global_env_evm Ppconstr.pr_constr_expr c | c, None -> pr_glob_constr c let pr_term (k, c) = pr_guarded (guard_term k) pr_glob_constr_and_expr c diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 99cf197b78..3e44bd4d3b 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -203,8 +203,8 @@ let pr_raw_ssrhintref env sigma prc _ _ = let open CAst in function let pr_rawhintref env sigma c = match DAst.get c with | GApp (f, args) when isRHoles args -> - pr_glob_constr_env env f ++ str "|" ++ int (List.length args) - | _ -> pr_glob_constr_env env c + pr_glob_constr_env env sigma f ++ str "|" ++ int (List.length args) + | _ -> pr_glob_constr_env env sigma c let pr_glob_ssrhintref env sigma _ _ _ (c, _) = pr_rawhintref env sigma c diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index d99ead139d..97926753f5 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -195,7 +195,7 @@ let interp_glob ist glob = Goal.enter_one ~__LOC__ begin fun goal -> let env = Goal.env goal in let sigma = Goal.sigma goal in Ssrprinters.ppdebug (lazy - Pp.(str"interp-in: " ++ Printer.pr_glob_constr_env env glob)); + Pp.(str"interp-in: " ++ Printer.pr_glob_constr_env env sigma glob)); try let sigma,term = Tacinterp.interp_open_constr ist env sigma (glob,None) in Ssrprinters.ppdebug (lazy @@ -205,7 +205,7 @@ let interp_glob ist glob = Goal.enter_one ~__LOC__ begin fun goal -> (* XXX this is another catch all! *) let e, info = Exninfo.capture e in Ssrprinters.ppdebug (lazy - Pp.(str"interp-err: " ++ Printer.pr_glob_constr_env env glob)); + Pp.(str"interp-err: " ++ Printer.pr_glob_constr_env env sigma glob)); tclZERO ~info e end diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index a4aa08300d..ea014250ca 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -88,8 +88,12 @@ let pr_guarded guard prc c = let s = Pp.string_of_ppcmds (prc c) ^ "$" in if guard s (skip_wschars s 0) then pr_paren prc c else prc c (* More sensible names for constr printers *) -let prl_glob_constr c = pr_lglob_constr_env (Global.env ()) c -let pr_glob_constr c = pr_glob_constr_env (Global.env ()) c +let with_global_env_evm f x = + let env = Global.env () in + let sigma = Evd.from_env env in + f env sigma x +let prl_glob_constr = with_global_env_evm pr_lglob_constr_env +let pr_glob_constr = with_global_env_evm pr_glob_constr_env let prl_constr_expr = pr_lconstr_expr let pr_constr_expr = pr_constr_expr let prl_glob_constr_and_expr env sigma = function diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index a12a832f76..402a6f6ed3 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -648,26 +648,16 @@ let detype_cofix detype flags avoid env sigma n (names,tys,bodies) = Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) -(* TODO use some algebraic type with a case for unnamed univs so we - can cleanly detype them. NB: this corresponds to a hack in - Pretyping.interp_universe_level_name to convert Foo.xx strings into - universes. *) -let hack_qualid_of_univ_level sigma l = - match Termops.reference_of_level sigma l with - | Some qid -> qid - | None -> - let path = String.split_on_char '.' (Univ.Level.to_string l) in - let path = List.rev_map Id.of_string_soft path in - Libnames.qualid_of_dirpath (DirPath.make path) +let detype_level_name sigma l = + if Univ.Level.is_sprop l then GSProp else + if Univ.Level.is_prop l then GProp else + if Univ.Level.is_set l then GSet else + match UState.id_of_level (Evd.evar_universe_context sigma) l with + | Some id -> GLocalUniv (CAst.make id) + | None -> GUniv l let detype_universe sigma u = - let fn (l, n) = - let s = - if Univ.Level.is_prop l then GProp else - if Univ.Level.is_set l then GSet else - GType (hack_qualid_of_univ_level sigma l) in - (s, n) in - List.map fn (Univ.Universe.repr u) + List.map (on_fst (detype_level_name sigma)) (Univ.Universe.repr u) let detype_sort sigma = function | SProp -> UNamed [GSProp,0] @@ -684,8 +674,7 @@ type binder_kind = BProd | BLambda | BLetIn (* Main detyping function *) let detype_level sigma l = - let l = hack_qualid_of_univ_level sigma l in - UNamed (GType l) + UNamed (detype_level_name sigma l) let detype_instance sigma l = let l = EInstance.kind sigma l in diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index f42c754ef5..86d2cc78e0 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -48,8 +48,10 @@ let glob_sort_name_eq g1 g2 = match g1, g2 with | GSProp, GSProp | GProp, GProp | GSet, GSet -> true - | GType u1, GType u2 -> Libnames.qualid_eq u1 u2 - | (GSProp|GProp|GSet|GType _), _ -> false + | GUniv u1, GUniv u2 -> Univ.Level.equal u1 u2 + | GLocalUniv u1, GLocalUniv u2 -> lident_eq u1 u2 + | GRawUniv u1, GRawUniv u2 -> Univ.Level.equal u1 u2 + | (GSProp|GProp|GSet|GUniv _|GLocalUniv _|GRawUniv _), _ -> false exception ComplexSort @@ -60,19 +62,23 @@ let glob_sort_family = let open Sorts in function | UNamed [GSet,0] -> InSet | _ -> raise ComplexSort -let glob_sort_expr_eq f u1 u2 = +let map_glob_sort_gen f = function + | UNamed l -> UNamed (f l) + | UAnonymous _ as x -> x + +let glob_sort_gen_eq f u1 u2 = match u1, u2 with | UAnonymous {rigid=r1}, UAnonymous {rigid=r2} -> r1 = r2 | UNamed l1, UNamed l2 -> f l1 l2 | (UNamed _ | UAnonymous _), _ -> false let glob_sort_eq u1 u2 = - glob_sort_expr_eq + glob_sort_gen_eq (List.equal (fun (x,m) (y,n) -> glob_sort_name_eq x y && Int.equal m n)) u1 u2 let glob_level_eq u1 u2 = - glob_sort_expr_eq glob_sort_name_eq u1 u2 + glob_sort_gen_eq glob_sort_name_eq u1 u2 let binding_kind_eq bk1 bk2 = match bk1, bk2 with | Explicit, Explicit -> true diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 6da8173dce..5ad1a207f3 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -11,8 +11,12 @@ open Names open Glob_term +val map_glob_sort_gen : ('a -> 'b) -> 'a glob_sort_gen -> 'b glob_sort_gen + (** Equalities *) +val glob_sort_gen_eq : ('a -> 'a -> bool) -> 'a glob_sort_gen -> 'a glob_sort_gen -> bool + val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool val glob_level_eq : Glob_term.glob_level -> Glob_term.glob_level -> bool diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index a49c8abe26..a957bc0fcd 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -26,17 +26,23 @@ type glob_sort_name = | GSProp (** representation of [SProp] literal *) | GProp (** representation of [Prop] level *) | GSet (** representation of [Set] level *) - | GType of Libnames.qualid (** representation of a [Type] level *) + | GUniv of Univ.Level.t + | GLocalUniv of lident (** Locally bound universes (may also be nonstrict declaration) *) + | GRawUniv of Univ.Level.t + (** Hack for funind, DO NOT USE -type 'a glob_sort_expr = + Note that producing the similar Constrexpr.CRawType for printing + is OK, just don't try to reinterp it. *) + +type 'a glob_sort_gen = | UAnonymous of { rigid : bool } (** not rigid = unifiable by minimization *) | UNamed of 'a (** levels, occurring in universe instances *) -type glob_level = glob_sort_name glob_sort_expr +type glob_level = glob_sort_name glob_sort_gen (** sort expressions *) -type glob_sort = (glob_sort_name * int) list glob_sort_expr +type glob_sort = (glob_sort_name * int) list glob_sort_gen type glob_constraint = glob_sort_name * Univ.constraint_type * glob_sort_name diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index b70ff20e32..9dbded75ba 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -130,53 +130,32 @@ let is_strict_universe_declarations = (** Miscellaneous interpretation functions *) -let interp_known_universe_level_name evd qid = - try - let open Libnames in - if qualid_is_ident qid then Evd.universe_of_name evd @@ qualid_basename qid - else raise Not_found - with Not_found -> - let qid = Nametab.locate_universe qid in - Univ.Level.make qid - -let interp_universe_level_name evd qid = - try evd, interp_known_universe_level_name evd qid +let universe_level_name evd ({CAst.v=id} as lid) = + try evd, Evd.universe_of_name evd id with Not_found -> - if Libnames.qualid_is_ident qid then (* Undeclared *) - let id = Libnames.qualid_basename qid in - if not (is_strict_universe_declarations ()) then - new_univ_level_variable ?loc:qid.CAst.loc ~name:id univ_rigid evd - else user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name" - (Pp.(str "Undeclared universe: " ++ Id.print id)) - else - let dp, i = Libnames.repr_qualid qid in - let num = - try int_of_string (Id.to_string i) - with Failure _ -> - user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name" - (Pp.(str "Undeclared global universe: " ++ Libnames.pr_qualid qid)) - in - let level = Univ.Level.(make (UGlobal.make dp num)) in - let evd = - try Evd.add_global_univ evd level - with UGraph.AlreadyDeclared -> evd - in evd, level + if not (is_strict_universe_declarations ()) then + new_univ_level_variable ?loc:lid.CAst.loc ~name:id univ_rigid evd + else user_err ?loc:lid.CAst.loc ~hdr:"universe_level_name" + (Pp.(str "Undeclared universe: " ++ Id.print id)) -let interp_sort_name sigma = function +let sort_name sigma = function | GSProp -> sigma, Univ.Level.sprop | GProp -> sigma, Univ.Level.prop | GSet -> sigma, Univ.Level.set - | GType l -> interp_universe_level_name sigma l + | GUniv u -> sigma, u + | GRawUniv u -> + (try Evd.add_global_univ sigma u with UGraph.AlreadyDeclared -> sigma), u + | GLocalUniv l -> universe_level_name sigma l -let interp_sort_info ?loc evd l = +let sort_info ?loc evd l = List.fold_left (fun (evd, u) (l,n) -> - let evd', u' = interp_sort_name evd l in + let evd', u' = sort_name evd l in let u' = Univ.Universe.make u' in let u' = match n with | 0 -> u' | 1 -> Univ.Universe.super u' | n -> - user_err ?loc ~hdr:"interp_universe" + user_err ?loc ~hdr:"sort_info" (Pp.(str "Cannot interpret universe increment +" ++ int n)) in (evd', Univ.sup u u')) (evd, Univ.Universe.type0m) l @@ -393,24 +372,33 @@ let pretype_id pretype loc env sigma id = (*************************************************************************) (* Main pretyping function *) -let interp_known_glob_level ?loc evd = function +let known_universe_level_name evd lid = + try Evd.universe_of_name evd lid.CAst.v + with Not_found -> + let u = Nametab.locate_universe (Libnames.qualid_of_lident lid) in + Univ.Level.make u + +let known_glob_level evd = function | GSProp -> Univ.Level.sprop | GProp -> Univ.Level.prop | GSet -> Univ.Level.set - | GType qid -> - try interp_known_universe_level_name evd qid + | GUniv u -> u + | GRawUniv u -> anomaly Pp.(str "Raw universe in known_glob_level.") + | GLocalUniv lid -> + try known_universe_level_name evd lid with Not_found -> - user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_qualid qid) + user_err ?loc:lid.CAst.loc ~hdr:"known_level_info" + (str "Undeclared universe " ++ Id.print lid.CAst.v) -let interp_glob_level ?loc evd : glob_level -> _ = function +let glob_level ?loc evd : glob_level -> _ = function | UAnonymous {rigid} -> new_univ_level_variable ?loc (if rigid then univ_rigid else univ_flexible) evd - | UNamed s -> interp_sort_name evd s + | UNamed s -> sort_name evd s -let interp_instance ?loc evd l = +let instance ?loc evd l = let evd, l' = List.fold_left (fun (evd, univs) l -> - let evd, l = interp_glob_level ?loc evd l in + let evd, l = glob_level ?loc evd l in (evd, l :: univs)) (evd, []) l in @@ -424,7 +412,7 @@ let pretype_global ?loc rigid env evd gr us = let evd, instance = match us with | None -> evd, None - | Some l -> interp_instance ?loc evd l + | Some l -> instance ?loc evd l in Evd.fresh_global ?loc ~rigid ?names:instance !!env evd gr @@ -451,11 +439,11 @@ let pretype_ref ?loc sigma env ref us = let sigma, ty = type_of !!env sigma c in sigma, make_judge c ty -let interp_sort ?loc evd : glob_sort -> _ = function +let sort ?loc evd : glob_sort -> _ = function | UAnonymous {rigid} -> let evd, l = new_univ_level_variable ?loc (if rigid then univ_rigid else univ_flexible) evd in evd, Univ.Universe.make l - | UNamed l -> interp_sort_info ?loc evd l + | UNamed l -> sort_info ?loc evd l let judge_of_sort ?loc evd s = let judge = @@ -469,11 +457,22 @@ let pretype_sort ?loc sigma s = | UNamed [GProp,0] -> sigma, judge_of_prop | UNamed [GSet,0] -> sigma, judge_of_set | _ -> - let sigma, s = interp_sort ?loc sigma s in + let sigma, s = sort ?loc sigma s in judge_of_sort ?loc sigma s -let new_type_evar env sigma loc = - new_type_evar env sigma ~src:(Loc.tag ?loc Evar_kinds.InternalHole) +let new_typed_evar env sigma ?naming ~src tycon = + match tycon with + | Some ty -> + let sigma, c = new_evar env sigma ~src ?naming ty in + sigma, c, ty + | None -> + let sigma, ty = new_type_evar env sigma ~src in + let sigma, c = new_evar env sigma ~src ?naming ty in + let evk = fst (destEvar sigma c) in + let ido = Evd.evar_ident evk sigma in + let src = (fst src,Evar_kinds.EvarType (ido,evk)) in + let sigma = update_source sigma (fst (destEvar sigma ty)) src in + sigma, c, ty let mark_obligation_evar sigma k evc = match k with @@ -636,13 +635,9 @@ struct discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon let pretype_patvar self kind ?loc ~program_mode ~poly resolve_tc tycon env sigma = - let sigma, ty = - match tycon with - | Some ty -> sigma, ty - | None -> new_type_evar env sigma loc in let k = Evar_kinds.MatchingVar kind in - let sigma, uj_val = new_evar env sigma ~src:(loc,k) ty in - sigma, { uj_val; uj_type = ty } + let sigma, uj_val, uj_type = new_typed_evar env sigma ~src:(loc,k) tycon in + sigma, { uj_val; uj_type } let pretype_hole self (k, naming, ext) = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> @@ -653,19 +648,15 @@ struct | IntroIdentifier id -> IntroIdentifier (interp_ltac_id env id) | IntroAnonymous -> IntroAnonymous | IntroFresh id -> IntroFresh (interp_ltac_id env id) in - let sigma, ty = - match tycon with - | Some ty -> sigma, ty - | None -> new_type_evar env sigma loc in - let sigma, uj_val = new_evar env sigma ~src:(loc,k) ~naming ty in + let sigma, uj_val, uj_type = new_typed_evar env sigma ~src:(loc,k) ~naming tycon in let sigma = if program_mode then mark_obligation_evar sigma k uj_val else sigma in - sigma, { uj_val; uj_type = ty } + sigma, { uj_val; uj_type } | Some arg -> let sigma, ty = match tycon with | Some ty -> sigma, ty - | None -> new_type_evar env sigma loc in + | None -> new_type_evar env sigma ~src:(loc,Evar_kinds.InternalHole) in let c, sigma = GlobEnv.interp_glob_genarg env poly sigma ty arg in sigma, { uj_val = c; uj_type = ty } @@ -1144,7 +1135,7 @@ struct | None -> let sigma, p = match tycon with | Some ty -> sigma, ty - | None -> new_type_evar env sigma loc + | None -> new_type_evar env sigma ~src:(loc,Evar_kinds.CasesType false) in sigma, it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in let pred = nf_evar sigma pred in diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 7bb4a6e273..5668098fe6 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -30,8 +30,7 @@ val get_bidirectionality_hint : GlobRef.t -> int option val clear_bidirectionality_hint : GlobRef.t -> unit -val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map -> - glob_sort_name -> Univ.Level.t +val known_glob_level : Evd.evar_map -> glob_sort_name -> Univ.Level.t (** An auxiliary function for searching for fixpoint guard indexes *) diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 8942bc7805..4c410c3170 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -152,14 +152,15 @@ let tag_var = tag Tag.variable let pr_sep_com sep f c = pr_with_comments ?loc:(constr_loc c) (sep() ++ f c) - let pr_glob_sort_name = function - | GSProp -> str "SProp" - | GProp -> str "Prop" - | GSet -> str "Set" - | GType qid -> pr_qualid qid + let pr_sort_name_expr = function + | CSProp -> str "SProp" + | CProp -> str "Prop" + | CSet -> str "Set" + | CType qid -> pr_qualid qid + | CRawType s -> Univ.Level.pr s let pr_univ_expr (u,n) = - pr_glob_sort_name u ++ (match n with 0 -> mt () | _ -> str"+" ++ int n) + pr_sort_name_expr u ++ (match n with 0 -> mt () | _ -> str"+" ++ int n) let pr_univ l = match l with @@ -168,21 +169,22 @@ let tag_var = tag Tag.variable let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}" - let pr_glob_sort = let open Glob_term in function - | UNamed [GSProp,0] -> tag_type (str "SProp") - | UNamed [GProp,0] -> tag_type (str "Prop") - | UNamed [GSet,0] -> tag_type (str "Set") + let pr_sort_expr = function + | UNamed [CSProp,0] -> tag_type (str "SProp") + | UNamed [CProp,0] -> tag_type (str "Prop") + | UNamed [CSet,0] -> tag_type (str "Set") | UAnonymous {rigid=true} -> tag_type (str "Type") | UAnonymous {rigid=false} -> tag_type (str "Type") ++ pr_univ_annot (fun _ -> str "_") () | UNamed u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u) - let pr_glob_level = let open Glob_term in function - | UNamed GSProp -> tag_type (str "SProp") - | UNamed GProp -> tag_type (str "Prop") - | UNamed GSet -> tag_type (str "Set") + let pr_univ_level_expr = function + | UNamed CSProp -> tag_type (str "SProp") + | UNamed CProp -> tag_type (str "Prop") + | UNamed CSet -> tag_type (str "Set") | UAnonymous {rigid=true} -> tag_type (str "Type") | UAnonymous {rigid=false} -> tag_type (str "_") - | UNamed (GType u) -> tag_type (pr_qualid u) + | UNamed (CType u) -> tag_type (pr_qualid u) + | UNamed (CRawType s) -> tag_type (Univ.Level.pr s) let pr_qualid sp = let (sl, id) = repr_qualid sp in @@ -200,7 +202,7 @@ let tag_var = tag Tag.variable let pr_patvar = pr_id let pr_universe_instance l = - pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_level)) l + pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_univ_level_expr)) l let pr_reference qid = if qualid_is_ident qid then tag_var (pr_id @@ qualid_basename qid) @@ -664,7 +666,7 @@ let tag_var = tag Tag.variable | CPatVar p -> return (str "@?" ++ pr_patvar p, latom) | CSort s -> - return (pr_glob_sort s, latom) + return (pr_sort_expr s, latom) | CCast (a,b) -> return ( hv 0 (pr mt (LevelLt lcast) a ++ spc () ++ @@ -717,7 +719,7 @@ let tag_var = tag Tag.variable let transf env sigma c = if !Flags.beautify_file then let r = Constrintern.for_grammar (Constrintern.intern_constr env sigma) c in - Constrextern.extern_glob_constr (Termops.vars_of_env env) r + Constrextern.(extern_glob_constr (extern_env env sigma)) r else c let pr_expr env sigma prec c = diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 02e04573f8..d66b77efb2 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -32,9 +32,9 @@ val pr_id : Id.t -> Pp.t val pr_qualid : qualid -> Pp.t val pr_patvar : Pattern.patvar -> Pp.t -val pr_glob_sort_name : Glob_term.glob_sort_name -> Pp.t -val pr_glob_level : Glob_term.glob_level -> Pp.t -val pr_glob_sort : Glob_term.glob_sort -> Pp.t +val pr_sort_name_expr : sort_name_expr -> Pp.t +val pr_univ_level_expr : univ_level_expr -> Pp.t +val pr_sort_expr : sort_expr -> Pp.t val pr_guard_annot : (constr_expr -> Pp.t) -> local_binder_expr list diff --git a/printing/printer.ml b/printing/printer.ml index ea718526de..1425cebafc 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -97,10 +97,10 @@ let pr_ltype_env ?lax ?goal_concl_style env sigma ?impargs c = let pr_ljudge_env env sigma j = (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type) -let pr_lglob_constr_env env c = - pr_lconstr_expr env (Evd.from_env env) (extern_glob_constr (Termops.vars_of_env env) c) -let pr_glob_constr_env env c = - pr_constr_expr env (Evd.from_env env) (extern_glob_constr (Termops.vars_of_env env) c) +let pr_lglob_constr_env env sigma c = + pr_lconstr_expr env sigma (extern_glob_constr (extern_env env sigma) c) +let pr_glob_constr_env env sigma c = + pr_constr_expr env sigma (extern_glob_constr (extern_env env sigma) c) let pr_closed_glob_n_env ?lax ?goal_concl_style ?inctx ?scope env sigma n c = pr_constr_expr_n env sigma n (extern_closed_glob ?lax ?goal_concl_style ?inctx ?scope env sigma c) @@ -115,7 +115,7 @@ let pr_constr_pattern_env env sigma c = let pr_cases_pattern t = pr_cases_pattern_expr (extern_cases_pattern Names.Id.Set.empty t) -let pr_sort sigma s = pr_glob_sort (extern_sort sigma s) +let pr_sort sigma s = pr_sort_expr (extern_sort sigma s) let () = Termops.Internal.set_print_constr (fun env sigma t -> pr_lconstr_expr env sigma (extern_constr ~lax:true env sigma t)) diff --git a/printing/printer.mli b/printing/printer.mli index ea388ae57e..732af5570d 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -107,9 +107,9 @@ val pr_closed_glob_env : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t -val pr_lglob_constr_env : env -> 'a glob_constr_g -> Pp.t +val pr_lglob_constr_env : env -> evar_map -> 'a glob_constr_g -> Pp.t -val pr_glob_constr_env : env -> 'a glob_constr_g -> Pp.t +val pr_glob_constr_env : env -> evar_map -> 'a glob_constr_g -> Pp.t val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t 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/declareUctx.ml b/tactics/declareUctx.ml index 3f67ff20a4..bca43697cb 100644 --- a/tactics/declareUctx.ml +++ b/tactics/declareUctx.ml @@ -16,7 +16,7 @@ let name_instance inst = assert false | Some na -> try - let qid = Nametab.shortest_qualid_of_universe na in + let qid = Nametab.shortest_qualid_of_universe Names.Id.Set.empty na in Names.Name (Libnames.qualid_basename qid) with Not_found -> (* Best-effort naming from the string representation of the level. 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_13303.v b/test-suite/bugs/closed/bug_13303.v new file mode 100644 index 0000000000..6bee24b48a --- /dev/null +++ b/test-suite/bugs/closed/bug_13303.v @@ -0,0 +1,27 @@ +Module Pt1. + + Module M. Universe i. End M. + Module N. Universe i. End N. + Import M. + Notation foo := Type@{i (* M.i??? *)}. + Import N. + Fail Check foo : Type@{M.i}. (* should NOT succeed *) + Check foo : Type@{i (* N.i *)}. (* should succeed *) + + Definition bar@{i} := Type@{i}. + Check bar : Type@{N.i}. + Check bar : Type@{M.i}. + +End Pt1. + +Module Pt2. + + Module M. Universe i. Notation foo := Type@{i}. End M. + + Definition foo1 := M.foo. + (* should succeed, currently errors undeclared universe i *) + + Definition foo2@{i} : Type@{i} := M.foo. + (* should succeed, currently errors universe inconsistency *) + +End Pt2. 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/misc/quotation_token/src/quotation.mlg b/test-suite/misc/quotation_token/src/quotation.mlg index ba0bcb1b3c..0f843b3b14 100644 --- a/test-suite/misc/quotation_token/src/quotation.mlg +++ b/test-suite/misc/quotation_token/src/quotation.mlg @@ -7,6 +7,6 @@ GRAMMAR EXTEND Gram term: LEVEL "0" [ [ s = QUOTATION "foobar:" -> { - CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [GProp,0])) } ] ] + CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [CProp,0])) } ] ] ; END diff --git a/test-suite/misc/side-eff-leak-univs/src/evil.mlg b/test-suite/misc/side-eff-leak-univs/src/evil.mlg index d89ab887a8..bb6eaff409 100644 --- a/test-suite/misc/side-eff-leak-univs/src/evil.mlg +++ b/test-suite/misc/side-eff-leak-univs/src/evil.mlg @@ -7,7 +7,7 @@ open Stdarg TACTIC EXTEND magic | [ "magic" ident(i) ident(j) ] -> { - let open Glob_term in - DeclareUniv.do_constraint ~poly:false [ GType (Libnames.qualid_of_ident i), Univ.Lt, GType (Libnames.qualid_of_ident j)]; Proofview.tclUNIT() + let open Constrexpr in + DeclareUniv.do_constraint ~poly:false [ CType (Libnames.qualid_of_ident i), Univ.Lt, CType (Libnames.qualid_of_ident j)]; Proofview.tclUNIT() } END diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index d8d3f696b7..0fbb4f4c11 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -1,61 +1,61 @@ -Inductive Empty@{u} : Type@{u} := -(* u |= *) -Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A } -(* u |= *) +Inductive Empty@{uu} : Type@{uu} := +(* uu |= *) +Record PWrap (A : Type@{uu}) : Type@{uu} := pwrap { punwrap : A } +(* uu |= *) PWrap has primitive projections with eta conversion. Arguments PWrap _%type_scope Arguments pwrap _%type_scope _ -punwrap@{u} = -fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p - : forall A : Type@{u}, PWrap@{u} A -> A -(* u |= *) +punwrap@{uu} = +fun (A : Type@{uu}) (p : PWrap@{uu} A) => punwrap _ p + : forall A : Type@{uu}, PWrap@{uu} A -> A +(* uu |= *) Arguments punwrap _%type_scope _ -Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A } -(* u |= *) +Record RWrap (A : Type@{uu}) : Type@{uu} := rwrap { runwrap : A } +(* uu |= *) Arguments RWrap _%type_scope Arguments rwrap _%type_scope _ -runwrap@{u} = -fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap - : forall A : Type@{u}, RWrap@{u} A -> A -(* u |= *) +runwrap@{uu} = +fun (A : Type@{uu}) (r : RWrap@{uu} A) => let (runwrap) := r in runwrap + : forall A : Type@{uu}, RWrap@{uu} A -> A +(* uu |= *) Arguments runwrap _%type_scope _ -Wrap@{u} = fun A : Type@{u} => A - : Type@{u} -> Type@{u} -(* u |= *) +Wrap@{uu} = fun A : Type@{uu} => A + : Type@{uu} -> Type@{uu} +(* uu |= *) Arguments Wrap _%type_scope -wrap@{u} = -fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap - : forall A : Type@{u}, Wrap@{u} A -> A -(* u |= *) +wrap@{uu} = +fun (A : Type@{uu}) (Wrap : Wrap@{uu} A) => Wrap + : forall A : Type@{uu}, Wrap@{uu} A -> A +(* uu |= *) Arguments wrap {A}%type_scope {Wrap} -bar@{u} = nat - : Wrap@{u} Set -(* u |= Set < u *) -foo@{u u0 v} = -Type@{u0} -> Type@{v} -> Type@{u} - : Type@{max(u+1,u0+1,v+1)} -(* u u0 v |= *) +bar@{uu} = nat + : Wrap@{uu} Set +(* uu |= Set < uu *) +foo@{uu u v} = +Type@{u} -> Type@{v} -> Type@{uu} + : Type@{max(uu+1,u+1,v+1)} +(* uu u v |= *) Type@{i} -> Type@{j} : Type@{max(i+1,j+1)} (* {j i} |= *) = Type@{i} -> Type@{j} : Type@{max(i+1,j+1)} (* {j i} |= *) -mono = Type@{mono.u} - : Type@{mono.u+1} -(* {mono.u} |= *) +mono = Type@{mono.uu} + : Type@{mono.uu+1} +(* {mono.uu} |= *) mono - : Type@{mono.u+1} -Type@{mono.u} - : Type@{mono.u+1} + : Type@{mono.uu+1} +Type@{mono.uu} + : Type@{mono.uu+1} The command has indeed failed with message: -Universe u already exists. +Universe uu already exists. monomono : Type@{MONOU+1} mono.monomono @@ -63,23 +63,23 @@ mono.monomono monomono : Type@{MONOU+1} mono - : Type@{mono.u+1} + : Type@{mono.uu+1} The command has indeed failed with message: -Universe u already exists. +Universe uu already exists. bobmorane = let tt := Type@{UnivBinders.32} in let ff := Type@{UnivBinders.34} in tt -> ff : Type@{max(UnivBinders.31,UnivBinders.33)} The command has indeed failed with message: -Universe u already bound. +Universe uu already bound. foo@{E M N} = Type@{M} -> Type@{N} -> Type@{E} : Type@{max(E+1,M+1,N+1)} (* E M N |= *) -foo@{u u0 v} = -Type@{u0} -> Type@{v} -> Type@{u} - : Type@{max(u+1,u0+1,v+1)} -(* u u0 v |= *) +foo@{uu u v} = +Type@{u} -> Type@{v} -> Type@{uu} + : Type@{max(uu+1,u+1,v+1)} +(* uu u v |= *) Inductive Empty@{E} : Type@{E} := (* E |= *) Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } @@ -103,45 +103,38 @@ The command has indeed failed with message: This object does not support universe names. The command has indeed failed with message: Cannot enforce v < u because u < gU < gV < v -bind_univs.mono = -Type@{bind_univs.mono.u} - : Type@{bind_univs.mono.u+1} -(* {bind_univs.mono.u} |= *) -bind_univs.poly@{u} = Type@{u} - : Type@{u+1} -(* u |= *) -insec@{v} = Type@{u} -> Type@{v} - : Type@{max(u+1,v+1)} +insec@{v} = Type@{uu} -> Type@{v} + : Type@{max(uu+1,v+1)} (* v |= *) Inductive insecind@{k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{k} (* k |= *) Arguments inseccstr _%type_scope -insec@{u v} = Type@{u} -> Type@{v} - : Type@{max(u+1,v+1)} -(* u v |= *) -Inductive insecind@{u k} : Type@{k+1} := - inseccstr : Type@{k} -> insecind@{u k} -(* u k |= *) +insec@{uu v} = Type@{uu} -> Type@{v} + : Type@{max(uu+1,v+1)} +(* uu v |= *) +Inductive insecind@{uu k} : Type@{k+1} := + inseccstr : Type@{k} -> insecind@{uu k} +(* uu k |= *) Arguments inseccstr _%type_scope insec2@{u} = Prop : Type@{Set+1} (* u |= *) -inmod@{u} = Type@{u} - : Type@{u+1} -(* u |= *) -SomeMod.inmod@{u} = Type@{u} - : Type@{u+1} -(* u |= *) -inmod@{u} = Type@{u} - : Type@{u+1} -(* u |= *) -Applied.infunct@{u v} = -inmod@{u} -> Type@{v} - : Type@{max(u+1,v+1)} -(* u v |= *) +inmod@{uu} = Type@{uu} + : Type@{uu+1} +(* uu |= *) +SomeMod.inmod@{uu} = Type@{uu} + : Type@{uu+1} +(* uu |= *) +inmod@{uu} = Type@{uu} + : Type@{uu+1} +(* uu |= *) +Applied.infunct@{uu v} = +inmod@{uu} -> Type@{v} + : Type@{max(uu+1,v+1)} +(* uu v |= *) axfoo@{i u u0} : Type@{u} -> Type@{i} (* i u u0 |= *) @@ -166,3 +159,13 @@ Arguments axbar' _%type_scope Expands to: Constant UnivBinders.axbar' The command has indeed failed with message: When declaring multiple axioms in one command, only the first is allowed a universe binder (which will be shared by the whole block). +foo@{i} = Type@{M.i} -> Type@{i} + : Type@{max(M.i+1,i+1)} +(* i |= *) +bind_univs.mono = +Type@{bind_univs.mono.u} + : Type@{bind_univs.mono.u+1} +(* {bind_univs.mono.u} |= *) +bind_univs.poly@{u} = Type@{u} + : Type@{u+1} +(* u |= *) diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index 582a5e969a..ed6e90b2a6 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -5,32 +5,32 @@ Set Printing Universes. (* Unset Strict Universe Declaration. *) (* universe binders on inductive types and record projections *) -Inductive Empty@{u} : Type@{u} := . +Inductive Empty@{uu} : Type@{uu} := . Print Empty. Set Primitive Projections. -Record PWrap@{u} (A:Type@{u}) := pwrap { punwrap : A }. +Record PWrap@{uu} (A:Type@{uu}) := pwrap { punwrap : A }. Print PWrap. Print punwrap. Unset Primitive Projections. -Record RWrap@{u} (A:Type@{u}) := rwrap { runwrap : A }. +Record RWrap@{uu} (A:Type@{uu}) := rwrap { runwrap : A }. Print RWrap. Print runwrap. (* universe binders also go on the constants for operational typeclasses. *) -Class Wrap@{u} (A:Type@{u}) := wrap : A. +Class Wrap@{uu} (A:Type@{uu}) := wrap : A. Print Wrap. Print wrap. (* Instance in lemma mode used to ignore the binders. *) -Instance bar@{u} : Wrap@{u} Set. Proof. exact nat. Qed. +Instance bar@{uu} : Wrap@{uu} Set. Proof. exact nat. Qed. Print bar. Unset Strict Universe Declaration. (* The universes in the binder come first, then the extra universes in order of appearance. *) -Definition foo@{u +} := Type -> Type@{v} -> Type@{u}. +Definition foo@{uu +} := Type -> Type@{v} -> Type@{uu}. Print foo. Check Type@{i} -> Type@{j}. @@ -40,13 +40,13 @@ Eval cbv in Type@{i} -> Type@{j}. Set Strict Universe Declaration. (* Binders even work with monomorphic definitions! *) -Monomorphic Definition mono@{u} := Type@{u}. +Monomorphic Definition mono@{uu} := Type@{uu}. Print mono. Check mono. -Check Type@{mono.u}. +Check Type@{mono.uu}. Module mono. - Fail Monomorphic Universe u. + Fail Monomorphic Universe uu. Monomorphic Universe MONOU. Monomorphic Definition monomono := Type@{MONOU}. @@ -60,28 +60,28 @@ Import mono. Check monomono. (* unqualified MONOU *) Check mono. (* still qualified mono.u *) -Monomorphic Constraint Set < UnivBinders.mono.u. +Monomorphic Constraint Set < UnivBinders.mono.uu. Module mono2. - Monomorphic Universe u. + Monomorphic Universe uu. End mono2. -Fail Monomorphic Definition mono2@{u} := Type@{u}. +Fail Monomorphic Definition mono2@{uu} := Type@{uu}. Module SecLet. Unset Universe Polymorphism. Section foo. - (* Fail Let foo@{} := Type@{u}. (* doesn't parse: Let foo@{...} doesn't exist *) *) + (* Fail Let foo@{} := Type@{uu}. (* doesn't parse: Let foo@{...} doesn't exist *) *) Unset Strict Universe Declaration. - Let tt : Type@{u} := Type@{v}. (* names disappear in the ether *) - Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* names disappear into space *) + Let tt : Type@{uu} := Type@{v}. (* names disappear in the ether *) + Let ff : Type@{uu}. Proof. exact Type@{v}. Qed. (* names disappear into space *) Definition bobmorane := tt -> ff. End foo. Print bobmorane. End SecLet. (* fun x x => foo is nonsense with local binders *) -Fail Definition fo@{u u} := Type@{u}. +Fail Definition fo@{uu uu} := Type@{uu}. (* Using local binders for printing. *) Print foo@{E M N}. @@ -106,14 +106,9 @@ Fail Print Coq.Init.Logic@{E}. Monomorphic Universes gU gV. Monomorphic Constraint gU < gV. Fail Lemma foo@{u v|u < gU, gV < v, v < u} : nat. -(* Universe binders survive through compilation, sections and modules. *) -Require TestSuite.bind_univs. -Print bind_univs.mono. -Print bind_univs.poly. - Section SomeSec. - Universe u. - Definition insec@{v} := Type@{u} -> Type@{v}. + Universe uu. + Definition insec@{v} := Type@{uu} -> Type@{v}. Print insec. Inductive insecind@{k} := inseccstr : Type@{k} -> insecind. @@ -129,7 +124,7 @@ End SomeSec2. Print insec2. Module SomeMod. - Definition inmod@{u} := Type@{u}. + Definition inmod@{uu} := Type@{uu}. Print inmod. End SomeMod. Print SomeMod.inmod. @@ -138,7 +133,7 @@ Print inmod. Module Type SomeTyp. Definition inmod := Type. End SomeTyp. Module SomeFunct (In : SomeTyp). - Definition infunct@{u v} := In.inmod@{u} -> Type@{v}. + Definition infunct@{uu v} := In.inmod@{uu} -> Type@{v}. End SomeFunct. Module Applied := SomeFunct(SomeMod). Print Applied.infunct. @@ -147,7 +142,7 @@ Print Applied.infunct. In polymorphic mode the domain Type gets separate universes for the different axioms, but all axioms have to declare all universes. In - polymorphic mode they get the same universes, ie the type is only + monomorphic mode they get the same universes, ie the type is only interpd once. *) Axiom axfoo@{i+} axbar : Type -> Type@{i}. Monomorphic Axiom axfoo'@{i+} axbar' : Type -> Type@{i}. @@ -155,3 +150,18 @@ Monomorphic Axiom axfoo'@{i+} axbar' : Type -> Type@{i}. About axfoo. About axbar. About axfoo'. About axbar'. Fail Axiom failfoo failbar@{i} : Type. + +(* Notation interaction *) +Module Notas. + Unset Universe Polymorphism. + Module Import M. Universe i. End M. + + Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}. + Print foo. (* must not print Type@{i} -> Type@{i} *) + +End Notas. + +(* Universe binders survive through compilation, sections and modules. *) +Require TestSuite.bind_univs. +Print bind_univs.mono. +Print bind_univs.poly. 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/evars.v b/test-suite/success/evars.v index 253b48e4d9..2308656f7c 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -426,3 +426,12 @@ Abort. (* (reported as bug #7356) *) Check fun (P : nat -> Prop) (x:nat) (h:P x) => exist _ ?[z] (h : P ?z). + +(* A printing check in passing *) + +Axiom abs : forall T, T. +Fail Type let x := _ in + ltac:( + let t := type of x in + unify x (abs t); + exact 0). 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/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 5d49d1635c..01b1025da1 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -1100,7 +1100,7 @@ let interp_constr flags ist c = let () = let intern = intern_constr in let interp ist c = interp_constr constr_flags ist c in - let print env c = str "constr:(" ++ Printer.pr_lglob_constr_env env c ++ str ")" in + let print env sigma c = str "constr:(" ++ Printer.pr_lglob_constr_env env sigma c ++ str ")" in let subst subst c = Detyping.subst_glob_constr (Global.env()) subst c in let obj = { ml_intern = intern; @@ -1113,7 +1113,7 @@ let () = let () = let intern = intern_constr in let interp ist c = interp_constr open_constr_no_classes_flags ist c in - let print env c = str "open_constr:(" ++ Printer.pr_lglob_constr_env env c ++ str ")" in + let print env sigma c = str "open_constr:(" ++ Printer.pr_lglob_constr_env env sigma c ++ str ")" in let subst subst c = Detyping.subst_glob_constr (Global.env()) subst c in let obj = { ml_intern = intern; @@ -1125,7 +1125,7 @@ let () = let () = let interp _ id = return (Value.of_ident id) in - let print _ id = str "ident:(" ++ Id.print id ++ str ")" in + let print _ _ id = str "ident:(" ++ Id.print id ++ str ")" in let obj = { ml_intern = (fun _ _ id -> GlbVal id, gtypref t_ident); ml_interp = interp; @@ -1147,7 +1147,7 @@ let () = let sigma = Evd.from_env env in Patternops.subst_pattern env sigma subst c in - let print env pat = str "pattern:(" ++ Printer.pr_lconstr_pattern_env env Evd.empty pat ++ str ")" in + let print env sigma pat = str "pattern:(" ++ Printer.pr_lconstr_pattern_env env sigma pat ++ str ")" in let interp _ c = return (Value.of_pattern c) in let obj = { ml_intern = intern; @@ -1169,7 +1169,7 @@ let () = return (Value.of_ext val_preterm c) in let subst subst c = Detyping.subst_glob_constr (Global.env()) subst c in - let print env c = str "preterm:(" ++ Printer.pr_lglob_constr_env env c ++ str ")" in + let print env sigma c = str "preterm:(" ++ Printer.pr_lglob_constr_env env sigma c ++ str ")" in let obj = { ml_intern = (fun _ _ e -> Empty.abort e); ml_interp = interp; @@ -1193,7 +1193,7 @@ let () = in let subst s c = Globnames.subst_global_reference s c in let interp _ gr = return (Value.of_reference gr) in - let print _ = function + let print _ _ = function | GlobRef.VarRef id -> str "reference:(" ++ str "&" ++ Id.print id ++ str ")" | r -> str "reference:(" ++ Printer.pr_global r ++ str ")" in @@ -1241,7 +1241,7 @@ let () = return (Tac2ffi.of_closure (Tac2ffi.abstract len clos)) in let subst s (ids, tac) = (ids, Genintern.substitute Ltac_plugin.Tacarg.wit_tactic s tac) in - let print env (ids, tac) = + let print env sigma (ids, tac) = let ids = if List.is_empty ids then mt () else pr_sequence Id.print ids ++ spc () ++ str "|-" ++ spc () @@ -1290,7 +1290,7 @@ let () = return (Tac2ffi.of_closure (Tac2ffi.abstract len clos)) in let subst s (ids, tac) = (ids, Genintern.substitute Tacarg.wit_tactic s tac) in - let print env (ids, tac) = + let print env sigma (ids, tac) = let ids = if List.is_empty ids then mt () else pr_sequence Id.print ids ++ str " |- " diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index eebd6635fa..d0655890a7 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -853,8 +853,10 @@ let pr_frame = function str "Prim <" ++ str ml.mltac_plugin ++ str ":" ++ str ml.mltac_tactic ++ str ">" | FrExtn (tag, arg) -> let obj = Tac2env.interp_ml_object tag in + let env = Global.env () in + let sigma = Evd.from_env env in str "Extn " ++ str (Tac2dyn.Arg.repr tag) ++ str ":" ++ spc () ++ - obj.Tac2env.ml_print (Global.env ()) arg + obj.Tac2env.ml_print env sigma arg let () = register_handler begin function | Tac2interp.LtacError (kn, args) -> diff --git a/user-contrib/Ltac2/tac2env.ml b/user-contrib/Ltac2/tac2env.ml index 6c2133f8f2..f6d07e484b 100644 --- a/user-contrib/Ltac2/tac2env.ml +++ b/user-contrib/Ltac2/tac2env.ml @@ -253,7 +253,7 @@ type ('a, 'b) ml_object = { ml_intern : 'r. (raw_tacexpr, glb_tacexpr, 'r) intern_fun -> ('a, 'b or_glb_tacexpr, 'r) intern_fun; ml_subst : Mod_subst.substitution -> 'b -> 'b; ml_interp : environment -> 'b -> valexpr Proofview.tactic; - ml_print : Environ.env -> 'b -> Pp.t; + ml_print : Environ.env -> Evd.evar_map -> 'b -> Pp.t; } module MLTypeObj = diff --git a/user-contrib/Ltac2/tac2env.mli b/user-contrib/Ltac2/tac2env.mli index 2468959810..af1197c24c 100644 --- a/user-contrib/Ltac2/tac2env.mli +++ b/user-contrib/Ltac2/tac2env.mli @@ -122,7 +122,7 @@ type ('a, 'b) ml_object = { ml_intern : 'r. (raw_tacexpr, glb_tacexpr, 'r) intern_fun -> ('a, 'b or_glb_tacexpr, 'r) intern_fun; ml_subst : Mod_subst.substitution -> 'b -> 'b; ml_interp : environment -> 'b -> valexpr Proofview.tactic; - ml_print : Environ.env -> 'b -> Pp.t; + ml_print : Environ.env -> Evd.evar_map -> 'b -> Pp.t; } val define_ml_object : ('a, 'b) Tac2dyn.Arg.tag -> ('a, 'b) ml_object -> unit diff --git a/user-contrib/Ltac2/tac2print.ml b/user-contrib/Ltac2/tac2print.ml index a37fe2f7a5..fe62de1fb3 100644 --- a/user-contrib/Ltac2/tac2print.ml +++ b/user-contrib/Ltac2/tac2print.ml @@ -274,7 +274,9 @@ let pr_glbexpr_gen lvl c = paren (hov 0 (c ++ spc () ++ (pr_sequence (pr_glbexpr E0) cl))) | GTacExt (tag, arg) -> let tpe = interp_ml_object tag in - hov 0 (tpe.ml_print (Global.env ()) arg) (* FIXME *) + let env = Global.env() in + let sigma = Evd.from_env env in + hov 0 (tpe.ml_print env sigma arg) (* FIXME *) | GTacPrm (prm, args) -> let args = match args with | [] -> mt () 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/declareUniv.ml b/vernac/declareUniv.ml index 1705915e70..1987d48e0f 100644 --- a/vernac/declareUniv.ml +++ b/vernac/declareUniv.ml @@ -109,9 +109,8 @@ let do_universe ~poly l = let do_constraint ~poly l = let open Univ in - let u_of_id x = - Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x - in + let evd = Evd.from_env (Global.env ()) in + let u_of_id x = Constrintern.interp_known_level evd x in let constraints = List.fold_left (fun acc (l, d, r) -> let lu = u_of_id l and ru = u_of_id r in Constraint.add (lu, d, ru) acc) diff --git a/vernac/declareUniv.mli b/vernac/declareUniv.mli index e4d1d5dc65..ca990a58eb 100644 --- a/vernac/declareUniv.mli +++ b/vernac/declareUniv.mli @@ -17,4 +17,4 @@ exception AlreadyDeclared of (string option * Id.t) val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit val do_universe : poly:bool -> lident list -> unit -val do_constraint : poly:bool -> Glob_term.glob_constraint list -> unit +val do_constraint : poly:bool -> Constrexpr.univ_constraint_expr list -> unit diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 9d86ea90e6..d35e13c4ef 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -572,6 +572,13 @@ let rec explain_evar_kind env sigma evk ty = strbrk "the type of " ++ Id.print id | Evar_kinds.BinderType Anonymous -> strbrk "the type of this anonymous binder" + | Evar_kinds.EvarType (ido,evk) -> + let pp = match ido with + | Some id -> str "?" ++ Id.print id + | None -> + try pr_existential_key sigma evk + with (* defined *) Not_found -> strbrk "an internal placeholder" in + strbrk "the type of " ++ pp | Evar_kinds.ImplicitArg (c,(n,ido),b) -> let id = Option.get ido in strbrk "the implicit parameter " ++ Id.print id ++ spc () ++ str "of" ++ @@ -961,7 +968,7 @@ let explain_not_match_error = function status (not b) ++ str" declaration was found" | IncompatibleUniverses incon -> str"the universe constraints are inconsistent: " ++ - Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes incon + Univ.explain_universe_inconsistency UnivNames.(pr_with_global_universes empty_binders) incon | IncompatiblePolymorphism (env, t1, t2) -> str "conversion of polymorphic values generates additional constraints: " ++ quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t1) ++ spc () ++ @@ -1218,7 +1225,7 @@ let error_large_non_prop_inductive_not_in_type () = str "Large non-propositional inductive types must be in Type." let error_inductive_missing_constraints (us,ind_univ) = - let pr_u = Univ.Universe.pr_with UnivNames.pr_with_global_universes in + let pr_u = Univ.Universe.pr_with UnivNames.(pr_with_global_universes empty_binders) in str "Missing universe constraint declared for inductive type:" ++ spc() ++ v 0 (prlist_with_sep spc (fun u -> hov 0 (pr_u u ++ str " <= " ++ pr_u ind_univ)) @@ -1406,7 +1413,7 @@ let _ = CErrors.register_handler (wrap_unhandled explain_exn_default) let rec vernac_interp_error_handler = function | Univ.UniverseInconsistency i -> str "Universe inconsistency." ++ spc() ++ - Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i ++ str "." + Univ.explain_universe_inconsistency UnivNames.(pr_with_global_universes empty_binders) i ++ str "." | TypeError(ctx,te) -> let te = map_ptype_error EConstr.of_constr te in explain_type_error ctx Evd.empty te diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 01873918aa..ff4365c8d3 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -60,8 +60,8 @@ let pr_red_expr = keyword let pr_uconstraint (l, d, r) = - pr_glob_sort_name l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ - pr_glob_sort_name r + pr_sort_name_expr l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ + pr_sort_name_expr r let pr_univ_name_list = function | None -> mt () diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 840754ccc6..0fc6c7f87b 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -206,7 +206,7 @@ let print_if_is_coercion ref = let pr_template_variables = function | [] -> mt () - | vars -> str "on " ++ prlist_with_sep spc UnivNames.pr_with_global_universes vars + | vars -> str "on " ++ prlist_with_sep spc UnivNames.(pr_with_global_universes empty_binders) vars let print_polymorphism ref = let poly = Global.is_polymorphic ref in @@ -668,7 +668,7 @@ let gallina_print_syntactic_def env kn = spc () ++ str ":=") ++ spc () ++ Constrextern.without_specific_symbols - [Notation.SynDefRule kn] (pr_glob_constr_env env) c) + [Notation.SynDefRule kn] (pr_glob_constr_env env (Evd.from_env env)) c) module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> Pp.t option end) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 0f63dfe5ce..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)) @@ -353,9 +354,9 @@ let universe_subgraph ?loc kept univ = let open Univ in let sigma = Evd.from_env (Global.env()) in let parse q = - let q = Glob_term.(GType q) in + let q = Constrexpr.CType q in (* this function has a nice error message for not found univs *) - Pretyping.interp_known_glob_level ?loc sigma q + Constrintern.interp_known_level sigma q in let kept = List.fold_left (fun kept q -> LSet.add (parse q) kept) LSet.empty kept in let csts = UGraph.constraints_for ~kept univ in @@ -377,7 +378,7 @@ let print_universes ?loc ~sort ~subgraph dst = if Global.is_joined_environment () then mt () else str"There may remain asynchronous universe constraints" in - let prl = UnivNames.pr_with_global_universes in + let prl = UnivNames.(pr_with_global_universes empty_binders) in begin match dst with | None -> UGraph.pr_universes prl univ ++ pr_remaining | Some s -> dump_universes_gen (fun u -> Pp.string_of_ppcmds (prl u)) univ s @@ -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 = @@ -1829,11 +1846,11 @@ let vernac_print ~pstate = | PrintHintDbName s -> Hints.pr_hint_db_by_name env sigma s | PrintHintDb -> Hints.pr_searchtable env sigma | PrintScopes -> - Notation.pr_scopes (Constrextern.without_symbols (pr_glob_constr_env env)) + Notation.pr_scopes (Constrextern.without_symbols (pr_glob_constr_env env sigma)) | PrintScope s -> - Notation.pr_scope (Constrextern.without_symbols (pr_glob_constr_env env)) s + Notation.pr_scope (Constrextern.without_symbols (pr_glob_constr_env env sigma)) s | PrintVisibility s -> - Notation.pr_visibility (Constrextern.without_symbols (pr_glob_constr_env env)) s + Notation.pr_visibility (Constrextern.without_symbols (pr_glob_constr_env env sigma)) s | PrintAbout (ref_or_by_not,udecl,glnumopt) -> print_about_hyp_globs ~pstate ref_or_by_not udecl glnumopt | PrintImplicit qid -> @@ -1867,9 +1884,9 @@ let vernac_locate ~pstate = let open Constrexpr in function | LocateTerm {v=AN qid} -> Prettyp.print_located_term qid | LocateAny {v=ByNotation (ntn, sc)} (* TODO : handle Ltac notations *) | LocateTerm {v=ByNotation (ntn, sc)} -> - let _, env = get_current_or_global_context ~pstate in + let sigma, env = get_current_or_global_context ~pstate in Notation.locate_notation - (Constrextern.without_symbols (pr_glob_constr_env env)) ntn sc + (Constrextern.without_symbols (pr_glob_constr_env env sigma)) ntn sc | LocateLibrary qid -> print_located_library qid | LocateModule qid -> Prettyp.print_located_module qid | LocateOther (s, qid) -> Prettyp.print_located_other s qid diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index defb0691c0..2e360cf969 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -129,8 +129,6 @@ type option_setting = (** Identifier and optional list of bound universes and constraints. *) -type sort_expr = Sorts.family - type definition_expr = | ProveBody of local_binder_expr list * constr_expr | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr @@ -210,8 +208,8 @@ type proof_end = | Proved of opacity_flag * lident option type scheme = - | InductionScheme of bool * qualid or_by_notation * sort_expr - | CaseScheme of bool * qualid or_by_notation * sort_expr + | InductionScheme of bool * qualid or_by_notation * Sorts.family + | CaseScheme of bool * qualid or_by_notation * Sorts.family | EqualityScheme of qualid or_by_notation type section_subset_expr = @@ -341,7 +339,7 @@ type nonrec vernac_expr = | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list | VernacUniverse of lident list - | VernacConstraint of Glob_term.glob_constraint list + | VernacConstraint of univ_constraint_expr list (* Gallina extensions *) | VernacBeginSection of lident |