diff options
166 files changed, 1623 insertions, 784 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 99ae4c23ce..bd015a40b6 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -17,9 +17,9 @@ stages: # some default values variables: - # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here - # for reference] - CACHEKEY: "bionic_coq-V2020-10-12-V89" + # Format: $IMAGE-V$DATE-$hash + # The $hash is the first 10 characters of the md5 of the dockerfile + CACHEKEY: "bionic_coq-V2020-11-26-db194d584e" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -59,6 +59,7 @@ before_script: - eval $(opam env) - opam list - opam config list + - dev/tools/check-cachekey.sh ################ GITLAB CACHING ###################### # - use artifacts between jobs # @@ -711,7 +712,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 +739,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 +797,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/clib/hashset.ml b/clib/hashset.ml index 89136e7870..ae43e7db92 100644 --- a/clib/hashset.ml +++ b/clib/hashset.ml @@ -52,7 +52,7 @@ module Make (E : EqType) = mutable rover : int; (* for internal bookkeeping *) } - let get_index t h = (h land max_int) mod (Array.length t.table) + let get_index t h = (h land max_int) mod (Array.length t) let limit = 7 let over_limit = 2 @@ -135,7 +135,7 @@ module Make (E : EqType) = let add_weak ob oh oi = let setter nb ni _ = Weak.blit ob oi nb ni 1 in let h = oh.(oi) in - add_aux newt setter None h (get_index newt h); + add_aux newt setter None h (get_index newt.table h); in iter_weak add_weak t; t.table <- newt.table; @@ -178,24 +178,28 @@ module Make (E : EqType) = in loop 0 - let find_or h t d ifnotfound = - let index = get_index t h in - let bucket = t.table.(index) in + let repr h d t = + let table = t.table in + let index = get_index table h in + let bucket = table.(index) in let hashes = t.hashes.(index) in let sz = Weak.length bucket in - let rec loop i = - if i >= sz then ifnotfound index - else if Int.equal h hashes.(i) then begin + let pos = ref 0 in + let ans = ref None in + while !pos < sz && !ans == None do + let i = !pos in + if Int.equal h hashes.(i) then begin match Weak.get bucket i with - | Some v when E.eq v d -> v - | _ -> loop (i + 1) - end else loop (i + 1) - in - loop 0 - - let repr h d t = - let ifnotfound index = add_aux t Weak.set (Some d) h index; d in - find_or h t d ifnotfound + | Some v as res when E.eq v d -> ans := res + | _ -> incr pos + end else incr pos + done; + if !pos >= sz then + let () = add_aux t Weak.set (Some d) h index in + d + else match !ans with + | None -> assert false + | Some v -> v let stats t = let fold accu bucket = max (count_bucket 0 bucket 0) accu in 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/README-developers.md b/dev/ci/README-developers.md index 801e29ac95..f5ca6c495f 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -171,7 +171,7 @@ loaded by subsequent jobs. **IMPORTANT**: When updating Coq's CI docker image, you must modify the `CACHEKEY` variable in [`.gitlab-ci.yml`](../../.gitlab-ci.yml) -and [`Dockerfile`](docker/bionic_coq/Dockerfile) +(see comment near it for details). The Docker building job reuses the uploaded image if it is available, but if you wish to save more time you can skip the job by setting 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..96d96328f8 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,5 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-10-12-V89" -# ^^ Update when modifying this file. +# Update CACHEKEY in the .gitlab-ci.yml when modifying this file. FROM ubuntu:bionic LABEL maintainer="e@x80.org" @@ -42,8 +41,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 +61,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/lint-repository.sh b/dev/lint-repository.sh index 7701264ad1..0bad2f4c62 100755 --- a/dev/lint-repository.sh +++ b/dev/lint-repository.sh @@ -32,4 +32,7 @@ find . "(" -path ./.git -prune ")" -o -type f -print0 | echo Checking overlays dev/tools/check-overlays.sh || CODE=1 +echo Checking CACHEKEY +dev/tools/check-cachekey.sh || CODE=1 + exit $CODE diff --git a/dev/shim/dune b/dev/shim/dune index 84b2e642e8..8006c629ed 100644 --- a/dev/shim/dune +++ b/dev/shim/dune @@ -7,7 +7,7 @@ (with-stdout-to coqtop-prelude (progn (echo "#!/usr/bin/env bash\n") - (bash "echo \"$(pwd)/%{bin:coqtop} -coqlib $(pwd)/%{project_root}\" \\$@") + (bash "echo '$(dirname $0)/%{bin:coqtop} -coqlib $(dirname $0)/%{project_root}' \\$@") (run chmod +x %{targets}))))) (rule @@ -19,7 +19,7 @@ (with-stdout-to coqc-prelude (progn (echo "#!/usr/bin/env bash\n") - (bash "echo \"$(pwd)/%{bin:coqc} -coqlib $(pwd)/%{project_root}\" \\$@") + (bash "echo '$(dirname $0)/%{bin:coqc} -coqlib $(dirname $0)/%{project_root}' \\$@") (run chmod +x %{targets}))))) (rule @@ -32,7 +32,7 @@ (with-stdout-to %{targets} (progn (echo "#!/usr/bin/env bash\n") - (bash "echo \"$(pwd)/%{bin:coqtop.byte} -coqlib $(pwd)/%{project_root}\" \\$@") + (bash "echo '$(dirname $0)/%{bin:coqtop.byte} -coqlib $(dirname $0)/%{project_root}' \\$@") (run chmod +x %{targets}))))) (rule @@ -48,5 +48,5 @@ (with-stdout-to coqide-prelude (progn (echo "#!/usr/bin/env bash\n") - (bash "echo \"$(pwd)/%{bin:coqide} -coqlib $(pwd)/%{project_root}\" \\$@") + (bash "echo '$(dirname $0)/%{bin:coqide} -coqlib $(dirname $0)/%{project_root}' \\$@") (run chmod +x %{targets}))))) diff --git a/dev/tools/check-cachekey.sh b/dev/tools/check-cachekey.sh new file mode 100755 index 0000000000..15e3fa93cb --- /dev/null +++ b/dev/tools/check-cachekey.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +hash=$(md5sum dev/ci/docker/bionic_coq/Dockerfile | head -c 10) +key=$(grep CACHEKEY: .gitlab-ci.yml) +keyhash=${key%\"} +keyhash=${keyhash##*-} +if ! [ "$hash" = "$keyhash" ]; then + echo "Bad CACHEKEY: expected '$hash' but got '$keyhash'" + exit 1 +fi 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/01-kernel/13501-fix-13495.rst b/doc/changelog/01-kernel/13501-fix-13495.rst new file mode 100644 index 0000000000..5c81efa8b9 --- /dev/null +++ b/doc/changelog/01-kernel/13501-fix-13495.rst @@ -0,0 +1,7 @@ +- **Fixed:** + Fix an incompleteness in the typechecking of `match` for + cumulative inductive types. This could result in breaking subject + reduction. + (`#13501 <https://github.com/coq/coq/pull/13501>`_, + fixes `#13495 <https://github.com/coq/coq/issues/13495>`_, + by Matthieu Sozeau). 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/inductive.ml b/kernel/inductive.ml index e34b3c0b47..ce12d65614 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -330,33 +330,45 @@ let check_allowed_sort ksort specif = let s = inductive_sort_family (snd specif) in raise (LocalArity (Some(elim_sort specif, ksort,s,error_elim_explain ksort s))) -let is_correct_arity env c pj ind specif params = +let check_correct_arity env c pj ind specif params = + (* We use l2r:true for compat with old versions which used CONV + instead of CUMUL called with arguments flipped. It is relevant + for performance eg in bedrock / Kami. *) let arsign,_ = get_instantiated_arity ind specif params in - let rec srec env pt ar = + let rec srec env ar pt = let pt' = whd_all env pt in - match kind pt', ar with - | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' -> - let () = - try conv env a1 a1' - with NotConvertible -> raise (LocalArity None) in - srec (push_rel (LocalAssum (na1,a1)) env) t ar' - (* The last Prod domain is the type of the scrutinee *) - | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *) - let env' = push_rel (LocalAssum (na1,a1)) env in - let ksort = match kind (whd_all env' a2) with - | Sort s -> Sorts.family s - | _ -> raise (LocalArity None) in - let dep_ind = build_dependent_inductive ind specif params in - let _ = - try conv env a1 dep_ind - with NotConvertible -> raise (LocalArity None) in - check_allowed_sort ksort specif - | _, (LocalDef _ as d)::ar' -> - srec (push_rel d env) (lift 1 pt') ar' - | _ -> - raise (LocalArity None) + match ar, kind pt' with + | (LocalAssum (_,a1))::ar', Prod (na1,a1',t) -> + let () = + try conv_leq ~l2r:true env a1 a1' + with NotConvertible -> raise (LocalArity None) in + srec (push_rel (LocalAssum (na1,a1)) env) ar' t + (* The last Prod domain is the type of the scrutinee *) + | [], Prod (na1,a1',a2) -> + let env' = push_rel (LocalAssum (na1,a1')) env in + let ksort = match kind (whd_all env' a2) with + | Sort s -> Sorts.family s + | _ -> raise (LocalArity None) + in + let dep_ind = build_dependent_inductive ind specif params in + let () = + (* This ensures that the type of the scrutinee is <= the + inductive type declared in the predicate. *) + try conv_leq ~l2r:true env dep_ind a1' + with NotConvertible -> raise (LocalArity None) + in + let () = check_allowed_sort ksort specif in + (* We return the "higher" inductive universe instance from the predicate, + the branches must be typeable using these universes. + The find_rectype call cannot fail due to the cumulativity check above. *) + let (pind, _args) = find_rectype env a1' in + pind + | (LocalDef _ as d)::ar', _ -> + srec (push_rel d env) ar' (lift 1 pt') + | _ -> + raise (LocalArity None) in - try srec env pj.uj_type (List.rev arsign) + try srec env (List.rev arsign) pj.uj_type with LocalArity kinds -> error_elim_arity env ind c pj kinds @@ -387,17 +399,16 @@ let build_branches_type (ind,u) (_,mip as specif) params p = let build_case_type env n p c realargs = whd_betaiota env (Term.lambda_appvect_assum (n+1) p (Array.of_list (realargs@[c]))) -let type_case_branches env (pind,largs) pj c = - let specif = lookup_mind_specif env (fst pind) in +let type_case_branches env ((ind, _ as pind),largs) pj c = + let specif = lookup_mind_specif env ind in let nparams = inductive_params specif in let (params,realargs) = List.chop nparams largs in let p = pj.uj_val in - let () = is_correct_arity env c pj pind specif params in + let pind = check_correct_arity env c pj pind specif params in let lc = build_branches_type pind specif params p in let ty = build_case_type env (snd specif).mind_nrealdecls p c realargs in (lc, ty) - (************************************************************************) (* Checking the case annotation is relevant *) 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..faad792ea9 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -458,7 +458,8 @@ let string_of_genarg_arg (ArgumentType arg) = | l -> pr_in (spc () ++ prlist_with_sep spc pr_id l) let pr_in_hyp_as prc pr_id = function - | (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat + | [] -> mt () + | l -> pr_in (spc () ++ prlist_with_sep pr_comma (fun (id,ipat) -> pr_id id ++ pr_as_ipat prc ipat) l) let pr_in_clause pr_id = function | { onhyps=None; concl_occs=NoOccurrences } -> @@ -755,7 +756,7 @@ let pr_goal_selector ~toplevel s = (if a then mt() else primitive "simple ") ++ primitive (with_evars ev "apply") ++ spc () ++ prlist_with_sep pr_comma pr_with_bindings_arg cb ++ - prlist_with_sep spc (pr_in_hyp_as (pr.pr_dconstr env sigma) pr.pr_name) inhyp + pr_non_empty_arg (pr_in_hyp_as (pr.pr_dconstr env sigma) pr.pr_name) inhyp ) | TacElim (ev,cb,cbo) -> hov 1 ( @@ -1130,12 +1131,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 +1167,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 +1190,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 +1213,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 +1243,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 +1302,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) @@ -1317,6 +1318,7 @@ let () = let pr_unit _ = str "()" in let open Genprint in register_basic_print0 wit_int_or_var (pr_or_var int) (pr_or_var int) int; + register_basic_print0 wit_nat_or_var (pr_or_var int) (pr_or_var int) int; register_basic_print0 wit_ref pr_qualid (pr_or_var (pr_located pr_global)) pr_global; register_basic_print0 wit_smart_global 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/evarconv.ml b/pretyping/evarconv.ml index cdf2922516..d0b724b755 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -448,6 +448,58 @@ let compare_cumulative_instances evd variances u u' = Success evd | Inr p -> UnifFailure (evd, UnifUnivInconsistency p) +let compare_heads env evd ~nargs term term' = + let check_strict evd u u' = + let cstrs = Univ.enforce_eq_instances u u' Univ.Constraint.empty in + try Success (Evd.add_constraints evd cstrs) + with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p) + in + match EConstr.kind evd term, EConstr.kind evd term' with + | Const (c, u), Const (c', u') when QConstant.equal env c c' -> + if Int.equal nargs 1 && Environ.is_array_type env c + then + let u = EInstance.kind evd u and u' = EInstance.kind evd u' in + compare_cumulative_instances evd [|Univ.Variance.Irrelevant|] u u' + else + let u = EInstance.kind evd u and u' = EInstance.kind evd u' in + check_strict evd u u' + | Const _, Const _ -> UnifFailure (evd, NotSameHead) + | Ind ((mi,i) as ind , u), Ind (ind', u') when Names.Ind.CanOrd.equal ind ind' -> + if EInstance.is_empty u && EInstance.is_empty u' then Success evd + else + let u = EInstance.kind evd u and u' = EInstance.kind evd u' in + let mind = Environ.lookup_mind mi env in + let open Declarations in + begin match mind.mind_variance with + | None -> check_strict evd u u' + | Some variances -> + let needed = Reduction.inductive_cumulativity_arguments (mind,i) in + if not (Int.equal nargs needed) + then check_strict evd u u' + else + compare_cumulative_instances evd variances u u' + end + | Ind _, Ind _ -> UnifFailure (evd, NotSameHead) + | Construct (((mi,ind),ctor as cons), u), Construct (cons', u') + when Names.Construct.CanOrd.equal cons cons' -> + if EInstance.is_empty u && EInstance.is_empty u' then Success evd + else + let u = EInstance.kind evd u and u' = EInstance.kind evd u' in + let mind = Environ.lookup_mind mi env in + let open Declarations in + begin match mind.mind_variance with + | None -> check_strict evd u u' + | Some variances -> + let needed = Reduction.constructor_cumulativity_arguments (mind,ind,ctor) in + if not (Int.equal nargs needed) + then check_strict evd u u' + else + Success (compare_constructor_instances evd u u') + end + | Construct _, Construct _ -> UnifFailure (evd, NotSameHead) + | _, _ -> anomaly (Pp.str "") + + let conv_fun f flags on_types = let typefn env evd pbty term1 term2 = let flags = { (default_flags env) with @@ -556,65 +608,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty else evar_eqappr_x flags env' evd CONV out2 out1 in let rigids env evd sk term sk' term' = - let check_strict evd u u' = - let cstrs = Univ.enforce_eq_instances u u' Univ.Constraint.empty in - try Success (Evd.add_constraints evd cstrs) - with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p) - in - let compare_heads evd = - match EConstr.kind evd term, EConstr.kind evd term' with - | Const (c, u), Const (c', u') when QConstant.equal env c c' -> - if Int.equal (Stack.args_size sk) 1 && Environ.is_array_type env c - then - let u = EInstance.kind evd u and u' = EInstance.kind evd u' in - compare_cumulative_instances evd [|Univ.Variance.Irrelevant|] u u' - else - let u = EInstance.kind evd u and u' = EInstance.kind evd u' in - check_strict evd u u' - | Const _, Const _ -> UnifFailure (evd, NotSameHead) - | Ind ((mi,i) as ind , u), Ind (ind', u') when Names.Ind.CanOrd.equal ind ind' -> - if EInstance.is_empty u && EInstance.is_empty u' then Success evd - else - let u = EInstance.kind evd u and u' = EInstance.kind evd u' in - let mind = Environ.lookup_mind mi env in - let open Declarations in - begin match mind.mind_variance with - | None -> check_strict evd u u' - | Some variances -> - let nparamsaplied = Stack.args_size sk in - let nparamsaplied' = Stack.args_size sk' in - let needed = Reduction.inductive_cumulativity_arguments (mind,i) in - if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed) - then check_strict evd u u' - else - compare_cumulative_instances evd variances u u' - end - | Ind _, Ind _ -> UnifFailure (evd, NotSameHead) - | Construct (((mi,ind),ctor as cons), u), Construct (cons', u') - when Names.Construct.CanOrd.equal cons cons' -> - if EInstance.is_empty u && EInstance.is_empty u' then Success evd - else - let u = EInstance.kind evd u and u' = EInstance.kind evd u' in - let mind = Environ.lookup_mind mi env in - let open Declarations in - begin match mind.mind_variance with - | None -> check_strict evd u u' - | Some variances -> - let nparamsaplied = Stack.args_size sk in - let nparamsaplied' = Stack.args_size sk' in - let needed = Reduction.constructor_cumulativity_arguments (mind,ind,ctor) in - if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed) - then check_strict evd u u' - else - Success (compare_constructor_instances evd u u') - end - | Construct _, Construct _ -> UnifFailure (evd, NotSameHead) - | _, _ -> anomaly (Pp.str "") - in - ise_and evd [(fun i -> - try compare_heads i - with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); - (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk sk')] + let nargs = Stack.args_size sk in + let nargs' = Stack.args_size sk' in + if not (Int.equal nargs nargs') then UnifFailure (evd, NotSameArgSize) + else + ise_and evd [(fun i -> + try compare_heads env i ~nargs term term' + with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); + (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk sk')] in let consume on_left (_, skF as apprF) (_,skM as apprM) i = if not (Stack.is_empty skF && Stack.is_empty skM) then diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index a5a8d1f916..be03ced7eb 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -84,6 +84,12 @@ val check_conv_record : env -> evar_map -> (constr Stack.t * constr Stack.t) * constr * (int option * constr) +(** Compares two constants/inductives/constructors unifying their universes. + It required the number of arguments applied to the c/i/c in order to decided + the kind of check it must perform. *) +val compare_heads : env -> evar_map -> + nargs:int -> EConstr.t -> EConstr.t -> Evarsolve.unification_result + (** Try to solve problems of the form ?x[args] = c by second-order matching, using typing to select occurrences *) diff --git a/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/eqdecide.ml b/tactics/eqdecide.ml index d4cc193eb3..9b3f9053cd 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -123,8 +123,8 @@ let idy = Id.of_string "y" let mkGenDecideEqGoal rectype ops g = let hypnames = pf_ids_set_of_hyps g in - let xname = next_ident_away idx hypnames - and yname = next_ident_away idy hypnames in + let xname = next_ident_away idx hypnames in + let yname = next_ident_away idy (Id.Set.add xname hypnames) in (mkNamedProd (make_annot xname Sorts.Relevant) rectype (mkNamedProd (make_annot yname Sorts.Relevant) rectype (mkDecideEqGoal true ops 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/bugs/closed/bug_13493.v b/test-suite/bugs/closed/bug_13493.v new file mode 100644 index 0000000000..779df8e7f2 --- /dev/null +++ b/test-suite/bugs/closed/bug_13493.v @@ -0,0 +1,7 @@ +Set Mangle Names. + +Goal forall (m n:nat), True. + intros m n. compare m n. + - constructor. + - constructor. +Qed. diff --git a/test-suite/bugs/closed/bug_13495.v b/test-suite/bugs/closed/bug_13495.v new file mode 100644 index 0000000000..489574b854 --- /dev/null +++ b/test-suite/bugs/closed/bug_13495.v @@ -0,0 +1,18 @@ +Universe u. +(* Constraint Set < u. *) +Polymorphic Cumulative Record pack@{u} := Pack { pack_type : Type@{u} }. +(* u is covariant *) + +Polymorphic Definition pack_id@{u} (p : pack@{u}) : pack@{u} := + match p with + | Pack T => Pack T + end. +Definition packid_nat (p : pack@{Set}) := pack_id@{u} p. +(* No constraints: Set <= u *) + +Definition sr_dont_break := Eval compute in packid_nat. +(* Incorrect elimination of "p" in the inductive type "pack": + ill-formed elimination predicate. + + This is because it tries to enforce Set = u + *) 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/Tactics.out b/test-suite/output/Tactics.out index 3f07261ca6..01bf727ebc 100644 --- a/test-suite/output/Tactics.out +++ b/test-suite/output/Tactics.out @@ -9,3 +9,4 @@ H is already used. a The command has indeed failed with message: This variable is used in hypothesis H. +Ltac test a b c d e := apply a, b in c as [], d, e as -> diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v index 8526e43a23..845bccc548 100644 --- a/test-suite/output/Tactics.v +++ b/test-suite/output/Tactics.v @@ -38,3 +38,10 @@ Fail intros ((n,_),H). Abort. End IntroWildcard. + +Module ApplyIn. + +Ltac test a b c d e := apply a, b in c as [], d, e as ->. +Print test. + +End ApplyIn. 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 |