diff options
40 files changed, 115 insertions, 78 deletions
diff --git a/.gitignore b/.gitignore index 582a8f43c7..0ab6e25852 100644 --- a/.gitignore +++ b/.gitignore @@ -101,7 +101,7 @@ doc/faq/axioms.pdf_t doc/faq/axioms.png doc/sphinx/index.rst doc/sphinx/zebibliography.rst -doc/sphinx/credits-wrapper.rst +doc/sphinx/credits.rst doc/stdlib/Library.out doc/stdlib/Library.ps doc/stdlib/Library.coqdoc.tex diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index cf9be860f9..a6b17fd148 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -9,7 +9,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2018-09-23-V01" + CACHEKEY: "bionic_coq-V2018-09-24-V01" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -112,7 +112,7 @@ after_script: - not-a-real-job script: - SPHINXENV='COQBIN="'"$PWD"'/_install_ci/bin/" COQBOOT=no' - - make -j "$NJOBS" SPHINXENV="$SPHINXENV" SPHINX_DEPS= sphinx + - make -j "$NJOBS" SPHINXENV="$SPHINXENV" SPHINX_DEPS= refman - make install-doc-sphinx artifacts: name: "$CI_JOB_NAME" @@ -288,13 +288,12 @@ doc:ml-api:ocamldoc: - dev/ocamldoc doc:ml-api:odoc: - <<: *dune-template stage: test dependencies: - build:egde:dune:dev + script: make -f Makefile.dune apidoc variables: OPAM_SWITCH: edge - DUNE_TARGET: apidoc artifacts: name: "$CI_JOB_NAME" paths: @@ -96,6 +96,7 @@ Standard Library want). - Added `Ndigits.N2Bv_sized`, and proved some lemmas about it. + Deprecated `Ndigits.N2Bv_gen`. - The scopes `int_scope` and `uint_scope` have been renamed to `dec_int_scope` and `dec_uint_scope`, to clash less with ssreflect diff --git a/Makefile.doc b/Makefile.doc index 788e4e61e7..db52607612 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -50,32 +50,35 @@ DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex ###################################################################### .PHONY: doc doc-html doc-pdf doc-ps -.PHONY: stdlib full-stdlib +.PHONY: stdlib full-stdlib sphinx -doc: sphinx stdlib +doc: refman stdlib ifndef QUICK SPHINX_DEPS := coq endif -# sphinx-html and sphinx-latex -sphinx-%: $(SPHINX_DEPS) +# refman-html and refman-latex +refman-%: $(SPHINX_DEPS) $(SHOW)'SPHINXBUILD doc/sphinx ($*)' $(HIDE)$(SPHINXENV) $(SPHINXBUILD) -b $* \ $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/$* -sphinx-pdf: sphinx-latex +refman-pdf: refman-latex +$(MAKE) -C $(SPHINXBUILDDIR)/latex -sphinx: $(SPHINX_DEPS) - +$(MAKE) sphinx-html - +$(MAKE) sphinx-pdf +refman: $(SPHINX_DEPS) + +$(MAKE) refman-html + +$(MAKE) refman-pdf + +# compatibility alias +sphinx: refman-html doc-html:\ - doc/stdlib/html/index.html sphinx-html + doc/stdlib/html/index.html refman-html doc-pdf:\ - doc/stdlib/Library.pdf sphinx-pdf + doc/stdlib/Library.pdf refman-pdf doc-ps:\ doc/stdlib/Library.ps @@ -188,7 +191,7 @@ install-doc-meta: $(MKDIR) $(FULLDOCDIR) $(INSTALLLIB) doc/LICENSE $(FULLDOCDIR)/LICENSE.doc -install-doc-html: install-doc-stdlib-html install-doc-sphinx-html +install-doc-html: install-doc-stdlib-html install-doc-sphinx install-doc-stdlib-html: $(MKDIR) $(FULLDOCDIR)/html/stdlib @@ -199,7 +202,7 @@ install-doc-printable: $(INSTALLLIB) doc/stdlib/Library.pdf $(FULLDOCDIR)/pdf $(INSTALLLIB) doc/stdlib/Library.ps $(FULLDOCDIR)/ps -install-doc-sphinx-html: +install-doc-sphinx: $(MKDIR) $(FULLDOCDIR)/sphinx (for f in `cd doc/sphinx/_build; find . -type f`; do \ $(MKDIR) $$(dirname $(FULLDOCDIR)/sphinx/$$f);\ diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index b04161918e..8d0f69626e 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-09-23-V01" +# CACHEKEY: "bionic_coq-V2018-09-24-V01" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -38,7 +38,7 @@ ENV COMPILER="4.02.3" # `num` does not have a version number as the right version to install varies # with the compiler version. ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8" \ - CI_OPAM="menhir.20180530 elpi.1.0.5 ocamlgraph.1.8.8" + CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. ENV CAMLP5_VER="6.14" \ diff --git a/dev/ci/user-overlays/08552-gares-elpi-11.sh b/dev/ci/user-overlays/08552-gares-elpi-11.sh new file mode 100644 index 0000000000..c08f44fc50 --- /dev/null +++ b/dev/ci/user-overlays/08552-gares-elpi-11.sh @@ -0,0 +1,5 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "8552" ] || [ "$CI_BRANCH" = "elpi-1.1" ]; then + Elpi_CI_REF=coq-master-elpi-1.1 +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 1eea2443fe..4f3d793ed4 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -219,7 +219,7 @@ General deprecation Proof engine - Due to the introduction of `EConstr` in 8.7, it is not necessary to +- Due to the introduction of `EConstr` in 8.7, it is not necessary to track "goal evar normal form status" anymore, thus the type `'a Proofview.Goal.t` loses its ghost argument. This may introduce some minor incompatibilities at the typing level. Code-wise, things diff --git a/doc/README.md b/doc/README.md index 1461fa2e2c..3db1261656 100644 --- a/doc/README.md +++ b/doc/README.md @@ -88,8 +88,11 @@ Alternatively, you can use some specific targets: - `make doc-html` to produce all HTML documents -- `make sphinx` - to produce the HTML and PDF versions of the reference manual +- `make refman` + to produce the HTML and PDF versions of the reference manual + +- `make refman-{html,pdf}` + to produce only one format of the reference manual - `make stdlib` to produce all formats of the Coq standard library @@ -103,12 +106,12 @@ to avoid treating Sphinx warnings as errors. Otherwise, Sphinx quits upon detecting the first warning. You can set this on the Sphinx `make` command line or as an environment variable: -- `make sphinx SPHINXWARNERROR=0` +- `make refman SPHINXWARNERROR=0` - ~~~ export SPHINXWARNERROR=0 ⋮ - make sphinx + make refman ~~~ Installation diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 904945a58d..4ad952bdfb 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -292,7 +292,9 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo \WTEG{\forall~x:T,U}{\Prop} ``.. preamble::`` A reST directive to include a TeX file. - Mostly useful to let MathJax know about `\def`s and `\newcommand`s. + Mostly useful to let MathJax know about `\def`s and `\newcommand`s. The + contents of the TeX file are wrapped in a math environment, as MathJax + doesn't process LaTeX definitions otherwise. Usage:: diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index b43d5fb6f0..71f01cbb17 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -106,7 +106,7 @@ def setup(app): master_doc = "index" # General information about the project. -project = 'The Coq Reference Manual' +project = 'Coq' copyright = '1999-2018, Inria' author = 'The Coq Development Team' @@ -335,7 +335,7 @@ latex_additional_files = [ "_static/coqnotations.sty" ] -latex_documents = [('index', 'CoqRefMan.tex', project, author, 'manual')] +latex_documents = [('index', 'CoqRefMan.tex', 'The Coq Reference Manual', author, 'manual')] # The name of an image file (relative to this directory) to place at the top of # the title page. diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits-contents.rst index 212f0a65b0..212f0a65b0 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits-contents.rst diff --git a/doc/sphinx/credits-wrapper.latex.rst b/doc/sphinx/credits-wrapper.latex.rst deleted file mode 100644 index 9f7dd49af8..0000000000 --- a/doc/sphinx/credits-wrapper.latex.rst +++ /dev/null @@ -1,3 +0,0 @@ -.. _credits: - -.. include:: credits.rst diff --git a/doc/sphinx/credits-wrapper.html.rst b/doc/sphinx/credits.html.rst index 2d35a12dc2..0b2b1c6ad1 100644 --- a/doc/sphinx/credits-wrapper.html.rst +++ b/doc/sphinx/credits.html.rst @@ -4,4 +4,4 @@ Credits ------- -.. include:: credits.rst +.. include:: credits-contents.rst diff --git a/doc/sphinx/credits.latex.rst b/doc/sphinx/credits.latex.rst new file mode 100644 index 0000000000..39101f9d52 --- /dev/null +++ b/doc/sphinx/credits.latex.rst @@ -0,0 +1,3 @@ +.. _credits: + +.. include:: credits-contents.rst diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst index 9d90857061..cf12b57414 100644 --- a/doc/sphinx/index.html.rst +++ b/doc/sphinx/index.html.rst @@ -1,11 +1,8 @@ -========================== - The Coq Reference Manual -========================== - .. _introduction: +========================== Introduction ------------- +========================== .. include:: introduction.rst @@ -28,7 +25,7 @@ Table of contents :caption: Preamble self - credits-wrapper + credits .. toctree:: :caption: The language @@ -89,3 +86,8 @@ License ------- .. include:: license.rst + +.. [#PG] Proof-General is available at https://proofgeneral.github.io/. + Optionally, you can enhance it with the minor mode + Company-Coq :cite:`Pit16` + (see https://github.com/cpitclaudel/company-coq). diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst index 0f2f7b4897..af757f8746 100644 --- a/doc/sphinx/index.latex.rst +++ b/doc/sphinx/index.latex.rst @@ -7,10 +7,15 @@ Introduction .. include:: introduction.rst +.. [#PG] Proof-General is available at https://proofgeneral.github.io/. + Optionally, you can enhance it with the minor mode + Company-Coq :cite:`Pit16` + (see https://github.com/cpitclaudel/company-coq). + Credits ------- -.. include:: credits-wrapper.rst +.. include:: credits.rst License ------- diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index b8d2f6b6dc..5bb7bf542c 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -35,11 +35,6 @@ are processed from a file. The `coqtop` read-eval-print-loop can also be used directly, for debugging purposes. - .. [#PG] Proof-General is available at https://proofgeneral.github.io/. - Optionally, you can enhance it with the minor mode - Company-Coq :cite:`Pit16` - (see https://github.com/cpitclaudel/company-coq). - - The compiled mode acts as a proof checker taking a file containing a whole development in order to ensure its correctness. Moreover, |Coq|’s compiler provides an output file containing a compact diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 97dabbf815..edf4e6ec9d 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -666,7 +666,9 @@ class ExampleDirective(BaseAdmonition): class PreambleDirective(Directive): r"""A reST directive to include a TeX file. - Mostly useful to let MathJax know about `\def`s and `\newcommand`s. + Mostly useful to let MathJax know about `\def`s and `\newcommand`s. The + contents of the TeX file are wrapped in a math environment, as MathJax + doesn't process LaTeX definitions otherwise. Usage:: @@ -693,7 +695,7 @@ class PreambleDirective(Directive): with open(abs_fname, encoding="utf-8") as ltx: latex = ltx.read() - node = make_math_node(latex, env.docname, nowrap=True) + node = make_math_node(latex, env.docname, nowrap=False) node['classes'] = ["math-preamble"] set_source_info(self, node) return [node] diff --git a/engine/ftactic.ml b/engine/ftactic.ml index e23a03c0c7..b371884ba4 100644 --- a/engine/ftactic.ml +++ b/engine/ftactic.ml @@ -61,7 +61,7 @@ let nf_enter f = (fun gl -> gl >>= fun gl -> Proofview.Goal.normalize gl >>= fun nfgl -> - Proofview.V82.wrap_exceptions (fun () -> f nfgl)) + Proofview.V82.wrap_exceptions (fun () -> f nfgl)) [@warning "-3"] let enter f = bind goals diff --git a/engine/ftactic.mli b/engine/ftactic.mli index 6c389b2d67..3c4fa6f4e8 100644 --- a/engine/ftactic.mli +++ b/engine/ftactic.mli @@ -42,6 +42,8 @@ val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic (** {5 Focussing} *) val nf_enter : (Proofview.Goal.t -> 'a t) -> 'a t +[@@ocaml.deprecated "Normalization is enforced by EConstr, please use [enter]"] + (** Enter a goal. The resulting tactic is focussed. *) val enter : (Proofview.Goal.t -> 'a t) -> 'a t diff --git a/engine/proofview.mli b/engine/proofview.mli index a9666e4f90..0bb3229a9b 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -497,6 +497,7 @@ module Goal : sig (** Normalises the argument goal. *) val normalize : t -> t tactic + [@@ocaml.deprecated "Normalization is enforced by EConstr, [normalize] is not needed anymore"] (** [concl], [hyps], [env] and [sigma] given a goal [gl] return respectively the conclusion of [gl], the hypotheses of [gl], the @@ -514,6 +515,7 @@ module Goal : sig the current goal is also given as an argument to [t]. The goal is normalised with respect to evars. *) val nf_enter : (t -> unit tactic) -> unit tactic + [@@ocaml.deprecated "Normalization is enforced by EConstr, please use [enter]"] (** Like {!nf_enter}, but does not normalize the goal beforehand. *) val enter : (t -> unit tactic) -> unit tactic diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index c2bc8c079c..b0f97c59b8 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -224,7 +224,7 @@ module Btauto = struct Tacticals.tclFAIL 0 msg gl let try_unification env = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let eq = Lazy.force eq in let concl = EConstr.Unsafe.to_constr concl in @@ -240,7 +240,7 @@ module Btauto = struct end let tac = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let concl = EConstr.Unsafe.to_constr concl in let sigma = Tacmach.New.project gl in diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index b13580bc03..3ae777cc9a 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -34,7 +34,7 @@ type lseqtac= GlobRef.t -> seqtac type 'a with_backtracking = tactic -> 'a let wrap n b continue seq = - Proofview.Goal.nf_enter begin fun gls -> + Proofview.Goal.enter begin fun gls -> Control.check_for_interrupt (); let nc = Proofview.Goal.hyps gls in let env=pf_env gls in diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 73490a2dfd..b0277e9cc2 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -99,7 +99,7 @@ let let_evar name typ = let hget_evar n = let open EConstr in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in let evl = evar_list sigma concl in diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index d42876e23e..ba3fa6fa0d 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -781,9 +781,9 @@ END (**********************************************************************) TACTIC EXTEND transparent_abstract -| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.nf_enter begin fun gl -> +| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.enter begin fun gl -> Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end ] -| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.nf_enter begin fun gl -> +| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.enter begin fun gl -> Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end ] END diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 414173ca79..67ffae59cc 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1469,7 +1469,7 @@ and interp_genarg ist x : Val.t Ftactic.t = independently of goals. *) and interp_genarg_constr_list ist x = - Ftactic.nf_enter begin fun gl -> + Ftactic.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let lc = Genarg.out_gen (glbwit (wit_list wit_constr)) x in @@ -1601,7 +1601,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacMutualFix (id,n,l) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual fix>") begin - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = pf_env gl in let f sigma (id,n,c) = let (sigma,c_interp) = interp_type ist env sigma c in @@ -1616,7 +1616,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacMutualCofix (id,l) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual cofix>") begin - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = pf_env gl in let f sigma (id,c) = let (sigma,c_interp) = interp_type ist env sigma c in @@ -1696,7 +1696,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacInductionDestruct (isrec,ev,(l,el)) -> (* spiwack: some unknown part of destruct needs the goal to be prenormalised. *) - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let sigma,l = @@ -1723,7 +1723,7 @@ and interp_atomic ist tac : unit Proofview.tactic = (* Conversion *) | TacReduce (r,cl) -> - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let (sigma,r_interp) = interp_red_expr ist (pf_env gl) (project gl) r in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl)) diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 105b5c59ae..48d677a864 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -58,7 +58,7 @@ let db_pr_goal gl = str" " ++ pc) ++ fnl () let db_pr_goal = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let pg = db_pr_goal gl in Proofview.tclLIFT (msg_tac_notice (str "Goal:" ++ fnl () ++ pg)) end diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index f22147f8b0..e0a369ca5f 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1456,7 +1456,7 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in let vm = dump_varmap (spec.typ) (vm_of_list env) in (* todo : directly generate the proof term - or generalize before conversion? *) - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> Tacticals.New.tclTHENLIST [ Tactics.change_concl @@ -1709,7 +1709,7 @@ let micromega_gen (normalise:'cst atom -> 'cst mc_cnf) unsat deduce spec dumpexpr prover tac = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let concl = Tacmach.New.pf_concl gl in let hyps = Tacmach.New.pf_hyps_types gl in @@ -1787,7 +1787,7 @@ let micromega_order_changer cert env ff = let formula_typ = (EConstr.mkApp (Lazy.force coq_Cstr,[| coeff|])) in let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in let vm = dump_varmap (typ) (vm_of_list env) in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> Tacticals.New.tclTHENLIST [ (Tactics.change_concl @@ -1817,7 +1817,7 @@ let micromega_genr prover tac = proof_typ = Lazy.force coq_QWitness ; dump_proof = dump_psatz coq_Q dump_q } in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let concl = Tacmach.New.pf_concl gl in let hyps = Tacmach.New.pf_hyps_types gl in diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index e14c4e2ec1..abae6940fa 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -588,7 +588,7 @@ let abstract_path sigma typ path t = let focused_simpl path = let open Tacmach.New in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let newc = context (project gl) (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in convert_concl_no_check newc DEFAULTcast end @@ -656,7 +656,7 @@ let new_hole env sigma c = let clever_rewrite_base_poly typ p result theorem = let open Tacmach.New in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let full = pf_concl gl in let env = pf_env gl in let (abstracted,occ) = abstract_path (project gl) typ (List.rev p) full in @@ -708,7 +708,7 @@ let refine_app gl t = let clever_rewrite p vpath t = let open Tacmach.New in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let full = pf_concl gl in let (abstracted,occ) = abstract_path (project gl) (Lazy.force coq_Z) (List.rev p) full in let vargs = List.map (fun p -> occurrence (project gl) p occ) vpath in @@ -1763,7 +1763,7 @@ let onClearedName id tac = (* so renaming may be necessary *) tclTHEN (tclTRY (clear [id])) - (Proofview.Goal.nf_enter begin fun gl -> + (Proofview.Goal.enter begin fun gl -> let id = fresh_id Id.Set.empty id gl in tclTHEN (introduction id) (tac id) end) @@ -1771,7 +1771,7 @@ let onClearedName id tac = let onClearedName2 id tac = tclTHEN (tclTRY (clear [id])) - (Proofview.Goal.nf_enter begin fun gl -> + (Proofview.Goal.enter begin fun gl -> let id1 = fresh_id Id.Set.empty (add_suffix id "_left") gl in let id2 = fresh_id Id.Set.empty (add_suffix id "_right") gl in tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] @@ -1956,7 +1956,7 @@ let destructure_goal = try let dec = decidability t in tclTHEN - (Proofview.Goal.nf_enter begin fun gl -> + (Proofview.Goal.enter begin fun gl -> refine_app gl (mkApp (Lazy.force coq_dec_not_not, [| t; dec |])) end) intro diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index e603480656..930048400a 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -1049,7 +1049,7 @@ let resolution unsafe sigma env (reified_concl,reified_hyps) systems_list = Tactics.apply (Lazy.force coq_I) let total_reflexive_omega_tactic unsafe = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> Coqlib.check_required_library ["Coq";"romega";"ROmega"]; rst_omega_eq (); rst_omega_var (); diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 1f3c758e5c..f2f236f448 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1088,7 +1088,7 @@ let () = CLexer.set_keyword_state frozen_lexer ;; (** Basic tactics *) -let rec fst_prod red tac = Proofview.Goal.nf_enter begin fun gl -> +let rec fst_prod red tac = Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in match EConstr.kind (Proofview.Goal.sigma gl) concl with | Prod (id,_,tgt) | LetIn(id,_,_,tgt) -> tac id diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 8b9c94f2db..a7aae5bd31 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -1949,7 +1949,7 @@ ARGUMENT EXTEND ssrexactarg TYPED AS ssrapplyarg PRINTED BY pr_ssraarg END let vmexacttac pf = - Goal.nf_enter begin fun gl -> + Goal.enter begin fun gl -> exact_no_check (EConstr.mkCast (pf, _vmcast, Tacmach.New.pf_concl gl)) end diff --git a/stm/stm.ml b/stm/stm.ml index 635bf9bf31..b7ba163309 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2009,7 +2009,7 @@ end = struct (* {{{ *) 1 goals in TaskQueue.join queue; let assign_tac : unit Proofview.tactic = - Proofview.(Goal.nf_enter begin fun g -> + Proofview.(Goal.enter begin fun g -> let gid = Goal.goal g in let f = try List.assoc gid res @@ -2301,7 +2301,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = | `Leaks -> Exninfo.iraise exn | `ValidBlock { base_state; goals_to_admit; recovery_command } -> begin let tac = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> if CList.mem_f Evar.equal (Proofview.Goal.goal gl) goals_to_admit then Proofview.give_up else Proofview.tclUNIT () diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index c8fd0b7a75..8e296de617 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -162,7 +162,7 @@ let gen_auto_multi_rewrite conds tac_main lbas cl = | None -> (* try to rewrite in all hypothesis (except maybe the rewritten one) *) - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let ids = Tacmach.New.pf_ids_of_hyps gl in try_do_hyps (fun id -> id) ids end) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 9c5fdcd1ce..3456d13bbe 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -416,7 +416,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm if get_typeclasses_filtered_unification () then let tac = matches_pattern concl p <*> - Proofview.Goal.nf_enter + Proofview.Goal.enter (fun gl -> unify_resolve_refine poly flags gl (c,None,clenv)) in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable else diff --git a/tactics/equality.ml b/tactics/equality.ml index 0e39215701..d0f4b2c680 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -249,7 +249,7 @@ let rewrite_elim with_evars frzevars cls c e = let tclNOTSAMEGOAL tac = let goal gl = Proofview.Goal.goal gl in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = project gl in let ev = goal gl in tac >>= fun () -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 95d545b046..6999b17d8e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2824,7 +2824,7 @@ let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) = let generalize_dep ?(with_let=false) c = let open Tacmach.New in let open Tacticals.New in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = pf_env gl in let sign = Proofview.Goal.hyps gl in let sigma = project gl in diff --git a/test-suite/bugs/closed/8532.v b/test-suite/bugs/closed/8532.v new file mode 100644 index 0000000000..00aa66e701 --- /dev/null +++ b/test-suite/bugs/closed/8532.v @@ -0,0 +1,8 @@ +(* Checking Print Assumptions relatively to a bound module *) + +Module Type Typ. + Parameter Inline(10) t : Type. +End Typ. +Module Terms_mod (SetVars : Typ). +Print Assumptions SetVars.t. +End Terms_mod. diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index 68a98e4292..a2a2430e91 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -578,6 +578,7 @@ Qed. (** To state nonetheless a second result about composition of conversions, we define a conversion on a given number of bits : *) +#[deprecated(since = "8.9.0", note = "Use N2Bv_sized instead.")] Fixpoint N2Bv_gen (n:nat)(a:N) : Bvector n := match n return Bvector n with | 0 => Bnil @@ -705,3 +706,10 @@ Proof with simpl; auto. destruct (Bv2N n v) as [|[]]; rewrite <- IHv... Qed. + +Lemma N2Bv_N2Bv_sized_above (a : N) (k : nat) : + N2Bv_sized (N.size_nat a + k) a = N2Bv a ++ Bvect_false k. +Proof with auto. + destruct a... + induction p; simpl; f_equal... +Qed. diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 0bcd3c64eb..b000745961 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -71,7 +71,7 @@ let rec fields_of_functor f subs mp0 args = function let rec lookup_module_in_impl mp = match mp with | MPfile _ -> Global.lookup_module mp - | MPbound _ -> assert false + | MPbound _ -> Global.lookup_module mp | MPdot (mp',lab') -> if ModPath.equal mp' (Global.current_modpath ()) then Global.lookup_module mp |