diff options
86 files changed, 688 insertions, 597 deletions
diff --git a/.gitattributes b/.gitattributes index 47538be4a3..58b1a31d36 100644 --- a/.gitattributes +++ b/.gitattributes @@ -11,17 +11,16 @@ # chunk, so we disable blank-at-eof. * -whitespace -# tabs are allowed in Makefiles. -Makefile* whitespace=blank-at-eol -tools/CoqMakefile.in whitespace=blank-at-eol - # in general we don't want tabs. *.asciidoc whitespace=blank-at-eol,tab-in-indent *.bib whitespace=blank-at-eol,tab-in-indent *.c whitespace=blank-at-eol,tab-in-indent *.css whitespace=blank-at-eol,tab-in-indent *.dtd whitespace=blank-at-eol,tab-in-indent +dune* whitespace=blank-at-eol,tab-in-indent +*.dune whitespace=blank-at-eol,tab-in-indent *.el whitespace=blank-at-eol,tab-in-indent +*.fake whitespace=blank-at-eol,tab-in-indent *.g whitespace=blank-at-eol,tab-in-indent *.h whitespace=blank-at-eol,tab-in-indent *.html whitespace=blank-at-eol,tab-in-indent @@ -32,12 +31,13 @@ tools/CoqMakefile.in whitespace=blank-at-eol *.md whitespace=blank-at-eol,tab-in-indent *.merlin whitespace=blank-at-eol,tab-in-indent *.ml whitespace=blank-at-eol,tab-in-indent -*.ml4 whitespace=blank-at-eol,tab-in-indent +*.mlg whitespace=blank-at-eol,tab-in-indent *.mli whitespace=blank-at-eol,tab-in-indent *.mll whitespace=blank-at-eol,tab-in-indent *.mllib whitespace=blank-at-eol,tab-in-indent *.mlp whitespace=blank-at-eol,tab-in-indent *.mlpack whitespace=blank-at-eol,tab-in-indent +*.nix whitespace=blank-at-eol,tab-in-indent *.nsh whitespace=blank-at-eol,tab-in-indent *.nsi whitespace=blank-at-eol,tab-in-indent *.py whitespace=blank-at-eol,tab-in-indent @@ -51,6 +51,14 @@ tools/CoqMakefile.in whitespace=blank-at-eol *.xml whitespace=blank-at-eol,tab-in-indent *.yml whitespace=blank-at-eol,tab-in-indent +.gitattributes whitespace=blank-at-eol,tab-in-indent +_CoqProject whitespace=blank-at-eol,tab-in-indent +Dockerfile whitespace=blank-at-eol,tab-in-indent + +# tabs are allowed in Makefiles. +Makefile* whitespace=blank-at-eol +tools/CoqMakefile.in whitespace=blank-at-eol + # CR is desired for these Windows files. *.bat whitespace=cr-at-eol,blank-at-eol,tab-in-indent diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index b3dc1fa896..a1da9be20b 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -154,7 +154,7 @@ after_script: - BIN=$(readlink -f ../_install_ci/bin)/ - LIB=$(readlink -f ../_install_ci/lib/coq)/ - export OCAMLPATH=$(readlink -f ../_install_ci/lib/):"$OCAMLPATH" - - make -j "$NJOBS" BIN="$BIN" LIB="$LIB" COQFLAGS="${COQFLAGS}" all + - make -j "$NJOBS" BIN="$BIN" COQLIB="$LIB" COQFLAGS="${COQFLAGS}" all artifacts: name: "$CI_JOB_NAME.logs" when: on_failure @@ -170,7 +170,7 @@ after_script: - cd _install_ci - find lib/coq/ -name '*.vo' -print0 > vofiles - for regexp in 's/.vo//' 's:lib/coq/plugins:Coq:' 's:lib/coq/theories:Coq:' 's:/:.:g'; do sed -z -i "$regexp" vofiles; done - - xargs -0 --arg-file=vofiles bin/coqchk -boot -silent -o -m -coqlib lib/coq/ + - xargs -0 --arg-file=vofiles bin/coqchk -silent -o -m -coqlib lib/coq/ .ci-template: &ci-template stage: test @@ -346,6 +346,16 @@ doc:refman:dune: paths: - _build/default/doc/sphinx_build/html +doc:stdlib:dune: + <<: *dune-ci-template + variables: + <<: *dune-ci-template-vars + DUNE_TARGET: stdlib-html + artifacts: + <<: *dune-ci-template-artifacts + paths: + - _build/default/doc/stdlib/html + doc:refman:deploy: stage: deploy environment: @@ -355,25 +365,29 @@ doc:refman:deploy: variables: - $DOCUMENTATION_DEPLOY_KEY dependencies: - - doc:refman + - doc:ml-api:odoc + - doc:refman:dune + - doc:stdlib:dune before_script: - which ssh-agent || ( apt-get update -y && apt-get install openssh-client -y ) - eval $(ssh-agent -s) - - echo "$DOCUMENTATION_DEPLOY_KEY" | tr -d '\r' | ssh-add - > /dev/null - mkdir -p ~/.ssh - chmod 700 ~/.ssh - ssh-keyscan -t rsa github.com >> ~/.ssh/known_hosts - git config --global user.name "coqbot" - git config --global user.email "coqbot@users.noreply.github.com" script: + - echo "$DOCUMENTATION_DEPLOY_KEY" | tr -d '\r' | ssh-add - > /dev/null - git clone git@github.com:coq/doc.git _deploy + - rm -rf _deploy/$CI_COMMIT_REF_NAME/api - rm -rf _deploy/$CI_COMMIT_REF_NAME/refman - rm -rf _deploy/$CI_COMMIT_REF_NAME/stdlib - mkdir -p _deploy/$CI_COMMIT_REF_NAME - - cp -rv _install_ci/share/doc/coq/sphinx/html _deploy/$CI_COMMIT_REF_NAME/refman - - cp -rv _install_ci/share/doc/coq/html/stdlib _deploy/$CI_COMMIT_REF_NAME/stdlib + - cp -rv _build/default/_doc/_html _deploy/$CI_COMMIT_REF_NAME/api + - cp -rv _build/default/doc/sphinx_build/html _deploy/$CI_COMMIT_REF_NAME/refman + - cp -rv _build/default/doc/stdlib/html _deploy/$CI_COMMIT_REF_NAME/stdlib - cd _deploy/$CI_COMMIT_REF_NAME/ - - git add refman stdlib + - git add api refman stdlib - git commit -m "Documentation of branch “$CI_COMMIT_REF_NAME” at $CI_COMMIT_SHORT_SHA" - git push # TODO: rebase and retry on failure diff --git a/CHANGES.md b/CHANGES.md index 38c197d8cc..af2b7991dd 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -116,7 +116,7 @@ Vernacular commands avoid conflicts with explicitly named binders. - Computation of implicit arguments now properly handles local definitions in the - binders for an `Instance`. + binders for an `Instance`, and can be mixed with implicit binders `{x : T}`. - `Declare Instance` now requires an instance name. @@ -135,6 +135,8 @@ Vernacular commands - The algorithm computing implicit arguments now behaves uniformly for primitive projection and application nodes (bug #9508). +- `Hypotheses` and `Variables` can now take implicit binders inside sections. + Tools - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values: diff --git a/Makefile.build b/Makefile.build index 8afb498a63..ea356d5f8e 100644 --- a/Makefile.build +++ b/Makefile.build @@ -201,7 +201,7 @@ COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR) $(COQUSERFLAGS) # Beware this depends on the makefile being in a particular dir, we # should pass an absolute path here but windows is tricky # c.f. https://github.com/coq/coq/pull/9560 -BOOTCOQC=$(TIMER) $(COQC) -coqlib . -boot $(COQOPTS) +BOOTCOQC=$(TIMER) $(COQC) -coqlib . -q $(COQOPTS) LOCALINCLUDES=$(addprefix -I ,$(SRCDIRS)) MLINCLUDES=$(LOCALINCLUDES) @@ -550,11 +550,11 @@ $(CSDPCERTBYTE): $(CSDPCERTCMO) .PHONY: validate check test-suite $(ALLSTDLIB).v -VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m +VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m -coqlib . validate: $(CHICKEN) | $(ALLVO:.$(VO)=.vo) $(SHOW)'COQCHK <theories & plugins>' - $(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS) + $(HIDE)$(CHICKEN) $(VALIDOPTS) $(ALLMODS) $(ALLSTDLIB).v: $(SHOW)'MAKE $(notdir $@)' @@ -828,7 +828,7 @@ theories/Init/%.vio: theories/Init/%.v $(VO_TOOLS_DEP) $(HIDE)$(BOOTCOQC) $< $(TIMING_ARG) $(TIMING_EXTRA) ifdef VALIDATE $(SHOW)'COQCHK $(call vo_to_mod,$@)' - $(HIDE)$(CHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \ + $(HIDE)$(CHICKEN) $(VALIDOPTS) -norec $(call vo_to_mod,$@) \ || ( RV=$$?; rm -f "$@"; exit $${RV} ) endif diff --git a/Makefile.dune b/Makefile.dune index e3a8a30bc2..da4c59af75 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -4,7 +4,8 @@ .PHONY: help voboot states world watch check # Main developer targets .PHONY: coq coqide coqide-server # Package targets .PHONY: quickbyte quickopt # Partial / quick developer targets -.PHONY: test-suite refman-html apidoc release # Accesory targets +.PHONY: refman-html stdlib-html apidoc # Documentation targets +.PHONY: test-suite release # Accesory targets .PHONY: ocheck trunk ireport clean # Maintenance targets # use DUNEOPT=--display=short for a more verbose build @@ -29,6 +30,7 @@ help: @echo "" @echo " - test-suite: run Coq's test suite" @echo " - refman-html: build Coq's reference manual [HTML version]" + @echo " - stdlib-html: build Coq's Stdlib documentation [HTML version]" @echo " - apidoc: build ML API documentation" @echo " - release: build Coq in release mode" @echo "" @@ -76,11 +78,14 @@ quickopt: voboot dune build $(DUNEOPT) $(QUICKOPT_TARGETS) test-suite: voboot - dune runtest $(DUNEOPT) + dune runtest --no-buffer $(DUNEOPT) refman-html: voboot dune build @refman-html +stdlib-html: voboot + dune build @stdlib-html + apidoc: voboot dune build $(DUNEOPT) @doc diff --git a/Makefile.ide b/Makefile.ide index 23ce83d263..db1cc3746d 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -70,7 +70,7 @@ SOURCEVIEWSHARE=$(shell pkg-config --variable=prefix gtksourceview-2.0)/share .PHONY: ide-toploop ide-byteloop ide-optloop # target to build CoqIde (native version) and the stuff needed to lauch it -coqide: coqide-files coqide-opt theories/Init/Prelude.$(VO) +coqide: coqide-files coqide-opt theories/Init/Prelude.$(VO) $(TOPBIN) # target to build CoqIde (in native and byte versions), and no more # NB: this target is used in the opam package coq-coqide diff --git a/checker/.depend b/checker/.depend deleted file mode 100644 index 09ab6bdd13..0000000000 --- a/checker/.depend +++ /dev/null @@ -1,58 +0,0 @@ -checker.cmo: type_errors.cmi term.cmo safe_typing.cmi indtypes.cmi \ - declarations.cmi check_stat.cmi check.cmo -checker.cmx: type_errors.cmx term.cmx safe_typing.cmx indtypes.cmx \ - declarations.cmx check_stat.cmx check.cmx -check.cmo: safe_typing.cmi -check.cmx: safe_typing.cmx -check_stat.cmo: term.cmo safe_typing.cmi indtypes.cmi environ.cmo \ - declarations.cmi check_stat.cmi -check_stat.cmx: term.cmx safe_typing.cmx indtypes.cmx environ.cmx \ - declarations.cmx check_stat.cmi -closure.cmo: term.cmo environ.cmo closure.cmi -closure.cmx: term.cmx environ.cmx closure.cmi -closure.cmi: term.cmo environ.cmo -declarations.cmo: term.cmo declarations.cmi -declarations.cmx: term.cmx declarations.cmi -declarations.cmi: term.cmo -environ.cmo: term.cmo declarations.cmi -environ.cmx: term.cmx declarations.cmx -indtypes.cmo: typeops.cmi term.cmo reduction.cmi inductive.cmi environ.cmo \ - declarations.cmi indtypes.cmi -indtypes.cmx: typeops.cmx term.cmx reduction.cmx inductive.cmx environ.cmx \ - declarations.cmx indtypes.cmi -indtypes.cmi: typeops.cmi term.cmo environ.cmo declarations.cmi -inductive.cmo: type_errors.cmi term.cmo reduction.cmi environ.cmo \ - declarations.cmi inductive.cmi -inductive.cmx: type_errors.cmx term.cmx reduction.cmx environ.cmx \ - declarations.cmx inductive.cmi -inductive.cmi: term.cmo environ.cmo declarations.cmi -main.cmo: checker.cmo -main.cmx: checker.cmx -mod_checking.cmo: typeops.cmi term.cmo subtyping.cmi reduction.cmi modops.cmi \ - inductive.cmi indtypes.cmi environ.cmo declarations.cmi -mod_checking.cmx: typeops.cmx term.cmx subtyping.cmx reduction.cmx modops.cmx \ - inductive.cmx indtypes.cmx environ.cmx declarations.cmx -modops.cmo: term.cmo environ.cmo declarations.cmi modops.cmi -modops.cmx: term.cmx environ.cmx declarations.cmx modops.cmi -modops.cmi: term.cmo environ.cmo declarations.cmi -reduction.cmo: term.cmo environ.cmo closure.cmi reduction.cmi -reduction.cmx: term.cmx environ.cmx closure.cmx reduction.cmi -reduction.cmi: term.cmo environ.cmo -safe_typing.cmo: validate.cmo modops.cmi mod_checking.cmo environ.cmo \ - declarations.cmi safe_typing.cmi -safe_typing.cmx: validate.cmx modops.cmx mod_checking.cmx environ.cmx \ - declarations.cmx safe_typing.cmi -safe_typing.cmi: term.cmo environ.cmo declarations.cmi -subtyping.cmo: typeops.cmi term.cmo reduction.cmi modops.cmi inductive.cmi \ - environ.cmo declarations.cmi subtyping.cmi -subtyping.cmx: typeops.cmx term.cmx reduction.cmx modops.cmx inductive.cmx \ - environ.cmx declarations.cmx subtyping.cmi -subtyping.cmi: term.cmo environ.cmo declarations.cmi -type_errors.cmo: term.cmo environ.cmo type_errors.cmi -type_errors.cmx: term.cmx environ.cmx type_errors.cmi -type_errors.cmi: term.cmo environ.cmo -typeops.cmo: type_errors.cmi term.cmo reduction.cmi inductive.cmi environ.cmo \ - declarations.cmi typeops.cmi -typeops.cmx: type_errors.cmx term.cmx reduction.cmx inductive.cmx environ.cmx \ - declarations.cmx typeops.cmi -typeops.cmi: term.cmo environ.cmo declarations.cmi diff --git a/checker/checker.ml b/checker/checker.ml index 3db7ccdcae..3c93ef7d36 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -189,9 +189,9 @@ let print_usage_channel co command = \n -admit module load module and dependencies without checking\ \n -norec module check module but admit dependencies without checking\ \n\ +\n -coqlib dir set coqchk's standard library location\ \n -where print coqchk's standard library location and exit\ \n -v print coqchk version and exit\ -\n -boot boot mode\ \n -o, --output-context print the list of assumptions\ \n -m, --memory print the maximum heap size\ \n -silent disable trace of constants being checked\ @@ -319,8 +319,6 @@ let explain_exn = function let deprecated flag = Feedback.msg_warning (str "Deprecated flag " ++ quote (str flag)) -let boot_opt = ref false - let parse_args argv = let rec parse = function | [] -> () @@ -357,7 +355,6 @@ let parse_args argv = | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () | ("-v"|"--version") :: _ -> version () - | "-boot" :: rem -> boot_opt := true; parse rem | ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem | ("-o" | "--output-context") :: rem -> Check_stat.output_context := true; parse rem diff --git a/dev/base_include b/dev/base_include index 48feeec147..b214959bad 100644 --- a/dev/base_include +++ b/dev/base_include @@ -1,24 +1,6 @@ - (* File to include to get some Coq facilities under the ocaml toplevel. This file is loaded by include *) -#cd".";; -#directory "parsing";; -#directory "interp";; -#directory "toplevel";; -#directory "library";; -#directory "kernel";; -#directory "gramlib";; -#directory "engine";; -#directory "pretyping";; -#directory "lib";; -#directory "proofs";; -#directory "tactics";; -#directory "printing";; -#directory "grammar";; -#directory "stm";; -#directory "vernac";; - #use "top_printers.ml";; #use "vm_printers.ml";; @@ -137,7 +119,6 @@ open Proof_global open Redexpr open Refiner open Tacmach -open Tactic_debug open Hints open Auto @@ -146,15 +127,9 @@ open Contradiction open Eauto open Elim open Equality -open Evar_tactics -open Extraargs -open Extratactics open Hipattern open Inv open Leminv -open Tacsubst -open Tacintern -open Tacinterp open Tacticals open Tactics open Eqschemes diff --git a/dev/ci/azure-build.sh b/dev/ci/azure-build.sh index c0030c566f..04c7d5db91 100755 --- a/dev/ci/azure-build.sh +++ b/dev/ci/azure-build.sh @@ -4,6 +4,4 @@ set -e -x cd $(dirname $0)/../.. -./configure -local -make -j 2 byte -make -j 2 world +make -f Makefile.dune coq coqide-server diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh index 8a1e36659c..9448a03f4f 100755 --- a/dev/ci/azure-opam.sh +++ b/dev/ci/azure-opam.sh @@ -10,4 +10,4 @@ bash opam64/install.sh opam init default -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $OPAM_VARIANT --disable-sandboxing eval "$(opam env)" -opam install -y num ocamlfind ounit +opam install -y num ocamlfind dune ounit diff --git a/dev/ci/azure-test.sh b/dev/ci/azure-test.sh index 8813245e5a..80a3d2e083 100755 --- a/dev/ci/azure-test.sh +++ b/dev/ci/azure-test.sh @@ -4,6 +4,5 @@ set -e -x #NB: if we make test-suite from the main makefile we get environment #too large for exec error -cd $(dirname $0)/../../test-suite -make -j 2 clean -make -j 2 PRINT_LOGS=1 +cd $(dirname $0)/../../ +make -f Makefile.dune test-suite diff --git a/dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh b/dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh new file mode 100644 index 0000000000..27ce9aca16 --- /dev/null +++ b/dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh @@ -0,0 +1,12 @@ +if [ "$CI_PULL_REQUEST" = "9567" ] || [ "$CI_BRANCH" = "hooks_unify" ]; then + + equations_CI_REF=hooks_unify + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + mtac2_CI_REF=hooks_unify + mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 + + paramcoq_CI_REF=hooks_unify + paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq + +fi diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 01c32041d2..da91c85856 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -106,6 +106,16 @@ refined, so you need to build enough of Coq once to use this target [it will then correctly compute the deps and rebuild if you call the script again] This will be fixed in the future. +## Dropping from coqtop: + +The following sequence is recommended: +``` +dune exec coqtop.byte +> Drop. +# #directory "dev";; +# #use "include_dune";; +``` + ## Compositionality, developer and release modes. By default [in "developer mode"], Dune will compose all the packages diff --git a/dev/inc_ltac b/dev/inc_ltac new file mode 100644 index 0000000000..8ef02445c2 --- /dev/null +++ b/dev/inc_ltac @@ -0,0 +1,7 @@ +open Evar_tactics +open Tactic_debug +open Tacsubst +open Tacintern +open Tacinterp +open Extraargs +open Extratactics diff --git a/dev/inc_ltac_dune b/dev/inc_ltac_dune new file mode 100644 index 0000000000..d7f505e8e0 --- /dev/null +++ b/dev/inc_ltac_dune @@ -0,0 +1,7 @@ +open Ltac_plugin__Evar_tactics +open Ltac_plugin__Tactic_debug +open Ltac_plugin__Tacsubst +open Ltac_plugin__Tacintern +open Ltac_plugin__Tacinterp +open Ltac_plugin__Extraargs +open Ltac_plugin__Extratactics diff --git a/dev/incdir b/dev/incdir new file mode 100644 index 0000000000..8ffd6bf6dc --- /dev/null +++ b/dev/incdir @@ -0,0 +1,16 @@ +#cd".";; +#directory "parsing";; +#directory "interp";; +#directory "toplevel";; +#directory "library";; +#directory "kernel";; +#directory "gramlib";; +#directory "engine";; +#directory "pretyping";; +#directory "lib";; +#directory "proofs";; +#directory "tactics";; +#directory "printing";; +#directory "grammar";; +#directory "stm";; +#directory "vernac";; diff --git a/dev/incdir_dune b/dev/incdir_dune new file mode 100644 index 0000000000..9d0fee1fa2 --- /dev/null +++ b/dev/incdir_dune @@ -0,0 +1,16 @@ +#cd".";; +#directory "_build/default/lib/.lib.objs/";; +#directory "_build/default/clib/.clib.objs/";; +#directory "_build/default/kernel/.kernel.objs/";; +#directory "_build/default/library/.library.objs/";; +#directory "_build/default/engine/.engine.objs/";; +#directory "_build/default/pretyping/.pretyping.objs/";; +#directory "_build/default/interp/.interp.objs/";; +#directory "_build/default/parsing/.parsing.objs/";; +#directory "_build/default/gramlib/.gramlib.objs/";; +#directory "_build/default/proofs/.proofs.objs/";; +#directory "_build/default/tactics/.tactics.objs/";; +#directory "_build/default/printing/.printing.objs/";; +#directory "_build/default/vernac/.vernac.objs/";; +#directory "_build/default/stm/.stm.objs/";; +#directory "_build/default/toplevel/.toplevel.objs/";; diff --git a/dev/include b/dev/include index c5de83b900..fa4bf827d7 100644 --- a/dev/include +++ b/dev/include @@ -1,4 +1,3 @@ - (* File to include to install the pretty-printers in the ocaml toplevel *) (* Typical usage : @@ -15,69 +14,8 @@ then ignore (Toploop.use_silently Format.std_formatter "dev/include") *) -(* For OCaml 3.10.x: - clflags.cmi (a ocaml compilation by-product) must be in the library path. - On Debian, install ocaml-compiler-libs, and uncomment the following: - #directory "+compiler-libs/utils";; - Clflags.recursive_types := true;; -*) - #cd ".";; +#use "incdir";; #use "base_include";; - -#install_printer (* pp_stdcmds *) pp;; - -#install_printer (* pattern *) pppattern;; -#install_printer (* glob_constr *) ppglob_constr;; -#install_printer (* open constr *) ppopenconstr;; -#install_printer (* constr *) ppconstr;; -#install_printer (* econstr *) ppeconstr;; -#install_printer (* constr_substituted *) ppsconstr;; -#install_printer (* constraints *) ppconstraints;; -#install_printer (* univ constraints *) ppuniverseconstraints;; -#install_printer (* universe *) ppuni;; -#install_printer (* universes *) ppuniverses;; -#install_printer (* univ level *) ppuni_level;; -#install_printer (* univ context *) ppuniverse_context;; -#install_printer (* univ context future *) ppuniverse_context_future;; -#install_printer (* univ context set *) ppuniverse_context_set;; -#install_printer (* univ set *) ppuniverse_set;; -#install_printer (* univ instance *) ppuniverse_instance;; -#install_printer (* univ subst *) ppuniverse_subst;; -#install_printer (* univ full subst *) ppuniverse_level_subst;; -#install_printer (* univ opt subst *) ppuniverse_opt_subst;; -#install_printer (* evar univ ctx *) ppevar_universe_context;; -#install_printer (* inductive *) ppind;; -#install_printer (* 'a scheme_kind *) ppscheme;; -#install_printer (* type_judgement *) pptype;; -#install_printer (* judgement *) ppj;; -#install_printer (* id set *) ppidset;; -#install_printer (* int set *) ppintset;; - -#install_printer (* Reductionops stcak of unfolded constants *) pp_cst_stack_t;; -#install_printer (* Reductionops machine stack *) pp_stack_t;; - -(*#install_printer (* hint_db *) print_hint_db;;*) -(*#install_printer (* hints_path *) pphintspath;;*) -#install_printer (* goal *) ppgoal;; -(*#install_printer (* sigma goal *) ppsigmagoal;;*) -#install_printer (* proof *) pproof;; -#install_printer (* Goal.goal *) ppgoalgoal;; -#install_printer (* proofview *) ppproofview;; -#install_printer (* metaset.t *) ppmetas;; -#install_printer (* evar *) ppevar;; -#install_printer (* evar_map *) ppevm;; -#install_printer (* Evar.Set.t *) ppexistentialset;; -#install_printer (* clenv *) ppclenv;; -#install_printer (* env *) ppenv;; -#install_printer (* Hint_db.t *) pphintdb;; -#install_printer (* named_context_val *) ppnamedcontextval;; - -#install_printer (* tactic *) pptac;; -#install_printer (* object *) ppobj;; -#install_printer (* global_reference *) ppglobal;; -#install_printer (* generic_argument *) pp_generic_argument;; - -#install_printer (* fconstr *) ppfconstr;; - -#install_printer (* Future.computation *) ppfuture;; +#use "inc_ltac";; +#use "include_printers";; diff --git a/dev/include_dune b/dev/include_dune new file mode 100644 index 0000000000..2ef8eb4d04 --- /dev/null +++ b/dev/include_dune @@ -0,0 +1,22 @@ +(* File to include to install the pretty-printers in the ocaml toplevel *) + +(* Typical usage : + + $ dune exec coqtop.byte # or even better : rlwrap coqtop.byte + Coq < Drop. + # #directory "dev";; + # #use "include";; + + Alternatively, you can avoid typing #use "include" after each Drop + by adding the following lines in your $HOME/.ocamlinit : + + #directory "+compiler-libs";; + if Filename.basename Sys.argv.(0) = "coqtop.byte" + then ignore (Toploop.use_silently Format.std_formatter "dev/include") +*) + +#cd ".";; +#use "incdir_dune";; +#use "base_include";; +#use "inc_ltac_dune";; +#use "include_printers";; diff --git a/dev/include_printers b/dev/include_printers new file mode 100644 index 0000000000..90088e40bf --- /dev/null +++ b/dev/include_printers @@ -0,0 +1,55 @@ +#install_printer (* pp_stdcmds *) pp;; +#install_printer (* pattern *) pppattern;; +#install_printer (* glob_constr *) ppglob_constr;; +#install_printer (* open constr *) ppopenconstr;; +#install_printer (* constr *) ppconstr;; +#install_printer (* econstr *) ppeconstr;; +#install_printer (* constr_substituted *) ppsconstr;; +#install_printer (* constraints *) ppconstraints;; +#install_printer (* univ constraints *) ppuniverseconstraints;; +#install_printer (* universe *) ppuni;; +#install_printer (* universes *) ppuniverses;; +#install_printer (* univ level *) ppuni_level;; +#install_printer (* univ context *) ppuniverse_context;; +#install_printer (* univ context future *) ppuniverse_context_future;; +#install_printer (* univ context set *) ppuniverse_context_set;; +#install_printer (* univ set *) ppuniverse_set;; +#install_printer (* univ instance *) ppuniverse_instance;; +#install_printer (* univ subst *) ppuniverse_subst;; +#install_printer (* univ full subst *) ppuniverse_level_subst;; +#install_printer (* univ opt subst *) ppuniverse_opt_subst;; +#install_printer (* evar univ ctx *) ppevar_universe_context;; +#install_printer (* inductive *) ppind;; +#install_printer (* 'a scheme_kind *) ppscheme;; +#install_printer (* type_judgement *) pptype;; +#install_printer (* judgement *) ppj;; +#install_printer (* id set *) ppidset;; +#install_printer (* int set *) ppintset;; + +#install_printer (* Reductionops stcak of unfolded constants *) pp_cst_stack_t;; +#install_printer (* Reductionops machine stack *) pp_stack_t;; + +(*#install_printer (* hint_db *) print_hint_db;;*) +(*#install_printer (* hints_path *) pphintspath;;*) +#install_printer (* goal *) ppgoal;; +(*#install_printer (* sigma goal *) ppsigmagoal;;*) +#install_printer (* proof *) pproof;; +#install_printer (* Goal.goal *) ppgoalgoal;; +#install_printer (* proofview *) ppproofview;; +#install_printer (* metaset.t *) ppmetas;; +#install_printer (* evar *) ppevar;; +#install_printer (* evar_map *) ppevm;; +#install_printer (* Evar.Set.t *) ppexistentialset;; +#install_printer (* clenv *) ppclenv;; +#install_printer (* env *) ppenv;; +#install_printer (* Hint_db.t *) pphintdb;; +#install_printer (* named_context_val *) ppnamedcontextval;; + +#install_printer (* tactic *) pptac;; +#install_printer (* object *) ppobj;; +#install_printer (* global_reference *) ppglobal;; +#install_printer (* generic_argument *) pp_generic_argument;; + +#install_printer (* fconstr *) ppfconstr;; + +#install_printer (* Future.computation *) ppfuture;; diff --git a/dev/tools/create_overlays.sh b/dev/tools/create_overlays.sh index 41392be5d7..ad60b1115f 100755 --- a/dev/tools/create_overlays.sh +++ b/dev/tools/create_overlays.sh @@ -42,7 +42,7 @@ OVERLAY_BRANCH=$(git rev-parse --abbrev-ref HEAD) OVERLAY_FILE=$(mktemp overlay-XXXX) # Create the overlay file -printf 'if [ "$CI_PULL_REQUEST" = "%s" ] || [ "$CI_BRANCH" = "%s" ]; then \n\n' "$PR_NUMBER" "$OVERLAY_BRANCH" > "$OVERLAY_FILE" +printf 'if [ "$CI_PULL_REQUEST" = "%s" ] || [ "$CI_BRANCH" = "%s" ]; then\n\n' "$PR_NUMBER" "$OVERLAY_BRANCH" > "$OVERLAY_FILE" # We first try to build the contribs while test $# -gt 0 diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 813ad71be9..425f21de70 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -12,7 +12,8 @@ OFFICIAL_REMOTE_HTTPS_URL="github.com/coq/coq" # Set SLOW_CONF to have the confirmation output wait for a newline # E.g. call $ SLOW_CONF= dev/tools/merge-pr.sh /PR number/ -if [ -z ${SLOW_CONF+x} ]; then +# emacs doesn't send characters until the RET so we can't quick_conf +if [ -z ${SLOW_CONF+x} ] || [ -n "$INSIDE_EMACS" ]; then QUICK_CONF="-n 1" else QUICK_CONF="" diff --git a/doc/common/styles/html/coqremote/header.html b/doc/common/styles/html/coqremote/header.html index c6c4509133..2f7ba14753 100644 --- a/doc/common/styles/html/coqremote/header.html +++ b/doc/common/styles/html/coqremote/header.html @@ -4,12 +4,12 @@ <head> <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> <link rel="shortcut icon" href="/favicon.ico" type="image/x-icon" /> -<link type="text/css" rel="stylesheet" media="all" href="/modules/node/node.css" /> -<link type="text/css" rel="stylesheet" media="all" href="/modules/system/defaults.css" /> -<link type="text/css" rel="stylesheet" media="all" href="/modules/system/system.css" /> -<link type="text/css" rel="stylesheet" media="all" href="/modules/user/user.css" /> -<link type="text/css" rel="stylesheet" media="all" href="/sites/all/themes/coq/style.css" /> -<link type="text/css" rel="stylesheet" media="all" href="/sites/all/themes/coq/coqdoc.css" /> +<link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/node/node.css" /> +<link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/system/defaults.css" /> +<link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/system/system.css" /> +<link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/user/user.css" /> +<link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/sites/all/themes/coq/style.css" /> +<link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/sites/all/themes/coq/coqdoc.css" /> <title>Standard Library | The Coq Proof Assistant</title> @@ -21,20 +21,20 @@ <div id="headertop"> <div id="nav"> <ul class="links-menu"> - <li><a href="/" class="active">Home</a></li> - <li><a href="/about-coq" title="More about coq">About Coq</a></li> - <li><a href="/download">Get Coq</a></li> - <li><a href="/documentation">Documentation</a></li> - <li><a href="/community">Community</a></li> + <li><a href="//coq.inria.fr/" class="active">Home</a></li> + <li><a href="//coq.inria.fr/about-coq" title="More about coq">About Coq</a></li> + <li><a href="//coq.inria.fr/download">Get Coq</a></li> + <li><a href="//coq.inria.fr/documentation">Documentation</a></li> + <li><a href="//coq.inria.fr/community">Community</a></li> </ul> </div> </div> <div id="header"> <div id="logoWrapper"> - <div id="logo"><a href="/" title="Home"><img src="/files/barron_logo.png" alt="Home" /></a> + <div id="logo"><a href="//coq.inria.fr/" title="Home"><img src="//coq.inria.fr/files/barron_logo.png" alt="Home" /></a> </div> - <div id="siteName"><a href="/" title="Home">The Coq Proof Assistant</a> + <div id="siteName"><a href="//coq.inria.fr/" title="Home">The Coq Proof Assistant</a> </div> </div> </div> diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index 9d10a8ba72..e370d37fc4 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -1,5 +1,5 @@ (* Ideally coq/coq#8811 would get merged and then this function could be much simpler. *) -let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook = +let edeclare ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps = let sigma = Evd.minimize_universes sigma in let body = EConstr.to_constr sigma body in let tyopt = Option.map (EConstr.to_constr sigma) tyopt in @@ -9,16 +9,17 @@ let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook = (Option.List.cons tyopt [body]) in let sigma = Evd.restrict_universe_context sigma uvars in let univs = Evd.check_univ_decl ~poly sigma udecl in + let uctx = Evd.evar_universe_context sigma in let ubinders = Evd.universe_binders sigma in let ce = Declare.definition_entry ?types:tyopt ~univs body in - DeclareDef.declare_definition ident k ce ubinders imps ~hook + let hook_data = Option.map (fun hook -> hook, uctx, []) hook in + DeclareDef.declare_definition ident k ce ubinders imps ?hook_data let packed_declare_definition ~poly ident value_with_constraints = let body, ctx = value_with_constraints in let sigma = Evd.from_ctx ctx in let k = (Decl_kinds.Global, poly, Decl_kinds.Definition) in let udecl = UState.default_univ_decl in - let nohook = Lemmas.mk_hook (fun _ x -> ()) in - ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook) + ignore (edeclare ident k ~opaque:false sigma udecl body None []) (* But this definition cannot be undone by Reset ident *) diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 25f983ac1e..f1733a5ebf 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2260,3 +2260,52 @@ expression as described in :ref:`ltac`. This construction is useful when one wants to define complicated terms using highly automated tactics without resorting to writing the proof-term by means of the interactive proof engine. + +.. _primitive-integers: + +Primitive Integers +-------------------------------- + +The language of terms features 63-bit machine integers as values. The type of +such a value is *axiomatized*; it is declared through the following sentence +(excerpt from the :g:`Int63` module): + +.. coqdoc:: + + Primitive int := #int63_type. + +This type is equipped with a few operators, that must be similarly declared. +For instance, equality of two primitive integers can be decided using the :g:`Int63.eqb` function, +declared and specified as follows: + +.. coqdoc:: + + Primitive eqb := #int63_eq. + Notation "m '==' n" := (eqb m n) (at level 70, no associativity) : int63_scope. + + Axiom eqb_correct : forall i j, (i == j)%int63 = true -> i = j. + +The complete set of such operators can be obtained looking at the :g:`Int63` module. + +These primitive declarations are regular axioms. As such, they must be trusted and are listed by the +:g:`Print Assumptions` command, as in the following example. + +.. coqtop:: in reset + + From Coq Require Import Int63. + Lemma one_minus_one_is_zero : (1 - 1 = 0)%int63. + Proof. apply eqb_correct; vm_compute; reflexivity. Qed. + +.. coqtop:: all + + Print Assumptions one_minus_one_is_zero. + +The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement +dedicated, efficient, rules to reduce the applications of these primitive +operations. + +These primitives, when extracted to OCaml (see :ref:`extraction`), are mapped to +types and functions of a :g:`Uint63` module. Said module is not produced by +extraction. Instead, it has to be provided by the user (if they want to compile +or execute the extracted code). For instance, an implementation of this module +can be taken from the kernel of Coq. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 237b534d67..b81830f06b 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -2094,9 +2094,9 @@ into a closing one (similar to :tacn:`now`). Its general syntax is: :name: by :undocumented: -The Ltac expression :n:`by [@tactic | [@tactic | …]` is equivalent to -:n:`[by @tactic | by @tactic | ...]` and this form should be preferred -to the former. +The Ltac expression :n:`by [@tactic | @tactic | …]` is equivalent to +:n:`do [done | by @tactic | by @tactic | …]`, which corresponds to the +standard Ltac expression :n:`first [done | @tactic; done | @tactic; done | …]`. In the script provided as example in section :ref:`indentation_ssr`, the paragraph corresponding to each sub-case ends with a tactic line prefixed diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index a98a46ba21..3e8dd25ee0 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1213,10 +1213,19 @@ Controlling the locality of commands occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this category. +.. _internal-registration-commands: + +Internal registration commands +-------------------------------- + +Due to their internal nature, the commands that are presented in this section +are not for general use. They are meant to appear only in standard libraries and +in support libraries of plug-ins. + .. _exposing-constants-to-ocaml-libraries: Exposing constants to OCaml libraries ----------------------------------------------------------------- +```````````````````````````````````````````````````````````````` .. cmd:: Register @qualid__1 as @qualid__2 @@ -1225,5 +1234,35 @@ Exposing constants to OCaml libraries calling :n:`Coqlib.lib_ref "@qualid__2"`; i.e., there is no need to known where is the constant defined (file, module, library, etc.). - Due to its internal nature, this command is not for general use. It is meant - to appear only in standard libraries and in support libraries of plug-ins. + As a special case, when the first segment of :n:`@qualid__2` is :g:`kernel`, + the constant is exposed to the kernel. For instance, the `Int63` module + features the following declaration: + + .. coqdoc:: + + Register bool as kernel.ind_bool. + + This makes the kernel aware of what is the type of boolean values. This + information is used for instance to define the return type of the + :g:`#int63_eq` primitive. + + .. seealso:: :ref:`primitive-integers` + +Inlining hints for the fast reduction machines +```````````````````````````````````````````````````````````````` + +.. cmd:: Register Inline @qualid + + This command gives as a hint to the reduction machines (VM and native) that + the body of the constant :n:`@qualid` should be inlined in the generated code. + +Registering primitive operations +```````````````````````````````` + +.. cmd:: Primitive @ident__1 := #@ident__2. + + Declares :n:`@ident__1` as the primitive operator :n:`#@ident__2`. When + running this command, the type of the primitive should be already known by + the kernel (this is achieved through this command for primitive types and + through the :cmd:`Register` command with the :g:`kernel` name-space for other + types). diff --git a/doc/stdlib/dune b/doc/stdlib/dune new file mode 100644 index 0000000000..7fe2493fbf --- /dev/null +++ b/doc/stdlib/dune @@ -0,0 +1,36 @@ +; This is an ad-hoc rule to ease the migration, it should be handled +; natively by Dune in the future. +(rule + (targets index-list.html) + (deps + make-library-index index-list.html.template hidden-files + (source_tree %{project_root}/theories) + (source_tree %{project_root}/plugins)) + (action + (chdir %{project_root} + ; On windows run will fail + (bash "doc/stdlib/make-library-index doc/stdlib/index-list.html doc/stdlib/hidden-files")))) + +(rule + (targets html) + (deps + ; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg + (source_tree %{project_root}/theories) + (source_tree %{project_root}/plugins) + (:header %{project_root}/doc/common/styles/html/coqremote/header.html) + (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html) + ; For .glob files, should be gone when Coq Dune is smarter. + (package coq)) + (action + (progn + (run mkdir -p html) + (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -R %{project_root}/plugins Coq $(find %{project_root}/theories %{project_root}/plugins -name *.v)") + (run mv html/index.html html/genindex.html) + (with-stdout-to + _index.html + (progn (cat %{header}) (cat index-list.html) (cat %{footer}))) + (run cp _index.html html/index.html)))) + +(alias + (name stdlib-html) + (deps html)) diff --git a/engine/namegen.ml b/engine/namegen.ml index 294b61fd3d..7ef4108c22 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -329,7 +329,7 @@ let next_name_away_in_goal na avoid = let next_global_ident_away id avoid = let id = if Id.Set.mem id avoid then restart_subscript id else id in - let bad id = Id.Set.mem id avoid || is_global id in + let bad id = Id.Set.mem id avoid || Global.exists_objlabel (Label.of_id id) in next_ident_away_from id bad (* 4- Looks for next fresh name outside a list; if name already used, diff --git a/ide/coq.ml b/ide/coq.ml index 91cd448eda..e7eea4ced2 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -119,7 +119,7 @@ let rec filter_coq_opts args = and asks_for_coqtop args = let pb_mes = GWindow.message_dialog - ~message:"Failed to load coqtop. Reset the preference to default ?" + ~message:"Failed to load coqidetop. Reset the preference to default ?" ~message_type:`QUESTION ~buttons:GWindow.Buttons.yes_no () in match pb_mes#run () with | `YES -> @@ -130,7 +130,7 @@ and asks_for_coqtop args = | `DELETE_EVENT | `NO -> let () = pb_mes#destroy () in let cmd_sel = GWindow.file_selection - ~title:"Coqtop to execute (edit your preference then)" + ~title:"coqidetop to execute (edit your preference then)" ~filename:(coqtop_path ()) ~urgency_hint:true () in match cmd_sel#run () with | `OK -> @@ -419,7 +419,7 @@ let rec respawn_coqtop ?(why=Unexpected) coqtop = let title = "Warning" in let icon = (warn_image ())#coerce in let buttons = ["Reset"; "Save all and quit"; "Quit without saving"] in - let ans = GToolbox.question_box ~title ~buttons ~icon "Coqtop died badly." in + let ans = GToolbox.question_box ~title ~buttons ~icon "coqidetop died badly." in if ans = 2 then (!save_all (); GtkMain.Main.quit ()) else if ans = 3 then GtkMain.Main.quit () | Planned -> () diff --git a/ide/coqide.ml b/ide/coqide.ml index 48c08899e0..94778e0c60 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1182,10 +1182,10 @@ let build_ui () = item "Help" ~label:"_Help"; item "Browse Coq Manual" ~label:"Browse Coq _Manual" ~callback:(fun _ -> - browse notebook#current_term.messages#default_route#add_string (doc_url ())); + browse notebook#current_term.messages#default_route#add_string Coq_config.wwwrefman); item "Browse Coq Library" ~label:"Browse Coq _Library" ~callback:(fun _ -> - browse notebook#current_term.messages#default_route#add_string library_url#get); + browse notebook#current_term.messages#default_route#add_string Coq_config.wwwstdlib); item "Help for keyword" ~label:"Help for _keyword" ~stock:`HELP ~callback:(fun _ -> on_current_term (fun sn -> browse_keyword sn.messages#default_route#add_string (get_current_word sn))); diff --git a/ide/ideutils.ml b/ide/ideutils.ml index c14af7d21d..5beaba3604 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -458,15 +458,6 @@ let browse prerr url = in run_command (fun _ -> ()) finally com -let doc_url () = - if doc_url#get = use_default_doc_url || doc_url#get = "" - then - let addr = List.fold_left Filename.concat (Envars.docdir ()) - ["html";"refman";"index.html"] - in - if Sys.file_exists addr then "file://"^addr else Coq_config.wwwrefman - else doc_url#get - let url_for_keyword = let ht = Hashtbl.create 97 in lazy ( @@ -476,13 +467,7 @@ let url_for_keyword = (fun x -> Sys.file_exists (Filename.concat x "index_urls.txt")) (Minilib.coqide_data_dirs ())) "index_urls.txt" in open_in index_urls - with Not_found -> - let doc_url = doc_url () in - let n = String.length doc_url in - if n > 8 && String.sub doc_url 0 7 = "file://" then - open_in (String.sub doc_url 7 (n-7) ^ "index_urls.txt") - else - raise Exit + with Not_found -> raise Exit in try while true do let s = input_line cin in @@ -503,7 +488,7 @@ let url_for_keyword = let browse_keyword prerr text = try let u = Lazy.force url_for_keyword text in - browse prerr (doc_url() ^ u) + browse prerr (Coq_config.wwwrefman ^ u) with Not_found -> prerr ("No documentation found for \""^text^"\".\n") let rec is_valid (s : Pp.t) = match Pp.repr s with diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 0031c59c17..531c71cd4b 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -13,7 +13,6 @@ val warning : string -> unit val cb : GData.clipboard -val doc_url : unit -> string val browse : (string -> unit) -> string -> unit val browse_keyword : (string -> unit) -> string -> unit diff --git a/ide/preferences.ml b/ide/preferences.ml index 4aa8c92f73..fb0eea1405 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -366,33 +366,6 @@ let text_font = in new preference ~name:["text_font"] ~init ~repr:Repr.(string) -let is_standard_doc_url url = - let wwwcompatprefix = "http://www.lix.polytechnique.fr/coq/" in - let n = String.length Coq_config.wwwcoq in - let n' = String.length Coq_config.wwwrefman in - url = Coq_config.localwwwrefman || - url = Coq_config.wwwrefman || - url = wwwcompatprefix ^ String.sub Coq_config.wwwrefman n (n'-n) - -let doc_url = -object - inherit [string] preference - ~name:["doc_url"] ~init:Coq_config.wwwrefman ~repr:Repr.(string) - as super - - method! set v = - if not (is_standard_doc_url v) && - v <> use_default_doc_url && - (* Extra hack to support links to last released doc version *) - v <> Coq_config.wwwcoq ^ "doc" && - v <> Coq_config.wwwcoq ^ "doc/" - then super#set v - -end - -let library_url = - new preference ~name:["library_url"] ~init:Coq_config.wwwstdlib ~repr:Repr.(string) - let show_toolbar = new preference ~name:["show_toolbar"] ~init:true ~repr:Repr.(bool) @@ -692,7 +665,7 @@ let configure ?(apply=(fun () -> ())) parent = let cmd_coqtop = string ~f:(fun s -> cmd_coqtop#set (if s = "AUTO" then None else Some s)) - " coqtop" (match cmd_coqtop#get with |None -> "AUTO" | Some x -> x) in + " coqidetop" (match cmd_coqtop#get with |None -> "AUTO" | Some x -> x) in let cmd_coqc = pstring " coqc" cmd_coqc in let cmd_make = pstring " make" cmd_make in let cmd_coqmakefile = pstring "coqmakefile" cmd_coqmakefile in @@ -948,32 +921,6 @@ let configure ?(apply=(fun () -> ())) parent = else cmd_browse#get]) cmd_browse#get in - let doc_url = - let predefined = [ - "file://"^(List.fold_left Filename.concat (Envars.docdir ()) ["refman";"html"]); - Coq_config.wwwrefman; - use_default_doc_url - ] in - combo - "Manual URL" - ~f:doc_url#set - ~new_allowed: true - (predefined@[if List.mem doc_url#get predefined then "" - else doc_url#get]) - doc_url#get in - let library_url = - let predefined = [ - "file://"^(List.fold_left Filename.concat (Envars.docdir ()) ["stdlib";"html"]); - Coq_config.wwwstdlib - ] in - combo - "Library URL" - ~f:(fun s -> library_url#set s) - ~new_allowed: true - (predefined@[if List.mem library_url#get predefined then "" - else library_url#get]) - library_url#get - in let automatic_tactics = strings ~f:automatic_tactics#set @@ -1039,7 +986,7 @@ let configure ?(apply=(fun () -> ())) parent = Section("Appearance", Some `PREFERENCES, [window_width; window_height]); Section("Externals", None, [cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; - cmd_print;cmd_editor;cmd_browse;doc_url;library_url]); + cmd_print;cmd_editor;cmd_browse]); Section("Tactics Wizard", None, [automatic_tactics]); Section("Shortcuts", Some `PREFERENCES, diff --git a/ide/preferences.mli b/ide/preferences.mli index 7ed6a40bdb..cf2265781c 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -74,8 +74,6 @@ val modifiers_valid : string preference val cmd_browse : string preference val cmd_editor : string preference val text_font : string preference -val doc_url : string preference -val library_url : string preference val show_toolbar : bool preference val contextual_menus_on_goal : bool preference val window_width : int preference diff --git a/interp/declare.ml b/interp/declare.ml index 175f9c66df..4371b15c82 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -430,9 +430,6 @@ let assumption_message id = discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *) Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared") -let register_message id = - Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is registered") - (** Monomorphic universes need to survive sections. *) let input_universe_context : Univ.ContextSet.t -> Libobject.obj = diff --git a/interp/declare.mli b/interp/declare.mli index 6f53d6872b..8f1e73c88c 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -74,7 +74,6 @@ val declare_mind : mutual_inductive_entry -> Libobject.object_name * bool val definition_message : Id.t -> unit val assumption_message : Id.t -> unit -val register_message : Id.t -> unit val fixpoint_message : int array option -> Id.t list -> unit val cofixpoint_message : Id.t list -> unit val recursive_message : bool (** true = fixpoint *) -> diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index dc15d9d25e..a05f7b9b04 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1194,39 +1194,46 @@ let register_inline kn senv = let cb = {cb with const_inline_code = true} in let env = add_constant kn cb env in { senv with env} -let check_register_ind (mind,i) r env = - let mb = Environ.lookup_mind mind env in - let check_if b s = +let check_register_ind ind r env = + let (mb,ob as spec) = Inductive.lookup_mind_specif env ind in + let check_if b msg = if not b then - CErrors.user_err ~hdr:"check_register_ind" (Pp.str s) in - check_if (Int.equal (Array.length mb.mind_packets) 1) "A non mutual inductive is expected"; - let ob = mb.mind_packets.(i) in + CErrors.user_err ~hdr:"check_register_ind" msg in + check_if (Int.equal (Array.length mb.mind_packets) 1) Pp.(str "A non mutual inductive is expected"); + let is_monomorphic = function Monomorphic _ -> true | Polymorphic _ -> false in + check_if (is_monomorphic mb.mind_universes) Pp.(str "A universe monomorphic inductive type is expected"); + check_if (not @@ Inductive.is_private spec) Pp.(str "A non-private inductive type is expected"); + let check_nparams n = + check_if (Int.equal mb.mind_nparams n) Pp.(str "An inductive type with " ++ int n ++ str " parameters is expected") + in let check_nconstr n = check_if (Int.equal (Array.length ob.mind_consnames) n) - ("an inductive type with "^(string_of_int n)^" constructors is expected") + Pp.(str "an inductive type with " ++ int n ++ str " constructors is expected") in let check_name pos s = check_if (Id.equal ob.mind_consnames.(pos) (Id.of_string s)) - ("the "^(string_of_int (pos + 1))^ - "th constructor does not have the expected name: " ^ s) in + Pp.(str"the " ++ int (pos + 1) ++ str + "th constructor does not have the expected name: " ++ str s) in let check_type pos t = check_if (Constr.equal t ob.mind_user_lc.(pos)) - ("the "^(string_of_int (pos + 1))^ + Pp.(str"the " ++ int (pos + 1) ++ str "th constructor does not have the expected type") in let check_type_cte pos = check_type pos (Constr.mkRel 1) in match r with | CPrimitives.PIT_bool -> + check_nparams 0; check_nconstr 2; check_name 0 "true"; check_type_cte 0; check_name 1 "false"; check_type_cte 1 | CPrimitives.PIT_carry -> + check_nparams 1; check_nconstr 2; let test_type pos = let c = ob.mind_user_lc.(pos) in - let s = "the "^(string_of_int (pos + 1))^ - "th constructor does not have the expected type" in + let s = Pp.(str"the " ++ int (pos + 1) ++ str + "th constructor does not have the expected type") in check_if (Constr.isProd c) s; let (_,d,cd) = Constr.destProd c in check_if (Constr.is_Type d) s; @@ -1240,11 +1247,11 @@ let check_register_ind (mind,i) r env = check_name 1 "C1"; test_type 1; | CPrimitives.PIT_pair -> + check_nparams 2; check_nconstr 1; check_name 0 "pair"; let c = ob.mind_user_lc.(0) in - let s = "the "^(string_of_int 1)^ - "th constructor does not have the expected type" in + let s = Pp.str "the constructor does not have the expected type" in begin match Term.decompose_prod c with | ([_,b;_,a;_,_B;_,_A], codom) -> check_if (is_Type _A) s; @@ -1255,6 +1262,7 @@ let check_register_ind (mind,i) r env = | _ -> check_if false s end | CPrimitives.PIT_cmp -> + check_nparams 0; check_nconstr 3; check_name 0 "Eq"; check_type_cte 0; diff --git a/man/coqide.1 b/man/coqide.1 index 3592f6e4e3..62a102af03 100644 --- a/man/coqide.1 +++ b/man/coqide.1 @@ -100,15 +100,6 @@ Skip loading of rcfile. Set the rcfile to .IR f . .TP -.B \-batch -Batch mode (exits just after arguments parsing). -.TP -.B \-boot -Boot mode (implies -.B \-q -and -.BR \-batch ). -.TP .B \-emacs Tells Coq it is executed under Emacs. .TP diff --git a/man/coqtop.1 b/man/coqtop.1 index addfb54672..25d0ef7718 100644 --- a/man/coqtop.1 +++ b/man/coqtop.1 @@ -106,12 +106,6 @@ set the rcfile to batch mode (exits just after arguments parsing) .TP -.B \-boot -boot mode (implies -.B \-q -) - -.TP .B \-emacs tells Coq it is executed under Emacs diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 25a7675113..ca09cad1f3 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -353,7 +353,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) in let names = ref [new_princ_name] in let hook = - fun new_principle_type _ _ -> + fun new_principle_type _ _ _ _ -> if Option.is_empty sorts then (* let id_of_f = Label.to_id (con_label f) in *) @@ -385,7 +385,8 @@ let generate_functional_principle (evd: Evd.evar_map ref) (* Pr 1278 : Don't forget to close the goal if an error is raised !!!! *) - save false new_princ_name entry g_kind ~hook + let uctx = Evd.evar_universe_context sigma in + save false new_princ_name entry ~hook uctx g_kind with e when CErrors.noncritical e -> begin begin @@ -539,7 +540,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ this_block_funs 0 (prove_princ_for_struct evd false 0 (Array.of_list (List.map fst funs))) - (fun _ _ _ -> ()) + (fun _ _ _ _ _ -> ()) with e when CErrors.noncritical e -> begin begin @@ -614,7 +615,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ this_block_funs !i (prove_princ_for_struct evd false !i (Array.of_list (List.map fst funs))) - (fun _ _ _ -> ()) + (fun _ _ _ _ _ -> ()) in const with Found_type i -> diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index f9938c0356..cba3cc3d42 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -129,7 +129,7 @@ let get_locality = function | Local -> true | Global -> false -let save with_clean id const ?hook (locality,_,kind) = +let save with_clean id const ?hook uctx (locality,_,kind) = let fix_exn = Future.fix_exn_of const.const_entry_body in let l,r = match locality with | Discharge when Lib.sections_are_opened () -> @@ -144,7 +144,7 @@ let save with_clean id const ?hook (locality,_,kind) = (locality, ConstRef kn) in if with_clean then Proof_global.discard_current (); - Lemmas.call_hook ?hook ~fix_exn l r; + Lemmas.call_hook ?hook ~fix_exn uctx [] l r; definition_message id let with_full_print f a = diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 9584649cff..1e0b95df34 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -42,7 +42,14 @@ val const_of_id: Id.t -> GlobRef.t(* constantyes *) val jmeq : unit -> EConstr.constr val jmeq_refl : unit -> EConstr.constr -val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> ?hook:Lemmas.declaration_hook -> Decl_kinds.goal_kind -> unit +val save + : bool + -> Id.t + -> Safe_typing.private_constants Entries.definition_entry + -> ?hook:Lemmas.declaration_hook + -> UState.t + -> Decl_kinds.goal_kind + -> unit (* [with_full_print f a] applies [f] to [a] in full printing environment. diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index a8517e9ab1..8746c37309 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1310,7 +1310,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp let na = next_global_ident_away name Id.Set.empty in if Termops.occur_existential sigma gls_type then CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials"); - let hook _ _ = + let hook _ _ _ _ = let opacity = let na_ref = qualid_of_ident na in let na_global = Smartlocate.global_with_alias na_ref in @@ -1560,7 +1560,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let tcc_lemma_name = add_suffix function_name "_tcc" in let tcc_lemma_constr = ref Undefined in (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) - let hook _ _ = + let hook _ _ _ _ = let term_ref = Nametab.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_ident term_id] in diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 7da4464e59..2d833a2cde 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1989,7 +1989,7 @@ let add_morphism_infer atts m n = Decl_kinds.DefinitionBody Decl_kinds.Instance in let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in - let hook _ = function + let hook _ _ _ = function | Globnames.ConstRef cst -> add_instance (Typeclasses.new_instance (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info diff --git a/pretyping/cases.ml b/pretyping/cases.ml index ed7c3d6770..1ad90b2953 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -426,7 +426,7 @@ let adjust_tomatch_to_pattern ~program_mode sigma pb ((current,typ),deps,dep) = let tm1 = List.map (fun eqn -> List.hd eqn.patterns) pb.mat in (match find_row_ind tm1 with | None -> sigma, (current, tmtyp) - | Some (_,(ind,_)) -> + | Some (loc,(ind,_)) -> let sigma, indt = inductive_template !!(pb.env) sigma None ind in let sigma, current = if List.is_empty deps && isEvar sigma typ then @@ -435,7 +435,7 @@ let adjust_tomatch_to_pattern ~program_mode sigma pb ((current,typ),deps,dep) = | None -> sigma, current | Some sigma -> sigma, current else - let sigma, j = Coercion.inh_conv_coerce_to ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in + let sigma, j = Coercion.inh_conv_coerce_to ?loc ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in sigma, j.uj_val in sigma, (current, try_find_ind !!(pb.env) sigma indt names)) diff --git a/stm/stm.ml b/stm/stm.ml index b4f26570c6..8af1a2ebd2 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2647,10 +2647,6 @@ type stm_init_options = { some point. *) doc_type : stm_doc_type; - (* Allow compiling modules in the Coq prefix. Irrelevant in - interactive mode. *) - allow_coq_overwrite : bool; - (* Initial load path in scope for the document. Usually extracted from -R options / _CoqProject *) iload_path : Mltop.coq_path list; @@ -2678,16 +2674,6 @@ let init_core () = if !cur_opt.async_proofs_mode = APon then Control.enable_thread_delay := true; State.register_root_state () -let check_coq_overwriting ~allow_coq_overwrite p = - if not allow_coq_overwrite then - let l = DirPath.repr p in - let id, l = match l with id::l -> id,l | [] -> assert false in - let is_empty = match l with [] -> true | _ -> false in - if not is_empty && Id.equal (CList.last l) Libnames.coq_root then - user_err - (str "Cannot build module " ++ DirPath.print p ++ str "." ++ spc () ++ - str "it starts with prefix \"Coq\" which is reserved for the Coq library.") - let dirpath_of_file f = let ldir0 = try @@ -2700,7 +2686,7 @@ let dirpath_of_file f = let ldir = Libnames.add_dirpath_suffix ldir0 id in ldir -let new_doc { doc_type ; allow_coq_overwrite; iload_path; require_libs; stm_options } = +let new_doc { doc_type ; iload_path; require_libs; stm_options } = let load_objs libs = let rq_file (dir, from, exp) = @@ -2735,14 +2721,12 @@ let new_doc { doc_type ; allow_coq_overwrite; iload_path; require_libs; stm_opti | VoDoc f -> let ldir = dirpath_of_file f in - check_coq_overwriting ~allow_coq_overwrite ldir; let () = Flags.verbosely Declaremods.start_library ldir in VCS.set_ldir ldir; set_compilation_hints f | VioDoc f -> let ldir = dirpath_of_file f in - check_coq_overwriting ~allow_coq_overwrite ldir; let () = Flags.verbosely Declaremods.start_library ldir in VCS.set_ldir ldir; set_compilation_hints f diff --git a/stm/stm.mli b/stm/stm.mli index 102e832d3e..91651e3534 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -67,10 +67,6 @@ type stm_init_options = { some point. *) doc_type : stm_doc_type; - (* Allow compiling modules in the Coq prefix. Irrelevant in - interactive mode. *) - allow_coq_overwrite : bool; - (* Initial load path in scope for the document. Usually extracted from -R options / _CoqProject *) iload_path : Mltop.coq_path list; diff --git a/test-suite/Makefile b/test-suite/Makefile index 03bfc5ffac..5582503d89 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -34,20 +34,24 @@ include ../Makefile.common # Default value when called from a freshly compiled Coq, but can be # easily overridden -LIB := .. + BIN := $(shell cd ..; pwd)/bin/ COQFLAGS?= -coqc_boot := $(BIN)coqc -coqlib $(LIB) -boot -q -test-mode -R prerequisite TestSuite $(COQFLAGS) -coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite $(COQFLAGS) -coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite +ifeq ($(COQLIB),) + # This method of setting `pwd` won't work on win32 OCaml + COQLIB := $(shell cd ..; pwd) +endif +export COQLIB + +coqc := $(BIN)coqc -q -R prerequisite TestSuite $(COQFLAGS) +coqchk := $(BIN)coqchk -R prerequisite TestSuite coqdoc := $(BIN)coqdoc -coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -test-mode -R prerequisite TestSuite -coqtopbyte := $(BIN)coqtop.byte +coqtop := $(BIN)coqtop -q -test-mode -R prerequisite TestSuite +coqtopbyte := $(BIN)coqtop.byte -q -coqc_interactive := $(coqc) -async-proofs-cache force -coqc_boot_interactive := $(coqc_boot) -async-proofs-cache force -coqdep := $(BIN)coqdep -coqlib $(LIB) +coqc_interactive := $(coqc) -test-mode -async-proofs-cache force +coqdep := $(BIN)coqdep VERBOSE?= SHOW := $(if $(VERBOSE),@true,@echo) @@ -398,7 +402,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) $(HIDE){ \ echo $(call log_intro,$<); \ output=$*.out.real; \ - $(coqc_boot_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \ + $(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \ | grep -v "Welcome to Coq" \ | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ @@ -437,7 +441,7 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out echo $(call log_intro,$<); \ tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \ tmpexpected=`mktemp /tmp/coqcheck.XXXXXX`; \ - $(coqc_boot_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \ + $(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \ | grep -v "Welcome to Coq" \ | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ @@ -492,7 +496,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG) $(HIDE){ \ echo $(call log_intro,$<); \ true "extract effective user time"; \ - res=`$(coqc_boot_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`; \ + res=`$(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`; \ R=$$?; times; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ @@ -556,7 +560,7 @@ $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG) echo $(call log_intro,$<); \ export BIN="$(BIN)"; \ export coqc="$(coqc)"; \ - export coqtop="$(coqc_boot)"; \ + export coqtop="$(coqc)"; \ export coqdep="$(coqdep)"; \ export coqtopbyte="$(coqtopbyte)"; \ "$<" 2>&1; R=$$?; times; \ @@ -578,7 +582,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake)) @echo "TEST $<" $(HIDE){ \ echo $(call log_intro,$<); \ - $(BIN)fake_ide $< "-coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off $(call get_coq_prog_args,"$<")" 2>&1; \ + $(BIN)fake_ide "$<" "-q -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off $(call get_coq_prog_args,"$<")" 2>&1; \ if [ $$? = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ diff --git a/test-suite/bugs/closed/bug_3393.v b/test-suite/bugs/closed/bug_3393.v index d2eb61e3e2..b0b573f5d5 100644 --- a/test-suite/bugs/closed/bug_3393.v +++ b/test-suite/bugs/closed/bug_3393.v @@ -109,6 +109,7 @@ Global Instance isisomorphism_compose' `{Funext} `{@IsIsomorphism (C -> D) F F' T} : @IsIsomorphism (C -> D) F F'' (T' o T)%natural_transformation := @isisomorphism_compose (C -> D) _ _ T' _ _ T _. +Arguments isisomorphism_compose' {H C D F' F''} T' {F} T {H0 H1}. Section lemmas. Context `{Funext}. Variable C : PreCategory. diff --git a/test-suite/bugs/closed/bug_3422.v b/test-suite/bugs/closed/bug_3422.v index 460ae8f110..1305104cdb 100644 --- a/test-suite/bugs/closed/bug_3422.v +++ b/test-suite/bugs/closed/bug_3422.v @@ -175,6 +175,7 @@ Global Instance isisomorphism_compose' `{@IsIsomorphism (C -> D) F F' T} : @IsIsomorphism (C -> D) F F'' (T' o T)%natural_transformation := @isisomorphism_compose (C -> D) _ _ T' _ _ T _. +Arguments isisomorphism_compose' {C D F' F''} T' {F} T {H H0}. Section lemmas. Local Open Scope natural_transformation_scope. diff --git a/test-suite/bugs/closed/bug_5198.v b/test-suite/bugs/closed/bug_5198.v index 5d4409f89b..4f24189d3f 100644 --- a/test-suite/bugs/closed/bug_5198.v +++ b/test-suite/bugs/closed/bug_5198.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-boot" "-nois") -*- *) +(* -*- mode: coq; coq-prog-args: ("-nois") -*- *) (* File reduced by coq-bug-finder from original input, then from 286 lines to 27 lines, then from 224 lines to 53 lines, then from 218 lines to 56 lines, then from 269 lines to 180 lines, then from 132 lines to 48 lines, then from diff --git a/test-suite/bugs/closed/bug_9313.v b/test-suite/bugs/closed/bug_9313.v new file mode 100644 index 0000000000..0845e7732c --- /dev/null +++ b/test-suite/bugs/closed/bug_9313.v @@ -0,0 +1,13 @@ +Set Implicit Arguments. +Existing Class True. + +Instance foo1 (a : nat) {b : nat} (e : a = b) : True := I. +Check foo1 (a := 3) (b := 4). + +Definition foo2 (a : nat) {b : nat} (e : a = b) : True := I. +Check foo2 (a := 3) (b := 4). + +Instance foo3 (a : nat) {b : nat} (e : a = b) : True. +exact I. +Qed. +Check foo3 (a := 3) (b := 4). diff --git a/test-suite/bugs/closed/bug_9363.v b/test-suite/bugs/closed/bug_9363.v new file mode 100644 index 0000000000..a3f6ad9fa2 --- /dev/null +++ b/test-suite/bugs/closed/bug_9363.v @@ -0,0 +1,17 @@ +(* Outside a section, Hypothesis, Variable, Axiom all obey implicit binders *) +Hypothesis foo1 : forall {n : nat}, True. +Variable foo1' : forall {n : nat}, True. +Axiom foo1'' : forall {n : nat}, True. +Check foo1 (n := 1). +Check foo1' (n := 1). +Check foo1'' (n := 1). + +Section bar. +(* Inside a section, Hypothesis and Variable do not, but they should *) +Hypothesis foo2 : forall {n : nat}, True. +Variable foo2' : forall {n : nat}, True. +Axiom foo2'' : forall {n : nat}, True. +Check foo2 (n := 1). +Check foo2' (n := 1). +Check foo2'' (n := 1). +End bar. diff --git a/test-suite/bugs/closed/bug_9526.v b/test-suite/bugs/closed/bug_9526.v new file mode 100644 index 0000000000..344d42083f --- /dev/null +++ b/test-suite/bugs/closed/bug_9526.v @@ -0,0 +1,30 @@ +Primitive int := #int63_type. + +Module bad1. +Polymorphic Inductive badcarry1 (A:Type) : Type := +| C0: A -> badcarry1 A +| C1: A -> badcarry1 A. + +Fail Register badcarry1 as kernel.ind_carry. + +End bad1. + +Module bad2. + +Inductive badcarry2 (A:Set) : Set := +| C0: A -> badcarry2 A +| C1: A -> badcarry2 A. + +Fail Register badcarry2 as kernel.ind_carry. + +End bad2. + +Module bad3. + +Inductive badcarry3 : Type -> Type := +| C0: forall A, A -> badcarry3 A +| C1: forall A, A -> badcarry3 A. + +Fail Register badcarry3 as kernel.ind_carry. + +End bad3. diff --git a/test-suite/dune b/test-suite/dune index eae072553a..9efc1e2dc1 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -1,3 +1,13 @@ +; The easiest way to generate a portable absolute path is to use OCaml +; itself to print it +(executable + (name ocaml_pwd) + (modules ocaml_pwd)) + +(rule + (targets libpath.inc) + (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe ../../install/%{context_name}/lib/coq/ )))) + (rule (targets summary.log) (deps @@ -14,60 +24,13 @@ ; For fake_ide (package coqide-server) (source_tree .)) - ; Finer-grained dependencies look like this + ; Finer-grained dependencies would look like this and be generated + ; by coqdep; that would allow tests to be run incrementally. ; ../tools/CoqMakefile.in ; ../theories/Init/Prelude.vo - ; ../theories/Arith/Arith.vo - ; ../theories/Arith/Compare.vo - ; ../theories/PArith/PArith.vo - ; ../theories/QArith/QArith.vo - ; ../theories/QArith/Qcanon.vo - ; ../theories/ZArith/ZArith.vo - ; ../theories/ZArith/Zwf.vo - ; ../theories/Sets/Ensembles.vo - ; ../theories/Numbers/Natural/Peano/NPeano.vo - ; ../theories/Numbers/Cyclic/Int31/Cyclic31.vo - ; ../theories/FSets/FMaps.vo - ; ../theories/FSets/FSets.vo - ; ../theories/MSets/MSets.vo - ; ../theories/Compat/Coq87.vo - ; ../theories/Compat/Coq88.vo - ; ../theories/Relations/Relations.vo - ; ../theories/Unicode/Utf8.vo - ; ../theories/Program/Program.vo - ; ../theories/Classes/EquivDec.vo - ; ../theories/Classes/DecidableClass.vo - ; ../theories/Classes/SetoidClass.vo - ; ../theories/Classes/RelationClasses.vo - ; ../theories/Logic/Classical.vo - ; ../theories/Logic/Hurkens.vo - ; ../theories/Logic/ClassicalFacts.vo - ; ../theories/Reals/Reals.vo - ; ../theories/Lists/Streams.vo - ; ../plugins/micromega/Lia.vo - ; ../plugins/micromega/Lqa.vo - ; ../plugins/micromega/Psatz.vo - ; ../plugins/micromega/MExtraction.vo - ; ../plugins/nsatz/Nsatz.vo - ; ../plugins/omega/Omega.vo - ; ../plugins/ssr/ssrbool.vo - ; ../plugins/derive/Derive.vo - ; ../plugins/funind/Recdef.vo - ; ../plugins/extraction/Extraction.vo - ; ../plugins/extraction/ExtrOcamlNatInt.vo - ; coqtop - ; coqtop.opt - ; coqidetop.opt - ; coqqueryworker.opt - ; coqtacticworker.opt - ; coqproofworker.opt - ; coqc - ; coqchk - ; coqdoc + ; %{bin:coqc} ; %{bin:coq_makefile} ; %{bin:fake_ide} (action (progn - ; XXX: we will allow to set the NJOBS variable in a future Dune - ; version, either by using an env var or by letting Dune set `-j` - (run make -j 2 BIN= PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests})))) + (bash "make -j %{env:NJOBS=2} BIN= COQLIB=%{read:libpath.inc} PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests}")))) diff --git a/test-suite/ocaml_pwd.ml b/test-suite/ocaml_pwd.ml new file mode 100644 index 0000000000..10ca52a4a9 --- /dev/null +++ b/test-suite/ocaml_pwd.ml @@ -0,0 +1,7 @@ +let _ = + let ch_dir = Sys.argv.(1) in + Sys.chdir ch_dir; + let dir = Sys.getcwd () in + (* Needed for windows *) + let dir = Filename.quote dir in + Format.printf "%s%!" dir diff --git a/test-suite/success/AdvancedTypeClasses.v b/test-suite/success/AdvancedTypeClasses.v index d0aa5c8578..0253ec46e4 100644 --- a/test-suite/success/AdvancedTypeClasses.v +++ b/test-suite/success/AdvancedTypeClasses.v @@ -71,7 +71,7 @@ Variable Inhabited: term -> Prop. Variable Inhabited_correct: forall `{interp_pair p}, Inhabited (repr p) -> p. Lemma L : Prop * A -> bool * (Type -> Set) . -apply (Inhabited_correct _ _). +apply Inhabited_correct. change (Inhabited (Fun (Prod PROP (Var A)) (Prod Bool (Fun TYPE SET)))). Admitted. diff --git a/theories/Classes/CEquivalence.v b/theories/Classes/CEquivalence.v index c376efef2e..f04ae90950 100644 --- a/theories/Classes/CEquivalence.v +++ b/theories/Classes/CEquivalence.v @@ -64,6 +64,9 @@ Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv. now transitivity y. Qed. +Arguments equiv_symmetric {A R} sa x y. +Arguments equiv_transitive {A R} sa x y z. + (** Use the [substitute] command which substitutes an equivalence in every hypothesis. *) Ltac setoid_subst H := diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index 516ea12099..384d041461 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -64,6 +64,9 @@ Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv | 1. now transitivity y. Qed. +Arguments equiv_symmetric {A R} sa x y. +Arguments equiv_transitive {A R} sa x y z. + (** Use the [substitute] command which substitutes an equivalence in every hypothesis. *) Ltac setoid_subst H := diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index f8f10b34ae..bd9d8c9221 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -187,7 +187,7 @@ COQDOCLIBS?=$(COQLIBS_NOML) COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1) COQMAKEFILE_VERSION:=@COQ_VERSION@ -COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") +COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)") CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) @@ -216,9 +216,9 @@ endif concat_path = $(if $(1),$(1)/$(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(2)),$(2)),$(2)) -COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)user-contrib) -COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)user-contrib) -COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)toploop) +COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/user-contrib) +COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)/user-contrib) +COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/toploop) # Files ####################################################################### # diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml index 68371edcb1..62a871aa0e 100644 --- a/tools/coq_dune.ml +++ b/tools/coq_dune.ml @@ -186,7 +186,7 @@ let pp_vo_dep dir fmt vo = (* We explicitly include the location of coqlib to avoid tricky issues with coqlib location *) let libflag = "-coqlib %{project_root}" in (* The final build rule *) - let action = sprintf "(chdir %%{project_root} (run coqc -boot %s %s %s %s))" libflag eflag cflag source in + let action = sprintf "(chdir %%{project_root} (run coqc -q %s %s %s %s))" libflag eflag cflag source in let all_targets = gen_coqc_targets vo in pp_rule fmt all_targets deps action diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 4f01a6bd87..68281d6481 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -123,9 +123,10 @@ let read_whole_file s = let quote s = if String.contains s ' ' || CString.is_empty s then "'" ^ s ^ "'" else s let generate_makefile oc conf_file local_file args project = + let coqlib = Envars.coqlib () in let makefile_template = - let template = "/tools/CoqMakefile.in" in - Envars.coqlib () ^ template in + let template = Filename.concat "tools" "CoqMakefile.in" in + Filename.concat coqlib template in let s = read_whole_file makefile_template in let s = List.fold_left (* We use global_substitute to avoid running into backslash issues due to \1 etc. *) @@ -260,7 +261,7 @@ let generate_conf_doc oc { defs; q_includes; r_includes } = eprintf "Warning: in %s\n" destination; destination end else "$(INSTALLDEFAULTROOT)" - else String.concat "/" gcd in + else String.concat Filename.dir_sep gcd in Printf.fprintf oc "COQMF_INSTALLCOQDOCROOT = %s\n" (quote root) let generate_conf_defs oc { defs; extra_args } = @@ -343,15 +344,13 @@ let chop_prefix p f = let len_f = String.length f in String.sub f len_p (len_f - len_p) -let clean_path p = - Str.global_replace (Str.regexp_string "//") "/" p - let destination_of { ml_includes; q_includes; r_includes; } file = let file_dir = CUnix.canonical_path_name (Filename.dirname file) in let includes = q_includes @ r_includes in let mk_destination logic canonical_path = - clean_path (physical_dir_of_logical_dir logic ^ "/" ^ - chop_prefix canonical_path file_dir ^ "/") in + Filename.concat + (physical_dir_of_logical_dir logic) + (chop_prefix canonical_path file_dir) in let candidates = CList.map_filter (fun {thing={ canonical_path }, logic} -> if is_prefix canonical_path file_dir then @@ -368,8 +367,9 @@ let destination_of { ml_includes; q_includes; r_includes; } file = with | [{thing={ canonical_path }, logic}], {thing={ canonical_path = p }} -> let destination = - clean_path (physical_dir_of_logical_dir logic ^ "/" ^ - chop_prefix p file_dir ^ "/") in + Filename.concat + (physical_dir_of_logical_dir logic) + (chop_prefix p file_dir) in Printf.printf "%s" (quote destination) | _ -> () (* skip *) | exception Not_found -> () (* skip *) diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml index 0ffa5bd7e4..c6d3551561 100644 --- a/tools/coq_tex.ml +++ b/tools/coq_tex.ml @@ -259,8 +259,6 @@ let parse_cl () = " Coq parts are written between 2 horizontal lines"; "-small", Arg.Set small, " Coq parts are written in small font"; - "-boot", Arg.Set boot, - " Launch coqtop with the -boot option" ] (fun s -> files := s :: !files) "coq-tex [options] file ..." @@ -279,7 +277,6 @@ let find_coqtop () = let _ = parse_cl (); if !image = "" then image := Filename.quote (find_coqtop ()); - if !boot then image := !image ^ " -boot"; if Sys.command (!image ^ " -batch -silent") <> 0 then begin Printf.printf "Error: "; let _ = Sys.command (!image ^ " -batch") in diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml index 0d3fb77551..5dd6cc6c83 100644 --- a/tools/coqdoc/cdglobals.ml +++ b/tools/coqdoc/cdglobals.ml @@ -79,14 +79,17 @@ let use_suffix prefix suffix = (** A weaker analog of the function in Envars *) +let getenv_else s dft = try Sys.getenv s with Not_found -> dft () + let guess_coqlib () = + getenv_else "COQLIB" (fun () -> let file = "theories/Init/Prelude.vo" in let coqbin = normalize_path (Filename.dirname Sys.executable_name) in let prefix = Filename.dirname coqbin in let coqlib = use_suffix prefix Coq_config.coqlibsuffix in if Sys.file_exists (coqlib / file) then coqlib else if not Coq_config.local && Sys.file_exists (Coq_config.coqlib / file) - then Coq_config.coqlib else prefix + then Coq_config.coqlib else prefix) let header_trailer = ref true let header_file = ref "" diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 1be440a750..230c5524b7 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -409,6 +409,7 @@ let set_kw = let gallina_kw_to_hide = "Implicit" space+ "Arguments" | ("Local" space+)? "Ltac" + | "From" | "Require" | "Import" | "Export" diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 606d954672..b703af934d 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -32,7 +32,7 @@ let is_keyword = build_table [ "About"; "AddPath"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "Compute"; "CoFixpoint"; "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example"; - "Export"; "Fact"; "Fix"; "Fixpoint"; "Function"; "Generalizable"; "Global"; "Grammar"; + "Export"; "Fact"; "Fix"; "Fixpoint"; "From"; "Function"; "Generalizable"; "Global"; "Grammar"; "Guarded"; "Goal"; "Hint"; "Debug"; "On"; "Hypothesis"; "Hypotheses"; "Resolve"; "Unfold"; "Immediate"; "Extern"; "Constructors"; "Rewrite"; diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index 8064ee8880..3fe6ad0718 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -112,7 +112,6 @@ let compile opts copts ~echo ~f_in ~f_out = let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude) Stm.new_doc Stm.{ doc_type = VoDoc long_f_dot_vo; - allow_coq_overwrite = opts.boot; iload_path; require_libs; stm_options; } in let state = { doc; sid; proof = None; time = opts.time } in @@ -163,7 +162,6 @@ let compile opts copts ~echo ~f_in ~f_out = let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude) Stm.new_doc Stm.{ doc_type = VioDoc long_f_dot_vio; - allow_coq_overwrite = opts.boot; iload_path; require_libs; stm_options; } in diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 0c9201c3a5..abfda07426 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -40,8 +40,6 @@ type native_compiler = NativeOff | NativeOn of { ondemand : bool } type t = { - boot : bool; - load_init : bool; load_rcfile : bool; rcfile : string option; @@ -93,8 +91,6 @@ let default_native = let default = { - boot = false; - load_init = true; load_rcfile = true; rcfile = None; @@ -179,6 +175,10 @@ let warn_deprecated_inputstate = CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.") +let warn_deprecated_boot = + CWarnings.create ~name:"deprecated-boot" ~category:"noop" + (fun () -> Pp.strbrk "The -boot option is deprecated, please use -q and/or -coqlib options instead.") + let set_inputstate opts s = warn_deprecated_inputstate (); { opts with inputstate = Some s } @@ -459,7 +459,9 @@ let parse_args ~help ~init arglist : t * string list = { oval with batch = true } |"-test-mode" -> Flags.test_mode := true; oval |"-beautify" -> Flags.beautify := true; oval - |"-boot" -> { oval with boot = true; load_rcfile = false; } + |"-boot" -> + warn_deprecated_boot (); + { oval with load_rcfile = false; } |"-bt" -> Backtrace.record_backtrace true; oval |"-color" -> set_color oval (next ()) |"-config"|"--config" -> { oval with print_config = true } diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index 9cc846edea..b89a88d1f6 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -16,8 +16,6 @@ type native_compiler = NativeOff | NativeOn of { ondemand : bool } type t = { - boot : bool; - load_init : bool; load_rcfile : bool; rcfile : string option; diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index e1d35e537b..74a089510e 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -11,7 +11,7 @@ open Util open Pp -let ( / ) s1 s2 = s1 ^ "/" ^ s2 +let ( / ) s1 s2 = Filename.concat s1 s2 let set_debug () = let () = Backtrace.record_backtrace true in diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 9115fbb726..92ac200bc0 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -221,7 +221,6 @@ let init_toploop opts = let doc, sid = Stm.(new_doc { doc_type = Interactive opts.toplevel_name; - allow_coq_overwrite = true; (* irrelevant *) iload_path; require_libs; stm_options; }) in let state = { doc; sid; proof = None; time = opts.time } in diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 0d17218a56..94ec6bb70d 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -62,7 +62,6 @@ let print_usage_common co command = \n\ \n -q skip loading of rcfile\ \n -init-file f set the rcfile to f\ -\n -boot boot mode (allows to overload the `Coq` library prefix, implies -q)\ \n -bt print backtraces (requires configure debug flag)\ \n -debug debug mode (implies -bt)\ \n -diffs (on|off|removed) highlight differences between proof steps\ diff --git a/vernac/class.ml b/vernac/class.ml index 823177d4d1..a6b3242cae 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -302,7 +302,7 @@ let try_add_new_identity_coercion id ~local poly ~source ~target = let try_add_new_coercion_with_source ref ~local poly ~source = try_add_new_coercion_core ref ~local poly (Some source) None false -let add_coercion_hook poly local ref = +let add_coercion_hook poly _uctx _trans local ref = let local = match local with | Discharge | Local -> true @@ -314,7 +314,7 @@ let add_coercion_hook poly local ref = let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly) -let add_subclass_hook poly local ref = +let add_subclass_hook poly _uctx _trans local ref = let stre = match local with | Local -> true | Global -> false diff --git a/vernac/classes.ml b/vernac/classes.ml index 27d8b7390d..263ebf5f5a 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -106,7 +106,7 @@ let id_of_class cl = | _ -> assert false let instance_hook k info global imps ?hook cst = - Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps; + Impargs.maybe_declare_manual_implicits false cst imps; let info = intern_info info in Typeclasses.declare_instance (Some info) (not global) cst; (match hook with Some h -> h cst | None -> ()) @@ -149,7 +149,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id if program_mode then let hook _ _ vis gr = let cst = match gr with ConstRef kn -> kn | _ -> assert false in - Impargs.declare_manual_implicits false gr ~enriching:false [imps]; + Impargs.declare_manual_implicits false gr [imps]; let pri = intern_info pri in Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst) in @@ -161,10 +161,10 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id in obls, Some constr, typ | None -> [||], None, termtype in - let univ_hook = Obligations.mk_univ_hook hook in + let hook = Lemmas.mk_hook hook in let ctx = Evd.evar_universe_context sigma in ignore (Obligations.add_definition id ?term:constr - ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~univ_hook obls) + ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls) else Flags.silently (fun () -> (* spiwack: it is hard to reorder the actions to do @@ -175,7 +175,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id let sigma = Evd.reset_future_goals sigma in Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype) ~hook:(Lemmas.mk_hook - (fun _ -> instance_hook k pri global imps ?hook)); + (fun _ _ _ -> instance_hook k pri global imps ?hook)); (* spiwack: I don't know what to do with the status here. *) if not (Option.is_empty term) then let init_refine = diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 466757c6bd..35d8be5c56 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Pp open CErrors open Util open Vars @@ -54,10 +53,11 @@ match local with let () = assumption_message ident in let () = if not !Flags.quiet && Proof_global.there_are_pending_proofs () then - Feedback.msg_info (str"Variable" ++ spc () ++ Id.print ident ++ + Feedback.msg_info Pp.(str"Variable" ++ spc () ++ Id.print ident ++ strbrk " is not visible from current goals") in let r = VarRef ident in + let () = maybe_declare_manual_implicits true r imps in let () = Typeclasses.declare_instance None true r in let () = if is_coe then Class.try_add_new_coercion r ~local:true false in (r,Univ.Instance.empty,true) @@ -203,4 +203,4 @@ let do_primitive id prim typopt = } in let _kn = declare_constant id.CAst.v (PrimitiveEntry entry,IsPrimitive) in - register_message id.CAst.v + Flags.if_verbose Feedback.msg_info Pp.(Id.print id.CAst.v ++ str " is declared") diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 5eb19eef54..28773a3965 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -94,22 +94,24 @@ let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt = let (ce, evd, univdecl, imps as def) = interp_definition ~program_mode univdecl bl (pi2 k) red_option c ctypopt in - if program_mode then - let env = Global.env () in - let (c,ctx), sideff = Future.force ce.const_entry_body in - assert(Safe_typing.empty_private_constants = sideff); - assert(Univ.ContextSet.is_empty ctx); - let typ = match ce.const_entry_type with - | Some t -> t - | None -> EConstr.to_constr ~abort_on_undefined_evars:false evd (Retyping.get_type_of env evd (EConstr.of_constr c)) - in - Obligations.check_evars env evd; - let obls, _, c, cty = - Obligations.eterm_obligations env ident evd 0 c typ - in - let ctx = Evd.evar_universe_context evd in - let univ_hook = Obligations.mk_univ_hook (fun _ _ l r -> Lemmas.call_hook ?hook l r) in - ignore(Obligations.add_definition - ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~univ_hook obls) - else let ce = check_definition ~program_mode def in - ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps ?hook) + if program_mode then + let env = Global.env () in + let (c,ctx), sideff = Future.force ce.const_entry_body in + assert(Safe_typing.empty_private_constants = sideff); + assert(Univ.ContextSet.is_empty ctx); + let typ = match ce.const_entry_type with + | Some t -> t + | None -> EConstr.to_constr ~abort_on_undefined_evars:false evd (Retyping.get_type_of env evd (EConstr.of_constr c)) + in + Obligations.check_evars env evd; + let obls, _, c, cty = + Obligations.eterm_obligations env ident evd 0 c typ + in + let ctx = Evd.evar_universe_context evd in + ignore(Obligations.add_definition + ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ?hook obls) + else + let ce = check_definition ~program_mode def in + let uctx = Evd.evar_universe_context evd in + let hook_data = Option.map (fun hook -> hook, uctx, []) hook in + ignore(DeclareDef.declare_definition ident k ?hook_data ce (Evd.universe_binders evd) imps ) diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index a30313d37c..cc9c83bd17 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -227,7 +227,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = in hook, recname, typ in (* XXX: Capturing sigma here... bad bad *) - let univ_hook = Obligations.mk_univ_hook (hook sigma) in + let hook = Lemmas.mk_hook (hook sigma) in (* XXX: Grounding non-ground terms here... bad bad *) let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in let fullctyp = EConstr.to_constr sigma typ in @@ -237,7 +237,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = in let ctx = Evd.evar_universe_context sigma in ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl - evars_typ ctx evars ~univ_hook) + evars_typ ctx evars ~hook) let out_def = function | Some def -> def diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 361ed1a737..7dcd098183 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -33,7 +33,7 @@ let get_locality id ~kind = function | Local -> true | Global -> false -let declare_definition ident (local, p, k) ?hook ce pl imps = +let declare_definition ident (local, p, k) ?hook_data ce pl imps = let fix_exn = Future.fix_exn_of ce.const_entry_body in let gr = match local with | Discharge when Lib.sections_are_opened () -> @@ -49,11 +49,17 @@ let declare_definition ident (local, p, k) ?hook ce pl imps = in let () = maybe_declare_manual_implicits false gr imps in let () = definition_message ident in - Lemmas.call_hook ~fix_exn ?hook local gr; gr + begin + match hook_data with + | None -> () + | Some (hook, uctx, extra_defs) -> + Lemmas.call_hook ~fix_exn ~hook uctx extra_defs local gr + end; + gr -let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t imps = +let declare_fix ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps = let ce = definition_entry ~opaque ~types:t ~univs ~eff def in - declare_definition f kind ce pl imps + declare_definition f kind ?hook_data ce pl imps let check_definition_evars ~allow_evars sigma = let env = Global.env () in diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index e455b59ab2..3f95ec7107 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -13,16 +13,26 @@ open Decl_kinds val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool -val declare_definition : Id.t -> definition_kind -> - ?hook:Lemmas.declaration_hook -> - Safe_typing.private_constants Entries.definition_entry -> UnivNames.universe_binders -> Impargs.manual_implicits -> - GlobRef.t +val declare_definition + : Id.t + -> definition_kind + -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list) + -> Safe_typing.private_constants Entries.definition_entry + -> UnivNames.universe_binders + -> Impargs.manual_implicits + -> GlobRef.t -val declare_fix : ?opaque:bool -> definition_kind -> - UnivNames.universe_binders -> Entries.universes_entry -> - Id.t -> Safe_typing.private_constants Entries.proof_output -> - Constr.types -> Impargs.manual_implicits -> - GlobRef.t +val declare_fix + : ?opaque:bool + -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list) + -> definition_kind + -> UnivNames.universe_binders + -> Entries.universes_entry + -> Id.t + -> Safe_typing.private_constants Entries.proof_output + -> Constr.types + -> Impargs.manual_implicits + -> GlobRef.t val prepare_definition : allow_evars:bool -> ?opaque:bool -> ?inline:bool -> poly:bool -> diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 83dd1aa8e4..77f125e878 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -34,10 +34,13 @@ open Impargs module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -type declaration_hook = Decl_kinds.locality -> GlobRef.t -> unit +type hook_type = UState.t -> (Id.t * Constr.t) list -> Decl_kinds.locality -> GlobRef.t -> unit +type declaration_hook = hook_type + let mk_hook hook = hook -let call_hook ?hook ?fix_exn l c = - try Option.iter (fun hook -> hook l c) hook + +let call_hook ?hook ?fix_exn uctx trans l c = + try Option.iter (fun hook -> hook uctx trans l c) hook with e when CErrors.noncritical e -> let e = CErrors.push e in let e = Option.cata (fun fix -> fix e) e fix_exn in @@ -174,7 +177,7 @@ let look_for_possibly_mutual_statements sigma = function (* Saving a goal *) -let save ?export_seff id const uctx do_guard (locality,poly,kind) hook = +let save ?export_seff id const uctx do_guard (locality,poly,kind) hook universes = let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in try let const = adjust_guardness_conditions const do_guard in @@ -203,7 +206,7 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook = gr in definition_message id; - call_hook ?hook locality r + call_hook ?hook universes [] locality r with e when CErrors.noncritical e -> let e = CErrors.push e in iraise (fix_exn e) @@ -289,7 +292,7 @@ let warn_let_as_axiom = (fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++ spc () ++ strbrk "declared as an axiom.") -let admit ?hook (id,k,e) pl () = +let admit ?hook ctx (id,k,e) pl () = let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in let () = match k with | Global, _, _ -> () @@ -297,16 +300,15 @@ let admit ?hook (id,k,e) pl () = in let () = assumption_message id in Declare.declare_univ_binders (ConstRef kn) pl; - call_hook ?hook Global (ConstRef kn) + call_hook ?hook ctx [] Global (ConstRef kn) (* Starting a goal *) -let universe_proof_terminator ?univ_hook compute_guard = +let standard_proof_terminator ?(hook : declaration_hook option) compute_guard = let open Proof_global in make_terminator begin function | Admitted (id,k,pe,ctx) -> - let hook = Option.map (fun univ_hook -> univ_hook (Some ctx)) univ_hook in - admit ?hook (id,k,pe) (UState.universe_binders ctx) (); + let () = admit ?hook ctx (id,k,pe) (UState.universe_binders ctx) () in Feedback.feedback Feedback.AddedAxiom | Proved (opaque,idopt, { id; entries=[const]; persistence; universes } ) -> let is_opaque, export_seff = match opaque with @@ -317,16 +319,12 @@ let universe_proof_terminator ?univ_hook compute_guard = let id = match idopt with | None -> id | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in - let hook = Option.map (fun univ_hook -> univ_hook (Some universes)) univ_hook in - save ~export_seff id const universes compute_guard persistence hook + let () = save ~export_seff id const universes compute_guard persistence hook universes in + () | Proved (opaque,idopt, _ ) -> CErrors.anomaly Pp.(str "[universe_proof_terminator] close_proof returned more than one proof term") end -let standard_proof_terminator ?hook compute_guard = - let univ_hook = Option.map (fun hook _ -> hook) hook in - universe_proof_terminator ?univ_hook compute_guard - let initialize_named_context_for_proof () = let sign = Global.named_context () in List.fold_right @@ -335,7 +333,7 @@ let initialize_named_context_for_proof () = let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in Environ.push_named_context_val d signv) sign Environ.empty_named_context_val -let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c = +let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?(hook : declaration_hook option) c = let terminator = match terminator with | None -> standard_proof_terminator ?hook compute_guard | Some terminator -> terminator ?hook compute_guard @@ -348,20 +346,6 @@ let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c let goals = [ Global.env_of_context sign , c ] in Proof_global.start_proof sigma id ?pl kind goals terminator -let start_proof_univs id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?univ_hook c = - let terminator = match terminator with - | None -> - universe_proof_terminator ?univ_hook compute_guard - | Some terminator -> terminator ?univ_hook compute_guard - in - let sign = - match sign with - | Some sign -> sign - | None -> initialize_named_context_for_proof () - in - let goals = [ Global.env_of_context sign , c ] in - Proof_global.start_proof sigma id ?pl kind goals terminator - let rec_tac_initializer finite guard thms snl = if finite then match List.map (fun (id,(t,_)) -> (id,t)) thms with @@ -394,11 +378,7 @@ let start_proof_with_initialization ?hook kind sigma decl recguard thms snl = match thms with | [] -> anomaly (Pp.str "No proof to start.") | (id,(t,(_,imps)))::other_thms -> - let hook ctx strength ref = - let ctx = match ctx with - | None -> UState.empty - | Some ctx -> ctx - in + let hook ctx _ strength ref = let other_thms_data = if List.is_empty other_thms then [] else (* there are several theorems defined mutually *) @@ -410,8 +390,8 @@ let start_proof_with_initialization ?hook kind sigma decl recguard thms snl = let thms_data = (strength,ref,imps)::other_thms_data in List.iter (fun (strength,ref,imps) -> maybe_declare_manual_implicits false ref imps; - call_hook ?hook strength ref) thms_data in - start_proof_univs id ~pl:decl kind sigma t ~univ_hook:(fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard; + call_hook ?hook ctx [] strength ref) thms_data in + start_proof id ~pl:decl kind sigma t ~hook ~compute_guard:guard; ignore (Proof_global.with_current_proof (fun _ p -> match init_tac with | None -> p,(true,[]) diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index a9a10a6e38..72c666e903 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -13,10 +13,29 @@ open Decl_kinds type declaration_hook -val mk_hook : (Decl_kinds.locality -> GlobRef.t -> unit) -> declaration_hook -val call_hook : - ?hook:declaration_hook -> ?fix_exn:Future.fix_exn -> - Decl_kinds.locality -> GlobRef.t -> unit +(* Hooks allow users of the API to perform arbitrary actions at + * proof/definition saving time. For example, to register a constant + * as a Coercion, perform some cleanup, update the search database, + * etc... + * + * Here, we use an extended hook type suitable for obligations / + * equations. + *) +(** [hook_type] passes to the client: + - [ustate]: universe constraints obtained when the term was closed + - [(n1,t1),...(nm,tm)]: association list between obligation + name and the corresponding defined term (might be a constant, + but also an arbitrary term in the Expand case of obligations) + - [locality]: Locality of the original declaration + - [ref]: identifier of the origianl declaration + *) +type hook_type = UState.t -> (Id.t * Constr.t) list -> Decl_kinds.locality -> GlobRef.t -> unit + +val mk_hook : hook_type -> declaration_hook +val call_hook + : ?hook:declaration_hook + -> ?fix_exn:Future.fix_exn + -> hook_type val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) -> @@ -24,12 +43,6 @@ val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ?compute_guard:Proof_global.lemma_possible_guards -> ?hook:declaration_hook -> EConstr.types -> unit -val start_proof_univs : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> - ?terminator:(?univ_hook:(UState.t option -> declaration_hook) -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) -> - ?sign:Environ.named_context_val -> - ?compute_guard:Proof_global.lemma_possible_guards -> - ?univ_hook:(UState.t option -> declaration_hook) -> EConstr.types -> unit - val start_proof_com : program_mode:bool -> ?inference_hook:Pretyping.inference_hook -> ?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list -> @@ -43,11 +56,6 @@ val start_proof_with_initialization : (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list -> int list option -> unit -val universe_proof_terminator : - ?univ_hook:(UState.t option -> declaration_hook) -> - Proof_global.lemma_possible_guards -> - Proof_global.proof_terminator - val standard_proof_terminator : ?hook:declaration_hook -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator diff --git a/vernac/obligations.ml b/vernac/obligations.ml index ba78c73131..38cdfc2d7a 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -20,15 +20,6 @@ open Pp open CErrors open Util -type univ_declaration_hook = UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit -let mk_univ_hook f = f -let call_univ_hook ?univ_hook ?fix_exn uctx trans l c = - try Option.iter (fun hook -> hook uctx trans l c) univ_hook - with e when CErrors.noncritical e -> - let e = CErrors.push e in - let e = Option.cata (fun fix -> fix e) e fix_exn in - iraise e - module NamedDecl = Context.Named.Declaration let get_fix_exn, stm_get_fix_exn = Hook.make () @@ -321,7 +312,7 @@ type program_info_aux = { prg_notations : notations ; prg_kind : definition_kind; prg_reduce : constr -> constr; - prg_hook : univ_declaration_hook option; + prg_hook : Lemmas.declaration_hook option; prg_opaque : bool; prg_sign: named_context_val; } @@ -482,9 +473,9 @@ let declare_definition prg = let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in let () = progmap_remove prg in let ubinders = UState.universe_binders uctx in - let hook = Lemmas.mk_hook (fun l r -> call_univ_hook ?univ_hook:prg.prg_hook ~fix_exn uctx obls l r; ()) in + let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in DeclareDef.declare_definition prg.prg_name - prg.prg_kind ce ubinders prg.prg_implicits ~hook + prg.prg_kind ce ubinders prg.prg_implicits ?hook_data let rec lam_index n t acc = match Constr.kind t with @@ -559,14 +550,16 @@ let declare_mutual_definition l = (* Declare the recursive definitions *) let univs = UState.univ_entry ~poly first.prg_ctx in let fix_exn = Hook.get get_fix_exn () in - let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs) - fixnames fixdecls fixtypes fiximps in - (* Declare notations *) - List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations; - Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; - let gr = List.hd kns in - call_univ_hook ?univ_hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr; - List.iter progmap_remove l; gr + let kns = List.map4 + (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs) + fixnames fixdecls fixtypes fiximps + in + (* Declare notations *) + List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations; + Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; + let gr = List.hd kns in + Lemmas.call_hook ?hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr; + List.iter progmap_remove l; gr let decompose_lam_prod c ty = let open Context.Rel.Declaration in @@ -663,7 +656,7 @@ let declare_obligation prg obl body ty uctx = in true, { obl with obl_body = body } -let init_prog_info ?(opaque = false) ?univ_hook sign n udecl b t ctx deps fixkind +let init_prog_info ?(opaque = false) ?hook sign n udecl b t ctx deps fixkind notations obls impls kind reduce = let obls', b = match b with @@ -689,7 +682,7 @@ let init_prog_info ?(opaque = false) ?univ_hook sign n udecl b t ctx deps fixkin prg_obligations = (obls', Array.length obls'); prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ; prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; - prg_hook = univ_hook; prg_opaque = opaque; + prg_hook = hook; prg_opaque = opaque; prg_sign = sign } let map_cardinal m = @@ -844,9 +837,9 @@ let solve_by_tac ?loc name evi t poly ctx = warn_solve_errored ?loc err; None -let obligation_terminator ?univ_hook name num guard auto pf = +let obligation_terminator ?hook name num guard auto pf = let open Proof_global in - let term = Lemmas.universe_proof_terminator ?univ_hook guard in + let term = Lemmas.standard_proof_terminator ?hook guard in match pf with | Admitted _ -> apply_terminator term pf | Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin @@ -912,7 +905,7 @@ let obligation_terminator ?univ_hook name num guard auto pf = | Proved (_, _, _ ) -> CErrors.anomaly Pp.(str "[obligation_terminator] close_proof returned more than one proof term") -let obligation_hook prg obl num auto ctx' _ gr = +let obligation_hook prg obl num auto ctx' _ _ gr = let obls, rem = prg.prg_obligations in let cst = match gr with GlobRef.ConstRef cst -> cst | _ -> assert false in let transparent = evaluable_constant cst (Global.env ()) in @@ -922,7 +915,6 @@ let obligation_hook prg obl num auto ctx' _ gr = if not transparent then err_not_transp () | _ -> () in - let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in let inst, ctx' = if not (pi2 prg.prg_kind) (* Not polymorphic *) then (* The universe context was declared globally, we continue @@ -969,11 +961,11 @@ let rec solve_obligation prg num tac = let evd = Evd.from_ctx prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in let auto n tac oblset = auto_solve_obligations n ~oblset tac in - let terminator ?univ_hook guard = + let terminator ?hook guard = Proof_global.make_terminator - (obligation_terminator ?univ_hook prg.prg_name num guard auto) in - let univ_hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in - let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~univ_hook in + (obligation_terminator ?hook prg.prg_name num guard auto) in + let hook = Lemmas.mk_hook (obligation_hook prg obl num auto) in + let () = Lemmas.start_proof ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in let _ = Pfedit.by !default_tactic in Option.iter (fun tac -> Proof_global.set_endline_tactic tac) tac @@ -1110,10 +1102,10 @@ let show_term n = let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic - ?(reduce=reduce) ?univ_hook ?(opaque = false) obls = + ?(reduce=reduce) ?hook ?(opaque = false) obls = let sign = Lemmas.initialize_named_context_for_proof () in let info = Id.print n ++ str " has type-checked" in - let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce ?univ_hook in + let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce ?hook in let obls,_ = prg.prg_obligations in if Int.equal (Array.length obls) 0 then ( Flags.if_verbose Feedback.msg_info (info ++ str "."); @@ -1130,13 +1122,13 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce) - ?univ_hook ?(opaque = false) notations fixkind = + ?hook ?(opaque = false) notations fixkind = let sign = Lemmas.initialize_named_context_for_proof () in let deps = List.map (fun (n, b, t, imps, obls) -> n) l in List.iter (fun (n, b, t, imps, obls) -> let prg = init_prog_info sign ~opaque n univdecl (Some b) t ctx deps (Some fixkind) - notations obls imps kind reduce ?univ_hook + notations obls imps kind reduce ?hook in progmap_add n (CEphemeron.create prg)) l; let _defined = List.fold_left (fun finished x -> diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 4eef668f56..c5720363b4 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -13,12 +13,6 @@ open Constr open Evd open Names -type univ_declaration_hook -val mk_univ_hook : (UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit) -> - univ_declaration_hook -val call_univ_hook : ?univ_hook:univ_declaration_hook -> ?fix_exn:Future.fix_exn -> - UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit - (* This is a hack to make it possible for Obligations to craft a Qed * behind the scenes. The fix_exn the Stm attaches to the Future proof * is not available here, so we provide a side channel to get it *) @@ -58,14 +52,19 @@ type progress = (* Resolution status of a program *) val default_tactic : unit Proofview.tactic ref -val add_definition : Names.Id.t -> ?term:constr -> types -> - UState.t -> - ?univdecl:UState.universe_decl -> (* Universe binders and constraints *) - ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list -> - ?kind:Decl_kinds.definition_kind -> - ?tactic:unit Proofview.tactic -> - ?reduce:(constr -> constr) -> - ?univ_hook:univ_declaration_hook -> ?opaque:bool -> obligation_info -> progress +val add_definition + : Names.Id.t + -> ?term:constr -> types + -> UState.t + -> ?univdecl:UState.universe_decl (* Universe binders and constraints *) + -> ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list + -> ?kind:Decl_kinds.definition_kind + -> ?tactic:unit Proofview.tactic + -> ?reduce:(constr -> constr) + -> ?hook:Lemmas.declaration_hook + -> ?opaque:bool + -> obligation_info + -> progress type notations = (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list @@ -82,7 +81,7 @@ val add_mutual_definitions : ?tactic:unit Proofview.tactic -> ?kind:Decl_kinds.definition_kind -> ?reduce:(constr -> constr) -> - ?univ_hook:univ_declaration_hook -> ?opaque:bool -> + ?hook:Lemmas.declaration_hook -> ?opaque:bool -> notations -> fixpoint_kind -> unit diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index d511bcd4fd..11b64a5247 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -542,7 +542,7 @@ let vernac_definition_hook p = function | Coercion -> Some (Class.add_coercion_hook p) | CanonicalStructure -> - Some (Lemmas.mk_hook (fun _ -> Recordops.declare_canonical_structure)) + Some (Lemmas.mk_hook (fun _ _ _ -> Recordops.declare_canonical_structure)) | SubClass -> Some (Class.add_subclass_hook p) | _ -> None |