diff options
83 files changed, 520 insertions, 498 deletions
diff --git a/dev/ci/user-overlays/13512-herbelin-master+fix13413-apply-on-intro-pattern-fresh-names.sh b/dev/ci/user-overlays/13512-herbelin-master+fix13413-apply-on-intro-pattern-fresh-names.sh new file mode 100644 index 0000000000..4c8cdbbb45 --- /dev/null +++ b/dev/ci/user-overlays/13512-herbelin-master+fix13413-apply-on-intro-pattern-fresh-names.sh @@ -0,0 +1,5 @@ +if [ "$CI_PULL_REQUEST" = "13415" ] || [ "$CI_BRANCH" = "intern-univs" ]; then + + overlay perennial https://github.com/herbelin/perennial master+adapt13512-fresness-names-apply-in-introduction-pattern + +fi diff --git a/dev/ci/user-overlays/13725-SkySkimmer-hint-rw-local.sh b/dev/ci/user-overlays/13725-SkySkimmer-hint-rw-local.sh new file mode 100644 index 0000000000..69bd038b78 --- /dev/null +++ b/dev/ci/user-overlays/13725-SkySkimmer-hint-rw-local.sh @@ -0,0 +1 @@ +overlay equations https://github.com/SkySkimmer/Coq-Equations hint-rw-local 13725 diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index 19562b60a2..894244044a 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -144,6 +144,7 @@ in time. together with its SHA256 hash in a signed e-mail to `dsi.securite` @ `inria.fr` putting `@maximedenes` in carbon copy. + The MacOS packages should be signed with our own certificate. A detailed step-by-step guide can be found [on the wiki](https://github.com/coq/coq/wiki/SigningReleases). +- [ ] Upload the PDF version of the reference manual to the GitHub release. (*TODO:* automate this.) - [ ] Prepare a page of news on the website with the link to the GitHub release (see [coq/www#63](https://github.com/coq/www/pull/63)). - [ ] Merge the website update, publish the release diff --git a/doc/changelog/04-tactics/13512-master+fix13413-apply-on-intro-pattern-fresh-names.rst b/doc/changelog/04-tactics/13512-master+fix13413-apply-on-intro-pattern-fresh-names.rst new file mode 100644 index 0000000000..aaacb2aadf --- /dev/null +++ b/doc/changelog/04-tactics/13512-master+fix13413-apply-on-intro-pattern-fresh-names.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Possible collision between a user-level name and an internal name when + using the :n:`%` introduction pattern + (`#13512 <https://github.com/coq/coq/pull/13512>`_, + fixes `#13413 <https://github.com/coq/coq/issues/13413>`_, + by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/13699-fix13579.rst b/doc/changelog/04-tactics/13699-fix13579.rst new file mode 100644 index 0000000000..9cf62fb595 --- /dev/null +++ b/doc/changelog/04-tactics/13699-fix13579.rst @@ -0,0 +1,6 @@ +- **Fixed:** + :tacn:`simpl` and :tacn:`hnf` now reduce primitive functions + on primitive integers, floats and arrays + (`#13699 <https://github.com/coq/coq/pull/13699>`_, + fixes `#13579 <https://github.com/coq/coq/issues/13579>`_, + by Pierre Roux). diff --git a/doc/changelog/04-tactics/13761-remove_convert_concl_nc.rst b/doc/changelog/04-tactics/13761-remove_convert_concl_nc.rst new file mode 100644 index 0000000000..1aa57ff8b1 --- /dev/null +++ b/doc/changelog/04-tactics/13761-remove_convert_concl_nc.rst @@ -0,0 +1,4 @@ +- **Removed:** + convert_concl_no_check. Use :tacn:`change_no_check` instead + (`#13761 <https://github.com/coq/coq/pull/13761>`_, + by Jim Fehrle). diff --git a/doc/changelog/04-tactics/13762-remove_double_induction.rst b/doc/changelog/04-tactics/13762-remove_double_induction.rst new file mode 100644 index 0000000000..4ea54a1ab6 --- /dev/null +++ b/doc/changelog/04-tactics/13762-remove_double_induction.rst @@ -0,0 +1,9 @@ +- **Removed:** + double induction tactic. Replace :n:`double induction @ident @ident` + with :n:`induction @ident; induction @ident` (or + :n:`induction @ident ; destruct @ident` depending on the exact needs). + Replace :n:`double induction @natural__1 @natural__2` with + :n:`induction @natural__1; induction natural__3` where :n:`natural__3` is the result + of :n:`natural__2 - natural__1` + (`#13762 <https://github.com/coq/coq/pull/13762>`_, + by Jim Fehrle). diff --git a/doc/changelog/07-vernac-commands-and-options/13725-hint-rw-local.rst b/doc/changelog/07-vernac-commands-and-options/13725-hint-rw-local.rst new file mode 100644 index 0000000000..653e9cd0cd --- /dev/null +++ b/doc/changelog/07-vernac-commands-and-options/13725-hint-rw-local.rst @@ -0,0 +1,5 @@ +- **Changed:** + :cmd:`Hint Rewrite` now supports locality attributes (including :attr:`export`) like other :ref:`Hint <creating_hints>` commands + (`#13725 <https://github.com/coq/coq/pull/13725>`_, + fixes `#13724 <https://github.com/coq/coq/issues/13724>`_, + by Gaëtan Gilbert). diff --git a/doc/changelog/07-vernac-commands-and-options/13764-remove_add_injtyp.rst b/doc/changelog/07-vernac-commands-and-options/13764-remove_add_injtyp.rst new file mode 100644 index 0000000000..fc6c88eab6 --- /dev/null +++ b/doc/changelog/07-vernac-commands-and-options/13764-remove_add_injtyp.rst @@ -0,0 +1,6 @@ +- **Removed:** + `Show Zify Spec`, `Add InjTyp` and 11 similar `Add *` commands. + For `Show Zify Spec`, use `Show Zify UnOpSpec` or `Show Zify BinOpSpec` instead. + For `Add *`, `Use Add Zify *` intead of `Add *` + (`#13764 <https://github.com/coq/coq/pull/13764>`_, + by Jim Fehrle). diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 38c4886e0f..3bd85d29c8 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -315,68 +315,6 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. prints the list of types that supported by :tacn:`zify` i.e., :g:`Z`, :g:`nat`, :g:`positive` and :g:`N`. -.. cmd:: Show Zify Spec - - .. deprecated:: 8.13 - Use :cmd:`Show Zify` ``UnOpSpec`` or :cmd:`Show Zify` ``BinOpSpec`` instead. - -.. cmd:: Add InjTyp @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``InjTyp`` instead. - -.. cmd:: Add BinOp @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``BinOp`` instead. - -.. cmd:: Add BinOpSpec @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``BinOpSpec`` instead. - -.. cmd:: Add UnOp @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``UnOp`` instead. - -.. cmd:: Add UnOpSpec @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``UnOpSpec`` instead. - -.. cmd:: Add CstOp @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``CstOp`` instead. - -.. cmd:: Add BinRel @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``BinRel`` instead. - -.. cmd:: Add PropOp @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``PropOp`` instead. - -.. cmd:: Add PropBinOp @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``PropBinOp`` instead. - -.. cmd:: Add PropUOp @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``PropUOp`` instead. - -.. cmd:: Add Saturate @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``Saturate`` instead. - - - .. [#csdp] Sources and binaries can be found at https://projects.coin-or.org/Csdp .. [#fnpsatz] Variants deal with equalities and strict inequalities. diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index fc40ba0249..58444e8e82 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -531,11 +531,11 @@ Commands and options .. _813HintWarning: - **Deprecated:** - The default value for hint locality is currently :attr:`local` in a section and - :attr:`global` otherwise, but is scheduled to change in a future release. For the - time being, adding hints outside of sections without specifying an explicit - locality is therefore triggering a deprecation warning. It is recommended to - use :attr:`export` whenever possible + Hint locality currently defaults to :attr:`local` in a section and + :attr:`global` otherwise, but this will change in a future release. + Hints added outside of sections without an explicit + locality now generate a deprecation warning. We recommend + using :attr:`export` where possible (`#13384 <https://github.com/coq/coq/pull/13384>`_, by Pierre-Marie Pédrot). - **Deprecated:** @@ -3191,7 +3191,7 @@ Other changes in 8.10+beta1 by Maxime Dénès, review by Pierre-Marie Pédrot). - New variant :tacn:`change_no_check` of :tacn:`change`, usable as a - documented replacement of :tacn:`convert_concl_no_check` + documented replacement of `convert_concl_no_check` (`#10012 <https://github.com/coq/coq/pull/10012>`_, `#10017 <https://github.com/coq/coq/pull/10017>`_, `#10053 <https://github.com/coq/coq/pull/10053>`_, and diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index b63ae32311..2046788ef3 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -339,7 +339,7 @@ the optional tactic of the ``Hint Rewrite`` command. .. coqtop:: in - Hint Rewrite Ack0 Ack1 Ack2 : base0. + Global Hint Rewrite Ack0 Ack1 Ack2 : base0. .. coqtop:: all @@ -367,7 +367,7 @@ the optional tactic of the ``Hint Rewrite`` command. .. coqtop:: in - Hint Rewrite g0 g1 g2 using lia : base1. + Global Hint Rewrite g0 g1 g2 using lia : base1. .. coqtop:: in diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 766f7ab44e..72970f46b0 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -498,10 +498,16 @@ one or more of its hypotheses. :n:`{? - } {+ @nat_or_var }` Selects the specified occurrences within a single goal or hypothesis. - Occurrences are numbered from left to right starting with 1 when the - goal is printed with the :flag:`Printing All` flag. (In particular, occurrences - in :ref:`implicit arguments <ImplicitArguments>` and - :ref:`coercions <Coercions>` are counted but not shown by default.) + Occurrences are numbered starting with 1 following a depth-first traversal + of the term's expression, including occurrences in + :ref:`implicit arguments <ImplicitArguments>` + and :ref:`coercions <Coercions>` that are not displayed by default. + (Set the :flag:`Printing All` flag to show those in the printed term.) + + For example, when matching the pattern `_ + _` in the term `(a + b) + c`, + occurrence 1 is `(...) + c` and + occurrence 2 is `(a + b)`. When matching that pattern with term `a + (b + c)`, + occurrence 1 is `a + (...)` and occurrence 2 is `b + c`. Specifying `-` includes all occurrences *except* the ones listed. @@ -2067,19 +2073,6 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) is the name given by :n:`intros until @natural` to the :n:`@natural`-th non-dependent premise of the goal. -.. tacn:: double induction @ident @ident - :name: double induction - - This tactic is deprecated and should be replaced by - :n:`induction @ident; induction @ident` (or - :n:`induction @ident ; destruct @ident` depending on the exact needs). - -.. tacv:: double induction @natural__1 @natural__2 - - This tactic is deprecated and should be replaced by - :n:`induction num1; induction num3` where :n:`num3` is the result - of :n:`num2 - num1` - .. tacn:: dependent induction @ident :name: dependent induction diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst index d7228a3907..30f7be5f13 100644 --- a/doc/sphinx/proofs/automatic-tactics/auto.rst +++ b/doc/sphinx/proofs/automatic-tactics/auto.rst @@ -273,18 +273,21 @@ Creating Hints :cmd:`Import` or :cmd:`Require` the current module. + :attr:`export` hints are visible from other modules when they :cmd:`Import` the current - module, but not when they only :cmd:`Require` it. This attribute is supported by - all `Hint` commands except for :cmd:`Hint Rewrite`. + module, but not when they only :cmd:`Require` it. + :attr:`global` hints are visible from other modules when they :cmd:`Import` or :cmd:`Require` the current module. + .. versionadded:: 8.14 + + The :cmd:`Hint Rewrite` now supports locality attributes like other `Hint` commands. + .. deprecated:: 8.13 The default value for hint locality will change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality will trigger a deprecation - warning. We recommend you use :attr:`export` whenever possible. + release. Hints added outside of sections without an explicit + locality are now deprecated. We recommend using :attr:`export` + where possible. The `Hint` commands are: diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index 8873d02888..663337bc64 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -91,7 +91,10 @@ Rewriting with Leibniz and setoid equality in the conclusion is replaced. If :n:`at @occs_nums` is specified, rewriting is always done with - :ref:`setoid rewriting <generalizedrewriting>`, even for Leibniz’s equality. + :ref:`setoid rewriting <generalizedrewriting>`, even for Leibniz’s equality, + which means that you must `Require Setoid` to use that form. + However, note that :tacn:`rewrite` (even when using setoid rewriting) and + :tacn:`setoid_rewrite` don't behave identically (as already mentioned above). :n:`by @ltac_expr3` If specified, is used to resolve all side conditions generated by the tactic. @@ -338,13 +341,6 @@ Rewriting with definitional equality exact H. Qed. - .. tacn:: convert_concl_no_check @one_term - - .. deprecated:: 8.11 - - Deprecated old name for :tacn:`change_no_check`. Does not support any of its - variants. - .. _performingcomputations: Performing computations @@ -890,10 +886,8 @@ the conversion in hypotheses :n:`{+ @ident}`. Conversion tactics applied to hypotheses ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. tacn:: @tactic in {+, @ident} - - Applies :token:`tactic` (any of the conversion tactics listed in this - section) to the hypotheses :n:`{+ @ident}`. + The form :n:`@tactic in {+, @ident }` applies :token:`tactic` (any of the + conversion tactics listed in this section) to the hypotheses :n:`{+ @ident}`. If :token:`ident` is a local definition, then :token:`ident` can be replaced by :n:`type of @ident` to address not the body but the type of the local diff --git a/interp/notation.ml b/interp/notation.ml index 33d96f0439..d6002d71b5 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1357,6 +1357,7 @@ let find_with_delimiters = function match (String.Map.find scope !scope_map).delimiters with | Some key -> Some (Some scope, Some key) | None -> None + | exception Not_found -> None let rec find_without_delimiters find (ntn_scope,ntn) = function | OpenScopeItem scope :: scopes -> diff --git a/kernel/environ.ml b/kernel/environ.ml index 6f2aeab203..63fbaa6a3b 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -571,6 +571,12 @@ let is_primitive env c = | Declarations.Primitive _ -> true | _ -> false +let get_primitive env c = + let cb = lookup_constant c env in + match cb.Declarations.const_body with + | Declarations.Primitive p -> Some p + | _ -> None + let is_int63_type env c = match env.retroknowledge.Retroknowledge.retro_int63 with | None -> false diff --git a/kernel/environ.mli b/kernel/environ.mli index dfd9173d10..414ef2b4d7 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -248,6 +248,7 @@ val constant_type_in : env -> Constant.t puniverses -> types val constant_opt_value_in : env -> Constant.t puniverses -> constr option val is_primitive : env -> Constant.t -> bool +val get_primitive : env -> Constant.t -> CPrimitives.t option val is_array_type : env -> Constant.t -> bool val is_int63_type : env -> Constant.t -> bool diff --git a/library/summary.ml b/library/summary.ml index 221ac868fa..572467ada3 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -131,28 +131,27 @@ let ref ?freeze ~name x = fst @@ ref_tag ?freeze ~name x module Local = struct -type 'a local_ref = ('a CEphemeron.key * 'a Dyn.tag) ref +type 'a local_ref = 'a CEphemeron.key ref * 'a CEphemeron.key Dyn.tag -let set r v = r := (CEphemeron.create v, snd !r) +let set (r, tag) v = r := CEphemeron.create v -let get r = - let key, name = !r in - try CEphemeron.get key +let get (key, name) = + try CEphemeron.get !key with CEphemeron.InvalidKey -> let { init_function } = DynMap.find name !sum_map in init_function (); - CEphemeron.get (fst !r) + CEphemeron.get !key -let ref ?(freeze=fun x -> x) ~name init = +let ref (type a) ~name (init : a) : a local_ref = let () = check_name (mangle name) in - let tag : 'a Dyn.tag = Dyn.create (mangle name) in - let r = pervasives_ref (CEphemeron.create init, tag) in + let tag : a CEphemeron.key Dyn.tag = Dyn.create (mangle name) in + let r = pervasives_ref (CEphemeron.create init) in let () = sum_map := DynMap.add tag - { freeze_function = (fun ~marshallable -> freeze (get r)); - unfreeze_function = (set r); - init_function = (fun () -> set r init) } !sum_map + { freeze_function = (fun ~marshallable -> !r); + unfreeze_function = (fun v -> r := v); + init_function = (fun () -> r := CEphemeron.create init) } !sum_map in - r + (r, tag) let (!) = get let (:=) = set diff --git a/library/summary.mli b/library/summary.mli index 7c5e1bee6f..a6f94a49ae 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -53,7 +53,7 @@ val ref_tag : ?freeze:(marshallable:bool -> 'a -> 'a) -> name:string -> 'a -> 'a module Local : sig type 'a local_ref - val ref : ?freeze:('a -> 'a) -> name:string -> 'a -> 'a local_ref + val ref : name:string -> 'a -> 'a local_ref val (:=) : 'a local_ref -> 'a -> unit val (!) : 'a local_ref -> 'a diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg index e39c066c95..b20c4d173d 100644 --- a/plugins/ltac/coretactics.mlg +++ b/plugins/ltac/coretactics.mlg @@ -259,13 +259,6 @@ TACTIC EXTEND simple_destruct | [ "simple" "destruct" quantified_hypothesis(h) ] -> { simple_destruct h } END -(** Double induction *) - -TACTIC EXTEND double_induction DEPRECATED { Deprecation.make () } -| [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] -> - { Elim.h_double_induction h1 h2 } -END - (* Admit *) TACTIC EXTEND admit diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 90c366ed63..d9da47134d 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -299,7 +299,7 @@ TACTIC EXTEND rewrite_star { -let add_rewrite_hint ~poly bases ort t lcsr = +let add_rewrite_hint ~locality ~poly bases ort t lcsr = let env = Global.env() in let sigma = Evd.from_env env in let f ce = @@ -315,7 +315,7 @@ let add_rewrite_hint ~poly bases ort t lcsr = in CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in let eqs = List.map f lcsr in - let add_hints base = add_rew_rules base eqs in + let add_hints base = add_rew_rules ~locality base eqs in List.iter add_hints bases let classify_hint _ = VtSideff ([], VtLater) @@ -323,15 +323,15 @@ let classify_hint _ = VtSideff ([], VtLater) } VERNAC COMMAND EXTEND HintRewrite CLASSIFIED BY { classify_hint } -| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] -> - { add_rewrite_hint ~poly:polymorphic bl o None l } -| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) +| #[ polymorphic; locality = option_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] -> + { add_rewrite_hint ~locality ~poly:polymorphic bl o None l } +| #[ polymorphic; locality = option_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ":" preident_list(bl) ] -> - { add_rewrite_hint ~poly:polymorphic bl o (Some t) l } -| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] -> - { add_rewrite_hint ~poly:polymorphic ["core"] o None l } -| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] -> - { add_rewrite_hint ~poly:polymorphic ["core"] o (Some t) l } + { add_rewrite_hint ~locality ~poly:polymorphic bl o (Some t) l } +| #[ polymorphic; locality = option_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] -> + { add_rewrite_hint ~locality ~poly:polymorphic ["core"] o None l } +| #[ polymorphic; locality = option_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] -> + { add_rewrite_hint ~locality ~poly:polymorphic ["core"] o (Some t) l } END (**********************************************************************) diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 069a342b2a..82b41e41bd 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -11,7 +11,6 @@ { open Pp -open Constr open Stdarg open Pcoq.Prim open Pcoq.Constr @@ -199,20 +198,6 @@ TACTIC EXTEND unify END { -let deprecated_convert_concl_no_check = - CWarnings.create - ~name:"convert_concl_no_check" ~category:"deprecated" - (fun () -> Pp.str "The syntax [convert_concl_no_check] is deprecated. Use [change_no_check] instead.") -} - -TACTIC EXTEND convert_concl_no_check -| ["convert_concl_no_check" constr(x) ] -> { - deprecated_convert_concl_no_check (); - Tactics.convert_concl ~check:false x DEFAULTcast - } -END - -{ let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_qualid let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global diff --git a/plugins/micromega/g_zify.mlg b/plugins/micromega/g_zify.mlg index 0e5cac2d4a..74b0708743 100644 --- a/plugins/micromega/g_zify.mlg +++ b/plugins/micromega/g_zify.mlg @@ -19,12 +19,6 @@ let warn_deprecated_Spec = (fun () -> Pp.strbrk ("Show Zify Spec is deprecated. Use either \"Show Zify BinOpSpec\" or \"Show Zify UnOpSpec\".")) -let warn_deprecated_Add = - CWarnings.create ~name:"deprecated-Zify-Add" ~category:"deprecated" - (fun () -> - Pp.strbrk ("Add <X> is deprecated. Use instead Add Zify <X>.")) - - } DECLARE PLUGIN "zify_plugin" @@ -41,17 +35,6 @@ VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF | ["Add" "Zify" "BinOpSpec" constr(t) ] -> { Zify.BinOpSpec.register t } | ["Add" "Zify" "UnOpSpec" constr(t) ] -> { Zify.UnOpSpec.register t } | ["Add" "Zify" "Saturate" constr(t) ] -> { Zify.Saturate.register t } -| ["Add" "InjTyp" constr(t) ] -> { warn_deprecated_Add (); Zify.InjTable.register t } -| ["Add" "BinOp" constr(t) ] -> { warn_deprecated_Add (); Zify.BinOp.register t } -| ["Add" "UnOp" constr(t) ] -> { warn_deprecated_Add (); Zify.UnOp.register t } -| ["Add" "CstOp" constr(t) ] -> { warn_deprecated_Add (); Zify.CstOp.register t } -| ["Add" "BinRel" constr(t) ] -> { warn_deprecated_Add (); Zify.BinRel.register t } -| ["Add" "PropOp" constr(t) ] -> { warn_deprecated_Add (); Zify.PropBinOp.register t } -| ["Add" "PropBinOp" constr(t) ] -> { warn_deprecated_Add (); Zify.PropBinOp.register t } -| ["Add" "PropUOp" constr(t) ] -> { warn_deprecated_Add (); Zify.PropUnOp.register t } -| ["Add" "BinOpSpec" constr(t) ] -> { warn_deprecated_Add (); Zify.BinOpSpec.register t } -| ["Add" "UnOpSpec" constr(t) ] -> { warn_deprecated_Add (); Zify.UnOpSpec.register t } -| ["Add" "Saturate" constr(t) ] -> { warn_deprecated_Add (); Zify.Saturate.register t } END TACTIC EXTEND ITER @@ -73,7 +56,4 @@ VERNAC COMMAND EXTEND ZifyPrint CLASSIFIED AS SIDEFF |[ "Show" "Zify" "BinRel"] -> { Zify.BinRel.print () } |[ "Show" "Zify" "UnOpSpec"] -> { Zify.UnOpSpec.print() } |[ "Show" "Zify" "BinOpSpec"] -> { Zify.BinOpSpec.print() } -|[ "Show" "Zify" "Spec"] -> { - warn_deprecated_Spec () ; - Zify.UnOpSpec.print() ; Zify.BinOpSpec.print ()} END diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 3da75f67b9..54a47a252d 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -468,23 +468,6 @@ let safe_meta_value sigma ev = try Some (Evd.meta_value sigma ev) with Not_found -> None -let strong_with_flags whdfun flags env sigma t = - let push_rel_check_zeta d env = - let open CClosure.RedFlags in - let d = match d with - | LocalDef (na,c,t) when not (red_set flags fZETA) -> LocalAssum (na,t) - | d -> d in - push_rel d env in - let rec strongrec env t = - map_constr_with_full_binders env sigma - push_rel_check_zeta strongrec env (whdfun flags env sigma t) in - strongrec env t - -let strong whdfun env sigma t = - let rec strongrec env t = - map_constr_with_full_binders env sigma push_rel strongrec env (whdfun env sigma t) in - strongrec env t - (*************************************) (*** Reduction using bindingss ***) (*************************************) @@ -978,6 +961,9 @@ let whd_betalet = red_of_state_red whd_betalet_state (* 2. Delta Reduction Functions *) +let whd_const_state c e = raw_whd_state_gen CClosure.RedFlags.(mkflags [fCONST c]) e +let whd_const c = red_of_state_red (whd_const_state c) + let whd_delta_state e = raw_whd_state_gen CClosure.delta e let whd_delta_stack = stack_red_of_state_red whd_delta_state let whd_delta = red_of_state_red whd_delta_state @@ -1281,7 +1267,9 @@ let plain_instance sigma s c = match s with let instance env sigma s c = (* if s = [] then c else *) - strong whd_betaiota env sigma (plain_instance sigma s c) + (* No need to compute contexts under binders as whd_betaiota is local *) + let rec strongrec t = EConstr.map sigma strongrec (whd_betaiota env sigma t) in + strongrec (plain_instance sigma s c) (* pseudo-reduction rule: * [hnf_prod_app env s (Prod(_,B)) N --> B[N] diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 59bc4a8b72..41d16f1c3c 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -143,13 +143,6 @@ type e_reduction_function = env -> evar_map -> constr -> evar_map * constr type stack_reduction_function = env -> evar_map -> constr -> constr * constr list -(** {6 Reduction Function Operators } *) - -val strong_with_flags : - (CClosure.RedFlags.reds -> reduction_function) -> - (CClosure.RedFlags.reds -> reduction_function) -val strong : reduction_function -> reduction_function - (** {6 Generic Optimized Reduction Function using Closures } *) val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function @@ -185,6 +178,7 @@ val whd_betalet_stack : stack_reduction_function (** {6 Head normal forms } *) +val whd_const : Constant.t -> reduction_function val whd_delta_stack : stack_reduction_function val whd_delta : reduction_function val whd_betadeltazeta_stack : stack_reduction_function diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 01819a650b..a103699716 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -68,8 +68,7 @@ let error_not_evaluable r = spc () ++ str "to an evaluable reference.") let is_evaluable_const env cst = - is_transparent env (ConstKey cst) && - (evaluable_constant cst env || is_primitive env cst) + is_transparent env (ConstKey cst) && evaluable_constant cst env let is_evaluable_var env id = is_transparent env (VarKey id) && evaluable_named id env @@ -163,6 +162,10 @@ let reference_value env sigma c u = | None -> raise NotEvaluable | Some d -> d +let is_primitive_val sigma c = match EConstr.kind sigma c with + | Int _ | Float _ | Array _ -> true + | _ -> false + (************************************************************************) (* Reduction of constants hiding a fixpoint (e.g. for "simpl" tactic). *) (* One reuses the name of the function after reduction of the fixpoint *) @@ -714,7 +717,8 @@ and reduce_params env sigma stack l = let arg = List.nth stack i in let rarg = whd_construct_stack env sigma arg in match EConstr.kind sigma (fst rarg) with - | Construct _ -> List.assign stack i (applist rarg) + | Construct _ | Int _ | Float _ | Array _ -> + List.assign stack i (applist rarg) | _ -> raise Redelimination) stack l @@ -770,6 +774,16 @@ and whd_simpl_stack env sigma = else s' with Redelimination -> s') + | Const (cst, _) when is_primitive env cst -> + (try + let args = + List.map_filter_i (fun i a -> + match a with CPrimitives.Kwhnf -> Some i | _ -> None) + (CPrimitives.kind (Option.get (get_primitive env cst))) in + let stack = reduce_params env sigma stack args in + whd_const cst env sigma (applist (x, stack)), [] + with Redelimination -> s') + | _ -> match match_eval_ref env sigma x stack with | Some (ref, u) -> @@ -880,11 +894,11 @@ and special_red_case env sigma (ci, u, pms, p, iv, c, lf) = in redrec (push_app sigma (c, [])) -(* reduce until finding an applied constructor or fail *) +(* reduce until finding an applied constructor (or primitive value) or fail *) and whd_construct_stack env sigma s = let (constr, cargs as s') = whd_simpl_stack env sigma (s, []) in - if reducible_mind_case sigma constr then s' + if reducible_mind_case sigma constr || is_primitive_val sigma constr then s' else match match_eval_ref env sigma constr cargs with | Some (ref, u) -> (match reference_opt_value env sigma ref u with @@ -1040,7 +1054,10 @@ let hnf_constr env sigma c = whd_simpl_orelse_delta_but_fix env sigma (c, []) let whd_simpl env sigma c = applist (whd_simpl_stack env sigma (c, [])) -let simpl env sigma c = strong whd_simpl env sigma c +let simpl env sigma c = + let rec strongrec env t = + map_constr_with_full_binders env sigma push_rel strongrec env (whd_simpl env sigma t) in + strongrec env c (* Reduction at specific subterms *) diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index cc56de066d..1d876537ef 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -206,9 +206,15 @@ let subst_hintrewrite (subst,(rbase,list as node)) = (rbase,list') (* Declaration of the Hint Rewrite library object *) -let inHintRewrite : string * HintDN.t -> Libobject.obj = +let inGlobalHintRewrite : string * HintDN.t -> Libobject.obj = let open Libobject in - declare_object @@ superglobal_object_nodischarge "HINT_REWRITE" + declare_object @@ superglobal_object_nodischarge "HINT_REWRITE_GLOBAL" + ~cache:cache_hintrewrite + ~subst:(Some subst_hintrewrite) + +let inExportHintRewrite : string * HintDN.t -> Libobject.obj = + let open Libobject in + declare_object @@ global_object_nodischarge "HINT_REWRITE_EXPORT" ~cache:cache_hintrewrite ~subst:(Some subst_hintrewrite) @@ -250,7 +256,8 @@ let find_applied_relation ?loc env sigma c left2right = spc () ++ str"of this term does not end with an applied relation.") (* To add rewriting rules to a base *) -let add_rew_rules base lrul = +let add_rew_rules ~locality base lrul = + let () = Hints.check_hint_locality locality in let counter = ref 0 in let env = Global.env () in let sigma = Evd.from_env env in @@ -267,5 +274,9 @@ let add_rew_rules base lrul = rew_tac = Option.map intern t} in incr counter; HintDN.add pat (!counter, rul) dn) HintDN.empty lrul - in Lib.add_anonymous_leaf (inHintRewrite (base,lrul)) - + in + let open Goptions in + match locality with + | OptLocal -> cache_hintrewrite ((),(base,lrul)) + | OptDefault | OptGlobal -> Lib.add_anonymous_leaf (inGlobalHintRewrite (base,lrul)) + | OptExport -> Lib.add_anonymous_leaf (inExportHintRewrite (base,lrul)) diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index 974aef8e8f..dec6cc5ef4 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -17,7 +17,7 @@ open Equality type raw_rew_rule = (constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option) CAst.t (** To add rewriting rules to a base *) -val add_rew_rules : string -> raw_rew_rule list -> unit +val add_rew_rules : locality:Goptions.option_locality -> string -> raw_rew_rule list -> unit (** The AutoRewrite tactic. The optional conditions tell rewrite how to handle matching and side-condition solving. diff --git a/tactics/cbn.ml b/tactics/cbn.ml index 39959d6fb8..6fb6cff04f 100644 --- a/tactics/cbn.ml +++ b/tactics/cbn.ml @@ -820,3 +820,15 @@ let whd_cbn flags env sigma t = (whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t, Stack.empty)) in Stack.zip ~refold:true sigma state + +let norm_cbn flags env sigma t = + let push_rel_check_zeta d env = + let open CClosure.RedFlags in + let d = match d with + | LocalDef (na,c,t) when not (red_set flags fZETA) -> LocalAssum (na,t) + | d -> d in + push_rel d env in + let rec strongrec env t = + map_constr_with_full_binders env sigma + push_rel_check_zeta strongrec env (whd_cbn flags env sigma t) in + strongrec env t diff --git a/tactics/cbn.mli b/tactics/cbn.mli index af54771382..a02a74f9e4 100644 --- a/tactics/cbn.mli +++ b/tactics/cbn.mli @@ -8,6 +8,13 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(** Weak-head cbn reduction. Despite the name, the cbn reduction is a complex + reduction distinct from call-by-name or call-by-need. *) val whd_cbn : CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr + +(** Strong variant of cbn reduction. *) +val norm_cbn : + CClosure.RedFlags.reds -> + Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr diff --git a/tactics/elim.ml b/tactics/elim.ml index 9a55cabc86..9e7843b2bb 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -19,7 +19,6 @@ open Tacmach.New open Tacticals.New open Clenv open Tactics -open Proofview.Notations type branch_args = { branchnum : int; (* the branch number *) @@ -28,8 +27,6 @@ type branch_args = { true=assumption, false=let-in *) branchnames : Tactypes.intro_patterns} -module NamedDecl = Context.Named.Declaration - type elim_kind = Case of bool | Elim (* Find the right elimination suffix corresponding to the sort of the goal *) @@ -217,52 +214,3 @@ let h_decompose l c = decompose_these c l let h_decompose_or = decompose_or let h_decompose_and = decompose_and - -(* The tactic Double performs a double induction *) - -let induction_trailer abs_i abs_j bargs = - tclTHEN - (tclDO (abs_j - abs_i) intro) - (onLastHypId - (fun id -> - Proofview.Goal.enter begin fun gl -> - let idty = pf_get_type_of gl (mkVar id) in - let fvty = global_vars (pf_env gl) (project gl) idty in - let possible_bring_hyps = - (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs - in - let (hyps,_) = - List.fold_left - (fun (bring_ids,leave_ids) d -> - let cid = NamedDecl.get_id d in - if not (List.mem cid leave_ids) - then (d::bring_ids,leave_ids) - else (bring_ids,cid::leave_ids)) - ([],fvty) possible_bring_hyps - in - let ids = List.rev (ids_of_named_context hyps) in - (tclTHENLIST - [revert ids; elimination_then (fun _ -> tclIDTAC) id]) - end - )) - -let double_ind h1 h2 = - Proofview.Goal.enter begin fun gl -> - let abs_i = depth_of_quantified_hypothesis true h1 gl in - let abs_j = depth_of_quantified_hypothesis true h2 gl in - let abs = - if abs_i < abs_j then Proofview.tclUNIT (abs_i,abs_j) else - if abs_i > abs_j then Proofview.tclUNIT (abs_j,abs_i) else - let info = Exninfo.reify () in - tclZEROMSG ~info (Pp.str "Both hypotheses are the same.") in - abs >>= fun (abs_i,abs_j) -> - (tclTHEN (tclDO abs_i intro) - (onLastHypId - (fun id -> - elimination_then - (introElimAssumsThen (induction_trailer abs_i abs_j)) id))) - end - -let h_double_induction = double_ind - - diff --git a/tactics/elim.mli b/tactics/elim.mli index 01053502e4..a603b472f7 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -21,4 +21,3 @@ val case_tac : bool -> or_and_intro_pattern option -> val h_decompose : inductive list -> constr -> unit Proofview.tactic val h_decompose_or : constr -> unit Proofview.tactic val h_decompose_and : constr -> unit Proofview.tactic -val h_double_induction : quantified_hypothesis -> quantified_hypothesis-> unit Proofview.tactic diff --git a/tactics/hints.ml b/tactics/hints.ml index 0cc8becd8f..058602acfd 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1187,6 +1187,28 @@ let create_hint_db l n st b = let hint = make_hint ~local:l n (CreateDB (b, st)) in Lib.add_anonymous_leaf (inAutoHint hint) +let warn_deprecated_hint_without_locality = + CWarnings.create ~name:"deprecated-hint-without-locality" ~category:"deprecated" + (fun () -> strbrk "The default value for hint locality is currently \ + \"local\" in a section and \"global\" otherwise, but is scheduled to change \ + in a future release. For the time being, adding hints outside of sections \ + without specifying an explicit locality is therefore deprecated. It is \ + recommended to use \"export\" whenever possible.") + +let check_hint_locality = let open Goptions in function +| OptGlobal -> + if Global.sections_are_opened () then + CErrors.user_err Pp.(str + "This command does not support the global attribute in sections."); +| OptExport -> + if Global.sections_are_opened () then + CErrors.user_err Pp.(str + "This command does not support the export attribute in sections."); +| OptDefault -> + if not @@ Global.sections_are_opened () then + warn_deprecated_hint_without_locality () +| OptLocal -> () + let interp_locality = function | Goptions.OptDefault | Goptions.OptGlobal -> false, true | Goptions.OptExport -> false, false diff --git a/tactics/hints.mli b/tactics/hints.mli index f5947bb946..381c7a1951 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -182,6 +182,8 @@ val searchtable_map : hint_db_name -> hint_db val searchtable_add : (hint_db_name * hint_db) -> unit +val check_hint_locality : Goptions.option_locality -> unit + (** [create_hint_db local name st use_dn]. [st] is a transparency state for unification using this db [use_dn] switches the use of the discrimination net for all hints diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index b415b30de8..87cae3abe5 100644 --- a/tactics/redexpr.ml +++ b/tactics/redexpr.ml @@ -46,9 +46,6 @@ let cbv_native env sigma c = let whd_cbn = Cbn.whd_cbn -let strong_cbn flags = - strong_with_flags whd_cbn flags - let simplIsCbn = Goptions.declare_bool_option_and_ref ~depr:false ~key:["SimplIsCbn"] ~value:false @@ -248,11 +245,11 @@ let reduction_of_red_expr_val = function | Hnf -> (e_red hnf_constr,DEFAULTcast) | Simpl (f,o) -> let whd_am = if simplIsCbn () then whd_cbn f else whd_simpl in - let am = if simplIsCbn () then strong_cbn f else simpl in + let am = if simplIsCbn () then Cbn.norm_cbn f else simpl in (contextualize (if head_style then whd_am else am) am o,DEFAULTcast) | Cbv f -> (e_red (cbv_norm_flags f),DEFAULTcast) | Cbn f -> - (e_red (strong_cbn f), DEFAULTcast) + (e_red (Cbn.norm_cbn f), DEFAULTcast) | Lazy f -> (e_red (clos_norm_flags f),DEFAULTcast) | Unfold ubinds -> (e_red (unfoldn (List.map out_with_occurrences ubinds)),DEFAULTcast) | Fold cl -> (e_red (fold_commands cl),DEFAULTcast) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b40bdbc25e..cbf12ac22f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -156,9 +156,6 @@ let convert_hyp ~check ~reorder d = end end -let convert_concl_no_check = convert_concl ~check:false -let convert_hyp_no_check = convert_hyp ~check:false ~reorder:false - let convert_gen pb x y = Proofview.Goal.enter begin fun gl -> match Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y with @@ -1244,8 +1241,6 @@ let force_destruction_arg with_evars env sigma c = (* tactic "cut" (actually modus ponens) *) (****************************************) -let normalize_cut = false - let cut c = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -1260,8 +1255,6 @@ let cut c = | sigma, s -> let r = Sorts.relevance_of_sort s in let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in - (* Backward compat: normalize [c]. *) - let c = if normalize_cut then strong whd_betaiota env sigma c else c in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Refine.refine ~typecheck:false begin fun h -> let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c r (Vars.lift 1 concl)) in @@ -1299,7 +1292,7 @@ let do_replace id = function [Ti] and the first one (resp last one) being [G] whose hypothesis [id] is replaced by P using the proof given by [tac] *) -let clenv_refine_in ?err with_evars targetid id sigma0 clenv tac = +let clenv_refine_in ?err with_evars targetid replace sigma0 clenv tac = let clenv = Clenv.clenv_pose_dependent_evars ~with_evars clenv in let evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd in let clenv = Clenv.update_clenv_evd clenv evd in @@ -1310,11 +1303,10 @@ let clenv_refine_in ?err with_evars targetid id sigma0 clenv tac = let new_hyp_prf = clenv_value clenv in let exact_tac = Logic.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf) in let naming = NamingMustBe (CAst.make targetid) in - let with_clear = do_replace (Some id) naming in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS (clear_metas evd)) (Tacticals.New.tclTHENLAST - (assert_after_then_gen ?err with_clear naming new_hyp_typ tac) exact_tac) + (assert_after_then_gen ?err replace naming new_hyp_typ tac) exact_tac) (********************************************) (* Elimination tactics *) @@ -1365,7 +1357,7 @@ let elimination_in_clause_scheme env sigma with_evars ~flags if EConstr.eq_constr sigma hyp_typ new_hyp_typ then user_err ~hdr:"general_rewrite_in" (str "Nothing to rewrite in " ++ Id.print id ++ str"."); - clenv_refine_in with_evars id id sigma elimclause'' + clenv_refine_in with_evars id true sigma elimclause'' (fun id -> Proofview.tclUNIT ()) (* @@ -1814,6 +1806,7 @@ let apply_in_once ?(respect_opaque = false) with_delta let t' = Tacmach.New.pf_get_hyp_typ id gl in let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in let targetid = find_name true (LocalAssum (make_annot Anonymous Sorts.Relevant,t')) naming gl in + let replace = Id.equal id targetid in let rec aux ?err idstoclear with_destruct c = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -1826,7 +1819,7 @@ let apply_in_once ?(respect_opaque = false) with_delta if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in try let clause = apply_in_once_main flags innerclause env sigma (loc,c,lbind) in - clenv_refine_in ?err with_evars targetid id sigma clause + clenv_refine_in ?err with_evars targetid replace sigma clause (fun id -> replace_error_option err ( apply_clear_request clear_flag false c <*> @@ -2324,26 +2317,31 @@ let rewrite_hyp_then with_evars thin l2r id tac = tclEVARSTHEN sigma (Tacticals.New.tclTHENFIRST eqtac (tac thin)) end -let prepare_naming ?loc = function - | IntroIdentifier id -> NamingMustBe (CAst.make ?loc id) - | IntroAnonymous -> NamingAvoid Id.Set.empty - | IntroFresh id -> NamingBasedOn (id, Id.Set.empty) - -let rec explicit_intro_names = let open CAst in function -| {v=IntroForthcoming _} :: l -> explicit_intro_names l -| {v=IntroNaming (IntroIdentifier id)} :: l -> Id.Set.add id (explicit_intro_names l) +let rec collect_intro_names = let open CAst in function +| {v=IntroForthcoming _} :: l -> collect_intro_names l +| {v=IntroNaming (IntroIdentifier id)} :: l -> + let ids1, ids2 = collect_intro_names l in Id.Set.add id ids1, ids2 | {v=IntroAction (IntroOrAndPattern l)} :: l' -> let ll = match l with IntroAndPattern l -> [l] | IntroOrPattern ll -> ll in - let fold accu l = Id.Set.union accu (explicit_intro_names (l@l')) in - List.fold_left fold Id.Set.empty ll + let fold (ids1',ids2') l = + let ids1, ids2 = collect_intro_names (l@l') in + Id.Set.union ids1 ids1', Id.Set.union ids2 ids2' in + List.fold_left fold (Id.Set.empty,Id.Set.empty) ll | {v=IntroAction (IntroInjection l)} :: l' -> - explicit_intro_names (l@l') + collect_intro_names (l@l') | {v=IntroAction (IntroApplyOn (c,pat))} :: l' -> - explicit_intro_names (pat::l') -| {v=(IntroNaming (IntroAnonymous | IntroFresh _) + collect_intro_names (pat::l') +| {v=IntroNaming (IntroFresh id)} :: l -> + let ids1, ids2 = collect_intro_names l in ids1, Id.Set.add id ids2 +| {v=(IntroNaming IntroAnonymous | IntroAction (IntroWildcard | IntroRewrite _))} :: l -> - explicit_intro_names l -| [] -> Id.Set.empty + collect_intro_names l +| [] -> Id.Set.empty, Id.Set.empty + +let explicit_intro_names l = fst (collect_intro_names l) + +let explicit_all_intro_names l = + let ids1,ids2 = collect_intro_names l in Id.Set.union ids1 ids2 let rec check_name_unicity env ok seen = let open CAst in function | {v=IntroForthcoming _} :: l -> check_name_unicity env ok seen l @@ -2368,30 +2366,33 @@ let rec check_name_unicity env ok seen = let open CAst in function check_name_unicity env ok seen l | [] -> () -let wild_id = Id.of_string "_tmp" - -let rec list_mem_assoc_right id = function - | [] -> false - | {CAst.v=id'}::l -> Id.equal id id' || list_mem_assoc_right id l +let fresh_wild ids = + let rec aux s = + if Id.Set.exists (fun id -> String.is_prefix s (Id.to_string id)) ids + then aux (s ^ "'") + else Id.of_string s in + aux "_H" -let check_thin_clash_then id thin avoid tac = - if list_mem_assoc_right id thin then - let newid = next_ident_away (add_suffix id "'") avoid in - let thin = - List.map CAst.(map (fun id' -> if Id.equal id id' then newid else id')) thin in - Tacticals.New.tclTHEN (rename_hyp [id,newid]) (tac thin) - else - tac thin +let make_naming ?loc avoid l = function + | IntroIdentifier id -> NamingMustBe (CAst.make ?loc id) + | IntroAnonymous -> NamingAvoid (Id.Set.union avoid (explicit_intro_names l)) + | IntroFresh id -> NamingBasedOn (id, Id.Set.union avoid (explicit_intro_names l)) -let make_tmp_naming avoid l = function +let rec make_naming_action avoid l = function (* In theory, we could use a tmp id like "wild_id" for all actions but we prefer to avoid it to avoid this kind of "ugly" names *) - (* Alternatively, we could have called check_thin_clash_then on - IntroAnonymous, but at the cost of a "renaming"; Note that in the - case of IntroFresh, we should use check_thin_clash_then anyway to - prevent the case of an IntroFresh precisely using the wild_id *) - | IntroWildcard -> NamingBasedOn (wild_id, Id.Set.union avoid (explicit_intro_names l)) - | pat -> NamingAvoid(Id.Set.union avoid (explicit_intro_names ((CAst.make @@ IntroAction pat)::l))) + | IntroWildcard -> + NamingBasedOn (fresh_wild (Id.Set.union avoid (explicit_all_intro_names l)), Id.Set.empty) + | IntroApplyOn (_,{CAst.v=pat;loc}) -> make_naming_pattern avoid ?loc l pat + | (IntroOrAndPattern _ | IntroInjection _ | IntroRewrite _) as pat -> + NamingAvoid(Id.Set.union avoid (explicit_intro_names ((CAst.make @@ IntroAction pat)::l))) + +and make_naming_pattern ?loc avoid l = function + | IntroNaming pat -> make_naming ?loc avoid l pat + | IntroAction pat -> make_naming_action avoid l pat + | IntroForthcoming _ -> NamingAvoid (Id.Set.union avoid (explicit_intro_names l)) + +let prepare_naming ?loc pat = make_naming ?loc Id.Set.empty [] pat let fit_bound n = function | None -> true @@ -2430,38 +2431,21 @@ let rec intro_patterns_core with_evars avoid ids thin destopt bound n tac = [CAst.make @@ IntroNaming IntroAnonymous] | {CAst.loc;v=pat} :: l -> if exceed_bound n bound then error_unexpected_extra_pattern loc bound pat else + let naming = make_naming_pattern avoid l pat in match pat with | IntroForthcoming onlydeps -> - intro_forthcoming_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l))) - destopt onlydeps bound n + intro_forthcoming_then_gen naming destopt onlydeps bound n (fun ids -> intro_patterns_core with_evars avoid ids thin destopt bound (n+List.length ids) tac l) | IntroAction pat -> - intro_then_gen (make_tmp_naming avoid l pat) - destopt true false + intro_then_gen naming destopt true false (intro_pattern_action ?loc with_evars pat thin destopt (fun thin bound' -> intro_patterns_core with_evars avoid ids thin destopt bound' 0 (fun ids thin -> intro_patterns_core with_evars avoid ids thin destopt bound (n+1) tac l))) | IntroNaming pat -> - intro_pattern_naming loc with_evars avoid ids pat thin destopt bound (n+1) tac l - - (* Pi-introduction rule, used backwards *) -and intro_pattern_naming loc with_evars avoid ids pat thin destopt bound n tac l = - match pat with - | IntroIdentifier id -> - check_thin_clash_then id thin avoid (fun thin -> - intro_then_gen (NamingMustBe CAst.(make ?loc id)) destopt true false - (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound n tac l)) - | IntroAnonymous -> - intro_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l))) - destopt true false - (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound n tac l) - | IntroFresh id -> - (* todo: avoid thinned names to interfere with generation of fresh name *) - intro_then_gen (NamingBasedOn (id, Id.Set.union avoid (explicit_intro_names l))) - destopt true false - (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound n tac l) + intro_then_gen naming destopt true false + (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound (n+1) tac l) and intro_pattern_action ?loc with_evars pat thin destopt tac id = match pat with @@ -2474,24 +2458,16 @@ and intro_pattern_action ?loc with_evars pat thin destopt tac id = | IntroRewrite l2r -> rewrite_hyp_then with_evars thin l2r id (fun thin -> tac thin None []) | IntroApplyOn ({CAst.loc=loc';v=f},{CAst.loc;v=pat}) -> - let naming,tac_ipat = - prepare_intros ?loc with_evars (IntroIdentifier id) destopt pat in - let doclear = - if naming = NamingMustBe (CAst.make ?loc id) then - Proofview.tclUNIT () (* apply_in_once do a replacement *) - else - clear [id] in - let f env sigma = let (sigma, c) = f env sigma in (sigma,(c, NoBindings)) - in + let naming = NamingMustBe (CAst.make ?loc id) in + let tac_ipat = prepare_action ?loc with_evars destopt pat in + let f env sigma = let (sigma, c) = f env sigma in (sigma,(c, NoBindings)) in apply_in_delayed_once true true with_evars naming id (None,CAst.make ?loc:loc' f) - (fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []]) + (fun id -> Tacticals.New.tclTHENLIST [tac_ipat id; tac thin None []]) -and prepare_intros ?loc with_evars dft destopt = function +and prepare_action ?loc with_evars destopt = function | IntroNaming ipat -> - prepare_naming ?loc ipat, - (fun id -> move_hyp id destopt) + (fun _ -> Proofview.tclUNIT ()) | IntroAction ipat -> - prepare_naming ?loc dft, (let tac thin bound = intro_patterns_core with_evars Id.Set.empty [] thin destopt bound 0 (fun _ l -> clear_wildcards l) in @@ -2528,9 +2504,19 @@ let intros_patterns with_evars = function (* Forward reasoning *) (**************************) -let prepare_intros_opt with_evars dft destopt = function - | None -> prepare_naming dft, (fun _id -> Proofview.tclUNIT ()) - | Some {CAst.loc;v=ipat} -> prepare_intros ?loc with_evars dft destopt ipat +let prepare_intros_opt with_evars dft destopt ipat = + let naming, loc, ipat = match ipat with + | None -> + let pat = IntroNaming dft in make_naming_pattern Id.Set.empty [] pat, None, pat + | Some {CAst.loc;v=(IntroNaming pat as ipat)} -> + (* "apply ... in H as id" needs to use id and H is kept iff id<>H *) + prepare_naming ?loc pat, loc, ipat + | Some {CAst.loc;v=(IntroAction pat as ipat)} -> + (* "apply ... in H as pat" reuses H so that old H is always cleared *) + (match dft with IntroIdentifier _ -> prepare_naming ?loc dft | _ -> make_naming_action Id.Set.empty [] pat), + loc, ipat + | Some {CAst.loc;v=(IntroForthcoming _)} -> assert false in + naming, prepare_action ?loc with_evars destopt ipat let ipat_of_name = function | Anonymous -> None @@ -3045,8 +3031,7 @@ let specialize (c,lbind) ipat = match EConstr.kind sigma (fst(EConstr.decompose_app sigma (snd(EConstr.decompose_lam_assum sigma c)))) with | Var id when Id.List.mem id (Tacmach.New.pf_ids_of_hyps gl) -> (* Like assert (id:=id args) but with the concept of specialization *) - let naming,tac = - prepare_intros_opt false (IntroIdentifier id) MoveLast ipat in + let naming,tac = prepare_intros_opt false (IntroIdentifier id) MoveLast ipat in let repl = do_replace (Some id) naming in Tacticals.New.tclTHENFIRST (assert_before_then_gen repl naming typ tac) @@ -3059,10 +3044,10 @@ let specialize (c,lbind) ipat = (* TODO: add intro to be more homogeneous. It will break scripts but will be easy to fix *) (Tacticals.New.tclTHENLAST (cut typ) (exact_no_check term)) - | Some {CAst.loc;v=ipat} -> + | Some _ as ipat -> (* Like pose proof with extra support for "with" bindings *) (* even though the "with" bindings forces full application *) - let naming,tac = prepare_intros ?loc false IntroAnonymous MoveLast ipat in + let naming, tac = prepare_intros_opt false IntroAnonymous MoveLast ipat in Tacticals.New.tclTHENFIRST (assert_before_then_gen false naming typ tac) (exact_no_check term) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index a6471be549..c07073a91a 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -35,10 +35,6 @@ val is_quantified_hypothesis : Id.t -> Proofview.Goal.t -> bool val introduction : Id.t -> unit Proofview.tactic val convert_concl : check:bool -> types -> cast_kind -> unit Proofview.tactic val convert_hyp : check:bool -> reorder:bool -> named_declaration -> unit Proofview.tactic -val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic -[@@ocaml.deprecated "use [Tactics.convert_concl]"] -val convert_hyp_no_check : named_declaration -> unit Proofview.tactic -[@@ocaml.deprecated "use [Tactics.convert_hyp]"] val mutual_fix : Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic val fix : Id.t -> int -> unit Proofview.tactic @@ -81,11 +77,6 @@ val auto_intros_tac : Names.Name.t list -> unit Proofview.tactic val intros : unit Proofview.tactic -(** [depth_of_quantified_hypothesis b h g] returns the index of [h] in - the conclusion of goal [g], up to head-reduction if [b] is [true] *) -val depth_of_quantified_hypothesis : - bool -> quantified_hypothesis -> Proofview.Goal.t -> int - val intros_until : quantified_hypothesis -> unit Proofview.tactic val intros_clearing : bool list -> unit Proofview.tactic diff --git a/test-suite/bugs/closed/bug_13413.v b/test-suite/bugs/closed/bug_13413.v new file mode 100644 index 0000000000..b4414a6a1d --- /dev/null +++ b/test-suite/bugs/closed/bug_13413.v @@ -0,0 +1,20 @@ +Goal forall (A B : Prop) (H : A -> B), A -> A -> B. +intros A B H ?%H H0. +exact H1. +Qed. + +Goal forall (A B : Prop) (H : A -> B), A -> A -> B. +intros A B H ?H%H H0. +exact H1. +Qed. + +Goal forall (A B : Prop) (H : A -> B), A -> A -> B. +intros A B H J%H H0. +exact J. +Qed. + +Set Mangle Names. +Goal forall (A B : Prop) (H : A -> B), A -> A -> B. +intros A B H ?%H _0. +assumption. +Qed. diff --git a/test-suite/misc/non-marshalable-state.sh b/test-suite/misc/non-marshalable-state.sh new file mode 100755 index 0000000000..eef7786ebc --- /dev/null +++ b/test-suite/misc/non-marshalable-state.sh @@ -0,0 +1,30 @@ +#!/usr/bin/env bash + +set -e + +export COQBIN=$BIN +export PATH=$COQBIN:$PATH + +cd misc/non-marshalable-state/ + +coq_makefile -f _CoqProject -o Makefile + +make clean + +make src/evil_plugin.cmxs +make src/good_plugin.cmxs + +RC=1 +# must fail +coqc -async-proofs on -I src -Q theories Marshal theories/evil.v 2> log1 1>&2 || RC=0 +# for this reason +grep -q 'Marshalling error' log1 || RC=1 + +# must work +coqc -async-proofs off -I src -Q theories Marshal theories/evil.v + +# must work +coqc -async-proofs on -I src -Q theories Marshal theories/good.v + + +exit $RC diff --git a/test-suite/misc/non-marshalable-state/_CoqProject b/test-suite/misc/non-marshalable-state/_CoqProject new file mode 100644 index 0000000000..09e68d866c --- /dev/null +++ b/test-suite/misc/non-marshalable-state/_CoqProject @@ -0,0 +1,9 @@ +-Q theories Marshal +-I src + +src/evil.mlg +src/good.mlg +src/evil_plugin.mlpack +src/good_plugin.mlpack +theories/evil.v +theories/good.v diff --git a/test-suite/misc/non-marshalable-state/src/evil.mlg b/test-suite/misc/non-marshalable-state/src/evil.mlg new file mode 100644 index 0000000000..59b2b5a8ac --- /dev/null +++ b/test-suite/misc/non-marshalable-state/src/evil.mlg @@ -0,0 +1,15 @@ +DECLARE PLUGIN "evil_plugin" + +{ + +let state = Summary.ref + ~name:"elpi-compiler-cache" + None + +} + +VERNAC COMMAND EXTEND magic CLASSIFIED AS SIDEFF +| [ "magic" ] -> { + state := Some (fun () -> ()) +} +END diff --git a/test-suite/misc/non-marshalable-state/src/evil_plugin.mlpack b/test-suite/misc/non-marshalable-state/src/evil_plugin.mlpack new file mode 100644 index 0000000000..6382aa69e1 --- /dev/null +++ b/test-suite/misc/non-marshalable-state/src/evil_plugin.mlpack @@ -0,0 +1 @@ +Evil diff --git a/test-suite/misc/non-marshalable-state/src/good.mlg b/test-suite/misc/non-marshalable-state/src/good.mlg new file mode 100644 index 0000000000..c6b9cbefd5 --- /dev/null +++ b/test-suite/misc/non-marshalable-state/src/good.mlg @@ -0,0 +1,16 @@ +DECLARE PLUGIN "good_plugin" + +{ + +let state = Summary.Local.ref + ~name:"elpi-compiler-cache" + None + +} + +VERNAC COMMAND EXTEND magic CLASSIFIED AS SIDEFF +| [ "magic" ] -> { + let open Summary.Local in + state := Some (fun () -> ()) +} +END diff --git a/test-suite/misc/non-marshalable-state/src/good_plugin.mlpack b/test-suite/misc/non-marshalable-state/src/good_plugin.mlpack new file mode 100644 index 0000000000..cd9dd73b78 --- /dev/null +++ b/test-suite/misc/non-marshalable-state/src/good_plugin.mlpack @@ -0,0 +1 @@ +Good diff --git a/test-suite/misc/non-marshalable-state/theories/evil.v b/test-suite/misc/non-marshalable-state/theories/evil.v new file mode 100644 index 0000000000..661482a975 --- /dev/null +++ b/test-suite/misc/non-marshalable-state/theories/evil.v @@ -0,0 +1,5 @@ +Declare ML Module "evil_plugin". + +magic. + +Lemma x : True. Proof. trivial. Qed. diff --git a/test-suite/misc/non-marshalable-state/theories/good.v b/test-suite/misc/non-marshalable-state/theories/good.v new file mode 100644 index 0000000000..eab9a043e1 --- /dev/null +++ b/test-suite/misc/non-marshalable-state/theories/good.v @@ -0,0 +1,5 @@ +Declare ML Module "good_plugin". + +magic. + +Lemma x : True. Proof. trivial. Qed. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index e46774f68a..9fd846ac16 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -11,7 +11,7 @@ eq_refl : ?y = ?y where ?y : [ |- nat] -Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x. Arguments eq {A}%type_scope _ _ Arguments eq_refl {B}%type_scope {y}, [_] _ @@ -22,7 +22,7 @@ eq_refl is not universe polymorphic Arguments eq_refl {B}%type_scope {y}, [_] _ (where some original arguments have been renamed) Expands to: Constructor Coq.Init.Logic.eq_refl -Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x +Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x. Arguments myEq _%type_scope _ _ Arguments myrefl {C}%type_scope x _ @@ -55,7 +55,7 @@ Expands to: Constant Arguments_renaming.Test1.myplus @myplus : forall Z : Type, Z -> nat -> nat -> nat Inductive myEq (A B : Type) (x : A) : A -> Prop := - myrefl : B -> myEq A B x x + myrefl : B -> myEq A B x x. Arguments myEq (_ _)%type_scope _ _ Arguments myrefl A%type_scope {C}%type_scope x _ diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index 8e10107673..fc3b6fbd99 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -5,7 +5,7 @@ A : Set a : A l : list' A Unable to unify "list' (A * A)%type" with "list' A". -Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x +Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x. Arguments foo _%type_scope _ Arguments Foo _%type_scope _ diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out index 02e58775b5..fdd609f5b2 100644 --- a/test-suite/output/InitSyntax.out +++ b/test-suite/output/InitSyntax.out @@ -1,5 +1,5 @@ Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := - exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x} + exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x}. Arguments sig2 [A]%type_scope (_ _)%type_scope Arguments exist2 [A]%type_scope (_ _)%function_scope _ _ _ diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out index ca8e1b58a8..7ca4de1e46 100644 --- a/test-suite/output/Int63Syntax.out +++ b/test-suite/output/Int63Syntax.out @@ -56,3 +56,21 @@ t = 2%i63 : int = 37151199385380486 : int + = 4 + : int + = 4 + : int + = 4 + : int + = add + : int -> int -> int + = 12 + : int + = 12 + : int + = 12 + : int + = 3 + x + : int + = 1 + 2 + x + : int diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v index 6f1046f7a5..50910264f2 100644 --- a/test-suite/output/Int63Syntax.v +++ b/test-suite/output/Int63Syntax.v @@ -40,3 +40,18 @@ Open Scope int63_scope. Check (2+2). Eval vm_compute in 2+2. Eval vm_compute in 65675757 * 565675998. + +Eval simpl in 2+2. +Eval hnf in 2+2. +Eval cbn in 2+2. +Eval hnf in PrimInt63.add. + +Eval simpl in (2 * 3) + (2 * 3). +Eval hnf in (2 * 3) + (2 * 3). +Eval cbn in (2 * 3) + (2 * 3). + +Section TestNoSimpl. +Variable x : int. +Eval simpl in 1 + 2 + x. +Eval hnf in 1 + 2 + x. +End TestNoSimpl. diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index fe16dba496..03b9e3b527 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -4,14 +4,14 @@ existT is template universe polymorphic on sigT.u0 sigT.u1 Arguments existT [A]%type_scope _%function_scope _ _ Expands to: Constructor Coq.Init.Specif.existT Inductive sigT (A : Type) (P : A -> Type) : Type := - existT : forall x : A, P x -> {x : A & P x} + existT : forall x : A, P x -> {x : A & P x}. Arguments sigT [A]%type_scope _%type_scope Arguments existT [A]%type_scope _%function_scope _ _ existT : forall [A : Type] (P : A -> Type) (x : A), P x -> {x : A & P x} Argument A is implicit -Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x. Arguments eq {A}%type_scope _ _ Arguments eq_refl {A}%type_scope {x}, [_] _ @@ -50,7 +50,7 @@ Arguments plus_n_O _%nat_scope plus_n_O is opaque Expands to: Constant Coq.Init.Peano.plus_n_O Inductive le (n : nat) : nat -> Prop := - le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m + le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m. Arguments le (_ _)%nat_scope Arguments le_n _%nat_scope @@ -60,7 +60,7 @@ comparison : Set comparison is not universe polymorphic Expands to: Inductive Coq.Init.Datatypes.comparison Inductive comparison : Set := - Eq : comparison | Lt : comparison | Gt : comparison + Eq : comparison | Lt : comparison | Gt : comparison. bar : foo bar is not universe polymorphic @@ -78,7 +78,7 @@ Arguments bar {x} Module Coq.Init.Peano Notation sym_eq := eq_sym Expands to: Notation Coq.Init.Logic.sym_eq -Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x. Arguments eq {A}%type_scope _ _ Arguments eq_refl {A}%type_scope {x}, {_} _ diff --git a/test-suite/output/PrintModule.out b/test-suite/output/PrintModule.out index 1a9bc068c5..7c7600b786 100644 --- a/test-suite/output/PrintModule.out +++ b/test-suite/output/PrintModule.out @@ -7,3 +7,11 @@ Module N : S with Module T := K := M Module N : S with Module T := M Module Type Func = Funsig (T0:Test) Sig Parameter x : T0.t. End +Module +A +:= Struct + Variant I : Set := C : nat -> I. + Record R : Set := Build_R { n : nat }. + Definition n : R -> nat. + End + diff --git a/test-suite/output/PrintModule.v b/test-suite/output/PrintModule.v index 54ef305be4..b4de03b556 100644 --- a/test-suite/output/PrintModule.v +++ b/test-suite/output/PrintModule.v @@ -60,3 +60,10 @@ Print Func. End Shortest_path. End QUX. + +Module A. +Variant I := C : nat -> I. +Record R := { n : nat }. +End A. + +Print Module A. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 95b6c6ee95..4993b747fa 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -1,6 +1,7 @@ -Inductive Empty@{uu} : Type@{uu} := +Inductive Empty@{uu} : Type@{uu} := . (* uu |= *) -Record PWrap (A : Type@{uu}) : Type@{uu} := pwrap { punwrap : A } +Record PWrap (A : Type@{uu}) : Type@{uu} := pwrap + { punwrap : A }. (* uu |= *) PWrap has primitive projections with eta conversion. @@ -12,7 +13,8 @@ fun (A : Type@{uu}) (p : PWrap@{uu} A) => punwrap _ p (* uu |= *) Arguments punwrap _%type_scope _ -Record RWrap (A : Type@{uu}) : Type@{uu} := rwrap { runwrap : A } +Record RWrap (A : Type@{uu}) : Type@{uu} := rwrap + { runwrap : A }. (* uu |= *) Arguments RWrap _%type_scope @@ -80,9 +82,9 @@ foo@{uu u v} = Type@{u} -> Type@{v} -> Type@{uu} : Type@{max(uu+1,u+1,v+1)} (* uu u v |= *) -Inductive Empty@{E} : Type@{E} := +Inductive Empty@{E} : Type@{E} := . (* E |= *) -Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } +Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }. (* E |= *) PWrap has primitive projections with eta conversion. @@ -107,7 +109,7 @@ insec@{v} = Type@{uu} -> Type@{v} : Type@{max(uu+1,v+1)} (* v |= *) Inductive insecind@{k} : Type@{k+1} := - inseccstr : Type@{k} -> insecind@{k} + inseccstr : Type@{k} -> insecind@{k}. (* k |= *) Arguments inseccstr _%type_scope @@ -115,7 +117,7 @@ insec@{uu v} = Type@{uu} -> Type@{v} : Type@{max(uu+1,v+1)} (* uu v |= *) Inductive insecind@{uu k} : Type@{k+1} := - inseccstr : Type@{k} -> insecind@{uu k} + inseccstr : Type@{k} -> insecind@{uu k}. (* uu k |= *) Arguments inseccstr _%type_scope diff --git a/test-suite/success/autorewrite.v b/test-suite/success/autorewrite.v index 71d333d439..0ac62fcdc9 100644 --- a/test-suite/success/autorewrite.v +++ b/test-suite/success/autorewrite.v @@ -4,25 +4,35 @@ Axiom Ack0 : forall m : nat, Ack 0 m = S m. Axiom Ack1 : forall n : nat, Ack (S n) 0 = Ack n 1. Axiom Ack2 : forall n m : nat, Ack (S n) (S m) = Ack n (Ack (S n) m). -Hint Rewrite Ack0 Ack1 Ack2 : base0. +Module M. + #[export] Hint Rewrite Ack0 Ack1 Ack2 : base0. -Lemma ResAck0 : (Ack 2 2 = 7 -> False) -> False. + Lemma ResAck0 : (Ack 2 2 = 7 -> False) -> False. + Proof. + intros. + autorewrite with base0 in H using try (apply H; reflexivity). + Qed. +End M. + +Lemma ResAck1 : forall H:(Ack 2 2 = 7 -> False), True -> False. Proof. intros. - autorewrite with base0 in H using try (apply H; reflexivity). -Qed. + Fail autorewrite with base0 in *. +Abort. + +Import M. Lemma ResAck1 : forall H:(Ack 2 2 = 7 -> False), True -> False. Proof. intros. autorewrite with base0 in *. - apply H;reflexivity. + apply H;reflexivity. Qed. (* Check autorewrite does not solve existing evars *) (* See discussion started by A. Chargueraud in Oct 2010 on coqdev *) -Hint Rewrite <- plus_n_O : base1. +Global Hint Rewrite <- plus_n_O : base1. Goal forall y, exists x, y+x = y. eexists. autorewrite with base1. Fail reflexivity. diff --git a/test-suite/success/forward.v b/test-suite/success/forward.v index 4e36dec15b..62c788e910 100644 --- a/test-suite/success/forward.v +++ b/test-suite/success/forward.v @@ -27,3 +27,7 @@ Fail match goal with |- (?f ?a) => idtac end. (* should be beta-iota reduced *) 2:match goal with _: (?f ?a) |- _ => idtac end. (* should not be beta-iota reduced *) Abort. +Goal nat. +assert nat as J%S by exact 0. +exact J. +Qed. diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 4983ee3c0d..615350c58c 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -154,50 +154,6 @@ induction H. change (0 = z -> True) in IHrepr''. Abort. -(* Test double induction *) - -(* This was failing in 8.5 and before because of a bug in the order of - hypotheses *) - -Set Warnings "-deprecated". - -Inductive I2 : Type := - C2 : forall x:nat, x=x -> I2. -Goal forall a b:I2, a = b. -double induction a b. -Abort. - -(* This was leaving useless hypotheses in 8.5 and before because of - the same bug. This is a change of compatibility. *) - -Inductive I3 : Prop := - C3 : forall x:nat, x=x -> I3. -Goal forall a b:I3, a = b. -double induction a b. -Fail clear H. (* H should have been erased *) -Abort. - -(* This one had quantification in reverse order in 8.5 and before *) -(* This is a change of compatibility. *) - -Goal forall m n, le m n -> le n m -> n=m. -intros m n. double induction 1 2. -3:destruct 1. (* Should be "S m0 <= m0" *) -Abort. - -(* Idem *) - -Goal forall m n p q, le m n -> le p q -> n+p=m+q. -intros *. double induction 1 2. -3:clear H2. (* H2 should have been erased *) -Abort. - -(* This is unchanged *) - -Goal forall m n:nat, n=m. -double induction m n. -Abort. - (* Mentioned as part of bug #12944 *) Inductive test : Set := cons : forall (IHv : nat) (v : test), test. diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index d37ad9f528..b8fbff05c6 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -152,3 +152,15 @@ Definition d := ltac:(intro x; exact (x*x)). Definition d' : nat -> _ := ltac:(intros;exact 0). End Evar. + +Module Wildcard. + +(* We check that the wildcard internal name does not interfere with + user fresh names (currently the prefix is "_H") *) + +Goal nat -> bool -> nat -> bool. +intros _ ?_H ?_H. +exact _H. +Qed. + +End Wildcard. diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v index d597c0404a..5fe2cade3b 100644 --- a/theories/FSets/FSetDecide.v +++ b/theories/FSets/FSetDecide.v @@ -489,7 +489,7 @@ the above form: variables. We are going to use them with [autorewrite]. *) - Hint Rewrite + Global Hint Rewrite F.empty_iff F.singleton_iff F.add_iff F.remove_iff F.union_iff F.inter_iff F.diff_iff : set_simpl. @@ -499,7 +499,7 @@ the above form: now split. Qed. - Hint Rewrite eq_refl_iff : set_eq_simpl. + Global Hint Rewrite eq_refl_iff : set_eq_simpl. (** ** Decidability of FSet Propositions *) diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 115c7cb365..d6277b3bb5 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -3327,7 +3327,7 @@ Ltac invlist f := (** * Exporting hints and tactics *) -Hint Rewrite +Global Hint Rewrite rev_involutive (* rev (rev l) = l *) rev_unit (* rev (l ++ a :: nil) = a :: rev l *) map_nth (* nth n (map f l) (f d) = f (nth n l d) *) diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v index aa0c419f0e..579e5e9630 100644 --- a/theories/MSets/MSetDecide.v +++ b/theories/MSets/MSetDecide.v @@ -489,7 +489,7 @@ the above form: variables. We are going to use them with [autorewrite]. *) - Hint Rewrite + Global Hint Rewrite F.empty_iff F.singleton_iff F.add_iff F.remove_iff F.union_iff F.inter_iff F.diff_iff : set_simpl. @@ -499,7 +499,7 @@ the above form: now split. Qed. - Hint Rewrite eq_refl_iff : set_eq_simpl. + Global Hint Rewrite eq_refl_iff : set_eq_simpl. (** ** Decidability of MSet Propositions *) diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v index f80929e320..2d210e24a6 100644 --- a/theories/MSets/MSetRBT.v +++ b/theories/MSets/MSetRBT.v @@ -651,7 +651,7 @@ Proof. destruct (rbal'_match l x r); ok. Qed. -Hint Rewrite In_node_iff In_leaf_iff +Global Hint Rewrite In_node_iff In_leaf_iff makeRed_spec makeBlack_spec lbal_spec rbal_spec rbal'_spec : rb. Ltac descolor := destruct_all Color.t. @@ -670,7 +670,7 @@ Proof. - descolor; autorew; rewrite IHl; intuition_in. - descolor; autorew; rewrite IHr; intuition_in. Qed. -Hint Rewrite ins_spec : rb. +Global Hint Rewrite ins_spec : rb. Instance ins_ok s x `{Ok s} : Ok (ins x s). Proof. @@ -685,7 +685,7 @@ Proof. unfold add. now autorew. Qed. -Hint Rewrite add_spec' : rb. +Global Hint Rewrite add_spec' : rb. Lemma add_spec s x y `{Ok s} : InT y (add x s) <-> X.eq y x \/ InT y s. @@ -754,7 +754,7 @@ Proof. * ok. apply lbal_ok; ok. Qed. -Hint Rewrite lbalS_spec rbalS_spec : rb. +Global Hint Rewrite lbalS_spec rbalS_spec : rb. (** ** Append for deletion *) @@ -807,7 +807,7 @@ Proof. [intros a y b | intros t Ht]; autorew; tauto. Qed. -Hint Rewrite append_spec : rb. +Global Hint Rewrite append_spec : rb. Lemma append_ok : forall x l r `{Ok l, Ok r}, lt_tree x l -> gt_tree x r -> Ok (append l r). @@ -861,7 +861,7 @@ induct s x. rewrite ?IHr by trivial; intuition_in; order. Qed. -Hint Rewrite del_spec : rb. +Global Hint Rewrite del_spec : rb. Instance del_ok s x `{Ok s} : Ok (del x s). Proof. @@ -882,7 +882,7 @@ Proof. unfold remove. now autorew. Qed. -Hint Rewrite remove_spec : rb. +Global Hint Rewrite remove_spec : rb. Instance remove_ok s x `{Ok s} : Ok (remove x s). Proof. diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index 48df5fe884..420c17c9a4 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -127,7 +127,7 @@ Qed. End N2Nat. -Hint Rewrite N2Nat.inj_double N2Nat.inj_succ_double +Global Hint Rewrite N2Nat.inj_double N2Nat.inj_succ_double N2Nat.inj_succ N2Nat.inj_add N2Nat.inj_mul N2Nat.inj_sub N2Nat.inj_pred N2Nat.inj_div2 N2Nat.inj_max N2Nat.inj_min N2Nat.id @@ -147,7 +147,7 @@ Proof. induction n; simpl; trivial. apply SuccNat2Pos.id_succ. Qed. -Hint Rewrite id : Nnat. +Global Hint Rewrite id : Nnat. Ltac nat2N := apply N2Nat.inj; now autorewrite with Nnat. (** [N.of_nat] is hence injective *) @@ -206,7 +206,7 @@ Proof. now rewrite N2Nat.inj_iter, !id. Qed. End Nat2N. -Hint Rewrite Nat2N.id : Nnat. +Global Hint Rewrite Nat2N.id : Nnat. (** Compatibility notations *) diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v index e3e8f532b3..374af6de63 100644 --- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -348,7 +348,7 @@ Local Notation "- x" := (ZnZ.opp x). Local Infix "*" := ZnZ.mul. Local Notation wB := (base ZnZ.digits). -Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_add ZnZ.spec_mul +Global Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_add ZnZ.spec_mul ZnZ.spec_opp ZnZ.spec_sub : cyclic. diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index 7c5b43096a..f74a78e876 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -51,7 +51,7 @@ Local Infix "+" := add. Local Infix "-" := sub. Local Infix "*" := mul. -Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_succ ZnZ.spec_pred +Global Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_succ ZnZ.spec_pred ZnZ.spec_add ZnZ.spec_mul ZnZ.spec_sub : cyclic. Ltac zify := unfold eq, zero, one, two, succ, pred, add, sub, mul in *; diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index f324bbf52b..7bb725538b 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -954,6 +954,7 @@ Proof. intros _ HH; generalize (HH H1); discriminate. clear H. generalize (ltb_spec j i); case Int63.ltb; intros H2; unfold bit; simpl. + change 62%int63 with (digits - 1)%int63. assert (F2: (φ j < φ i)%Z) by (case H2; auto); clear H2. replace (is_zero (((x << i) >> j) << (digits - 1))) with true; auto. case (to_Z_bounded j); intros H1j H2j. diff --git a/theories/Numbers/HexadecimalNat.v b/theories/Numbers/HexadecimalNat.v index 94a14b90bd..696e89bd8e 100644 --- a/theories/Numbers/HexadecimalNat.v +++ b/theories/Numbers/HexadecimalNat.v @@ -230,7 +230,7 @@ Proof. simpl_of_lu; rewrite ?Nat.add_succ_l, Nat.add_0_l, ?to_lu_succ, to_of_lu_sixteenfold by assumption; - unfold lnorm; simpl; now destruct nztail. + unfold lnorm; cbn; now destruct nztail. Qed. (** Second bijection result *) diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v index 0c097b6773..9d9244eefb 100644 --- a/theories/Numbers/Integer/Abstract/ZAdd.v +++ b/theories/Numbers/Integer/Abstract/ZAdd.v @@ -18,7 +18,7 @@ Include ZBaseProp Z. (** Theorems that are either not valid on N or have different proofs on N and Z *) -Hint Rewrite opp_0 : nz. +Global Hint Rewrite opp_0 : nz. Theorem add_pred_l n m : P n + m == P (n + m). Proof. diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v index 4d2361689d..832931e5ef 100644 --- a/theories/Numbers/Integer/Abstract/ZBits.v +++ b/theories/Numbers/Integer/Abstract/ZBits.v @@ -26,7 +26,7 @@ Include BoolEqualityFacts A. Ltac order_nz := try apply pow_nonzero; order'. Ltac order_pos' := try apply abs_nonneg; order_pos. -Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz. +Global Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz. (** Some properties of power and division *) @@ -566,7 +566,7 @@ Tactic Notation "bitwise" "as" simple_intropattern(m) simple_intropattern(Hm) Ltac bitwise := bitwise as ?m ?Hm. -Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise. +Global Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise. (** The streams of bits that correspond to a numbers are exactly the ones which are stationary after some point. *) diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v index 66cbba9e08..2ad8dfcedb 100644 --- a/theories/Numbers/NatInt/NZAdd.v +++ b/theories/Numbers/NatInt/NZAdd.v @@ -14,9 +14,9 @@ Require Import NZAxioms NZBase. Module Type NZAddProp (Import NZ : NZAxiomsSig')(Import NZBase : NZBaseProp NZ). -Hint Rewrite +Global Hint Rewrite pred_succ add_0_l add_succ_l mul_0_l mul_succ_l sub_0_r sub_succ_r : nz. -Hint Rewrite one_succ two_succ : nz'. +Global Hint Rewrite one_succ two_succ : nz'. Ltac nzsimpl := autorewrite with nz. Ltac nzsimpl' := autorewrite with nz nz'. @@ -39,7 +39,7 @@ Proof. intros n m. now rewrite add_succ_r, add_succ_l. Qed. -Hint Rewrite add_0_r add_succ_r : nz. +Global Hint Rewrite add_0_r add_succ_r : nz. Theorem add_comm : forall n m, n + m == m + n. Proof. @@ -58,7 +58,7 @@ Proof. intro n; now nzsimpl'. Qed. -Hint Rewrite add_1_l add_1_r : nz. +Global Hint Rewrite add_1_l add_1_r : nz. Theorem add_assoc : forall n m p, n + (m + p) == (n + m) + p. Proof. @@ -104,6 +104,6 @@ Proof. intro n; now nzsimpl'. Qed. -Hint Rewrite sub_1_r : nz. +Global Hint Rewrite sub_1_r : nz. End NZAddProp. diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v index 3d6465191d..14728eaf40 100644 --- a/theories/Numbers/NatInt/NZMul.v +++ b/theories/Numbers/NatInt/NZMul.v @@ -28,7 +28,7 @@ Proof. now rewrite add_cancel_r. Qed. -Hint Rewrite mul_0_r mul_succ_r : nz. +Global Hint Rewrite mul_0_r mul_succ_r : nz. Theorem mul_comm : forall n m, n * m == m * n. Proof. @@ -69,7 +69,7 @@ Proof. intro n. now nzsimpl'. Qed. -Hint Rewrite mul_1_l mul_1_r : nz. +Global Hint Rewrite mul_1_l mul_1_r : nz. Theorem mul_shuffle0 : forall n m p, n*m*p == n*p*m. Proof. diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v index 3b2a496229..00edcd641f 100644 --- a/theories/Numbers/NatInt/NZPow.v +++ b/theories/Numbers/NatInt/NZPow.v @@ -45,7 +45,7 @@ Module Type NZPowProp (Import B : NZPow' A) (Import C : NZMulOrderProp A). -Hint Rewrite pow_0_r pow_succ_r : nz. +Global Hint Rewrite pow_0_r pow_succ_r : nz. (** Power and basic constants *) @@ -76,14 +76,14 @@ Proof. - now nzsimpl. Qed. -Hint Rewrite pow_1_r pow_1_l : nz. +Global Hint Rewrite pow_1_r pow_1_l : nz. Lemma pow_2_r : forall a, a^2 == a*a. Proof. intros. rewrite two_succ. nzsimpl; order'. Qed. -Hint Rewrite pow_2_r : nz. +Global Hint Rewrite pow_2_r : nz. (** Power and nullity *) diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v index 313b9adfd1..427a18d4ae 100644 --- a/theories/Numbers/Natural/Abstract/NBits.v +++ b/theories/Numbers/Natural/Abstract/NBits.v @@ -23,7 +23,7 @@ Module Type NBitsProp Include BoolEqualityFacts A. Ltac order_nz := try apply pow_nonzero; order'. -Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz. +Global Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz. (** Some properties of power and division *) @@ -368,7 +368,7 @@ Proof. split. apply bits_inj. intros EQ; now rewrite EQ. Qed. -Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise. +Global Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise. Tactic Notation "bitwise" "as" simple_intropattern(m) := apply bits_inj; intros m; autorewrite with bitwise. diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index e97f2dc748..7d50bdacad 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -876,7 +876,7 @@ Lemma compare_xO_xI p q : (p~0 ?= q~1) = switch_Eq Lt (p ?= q). Proof. exact (compare_cont_spec p q Lt). Qed. -Hint Rewrite compare_xO_xO compare_xI_xI compare_xI_xO compare_xO_xI : compare. +Global Hint Rewrite compare_xO_xO compare_xI_xI compare_xI_xO compare_xO_xI : compare. Ltac simpl_compare := autorewrite with compare. Ltac simpl_compare_in H := autorewrite with compare in H. diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v index 8813131d7b..18e55aefc6 100644 --- a/theories/Program/Combinators.v +++ b/theories/Program/Combinators.v @@ -40,8 +40,8 @@ Proof. reflexivity. Qed. -Hint Rewrite @compose_id_left @compose_id_right : core. -Hint Rewrite <- @compose_assoc : core. +Global Hint Rewrite @compose_id_left @compose_id_right : core. +Global Hint Rewrite <- @compose_assoc : core. (** [flip] is involutive. *) diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 25af2d5ffb..090322054e 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -162,7 +162,7 @@ Ltac pi_eq_proofs := repeat pi_eq_proof. Ltac clear_eq_proofs := abstract_eq_proofs ; pi_eq_proofs. -Hint Rewrite <- eq_rect_eq : refl_id. +Global Hint Rewrite <- eq_rect_eq : refl_id. (** The [refl_id] database should be populated with lemmas of the form [coerce_* t eq_refl = t]. *) @@ -178,7 +178,7 @@ Lemma inj_pairT2_refl A (x : A) (P : A -> Type) (p : P x) : Eqdep.EqdepTheory.inj_pairT2 A P x p p eq_refl = eq_refl. Proof. apply UIP_refl. Qed. -Hint Rewrite @JMeq_eq_refl @UIP_refl_refl @inj_pairT2_refl : refl_id. +Global Hint Rewrite @JMeq_eq_refl @UIP_refl_refl @inj_pairT2_refl : refl_id. Ltac rewrite_refl_id := autorewrite with refl_id. diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index 5a23a20811..620ed6b5b7 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -180,4 +180,4 @@ intros; rewrite Q2R_mult. rewrite Q2R_inv; auto. Qed. -Hint Rewrite Q2R_plus Q2R_mult Q2R_opp Q2R_minus Q2R_inv Q2R_div : q2r_simpl. +Global Hint Rewrite Q2R_plus Q2R_mult Q2R_opp Q2R_minus Q2R_inv Q2R_div : q2r_simpl. diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 4ac54d280a..c3e67b9d5a 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -53,7 +53,7 @@ Module Type CompareFacts (Import O:DecStrOrder'). rewrite compare_gt_iff; intuition. Qed. - Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order. + Global Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order. Instance compare_compat : Proper (eq==>eq==>Logic.eq) compare. Proof. diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index abf7f681b0..c709149109 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -146,7 +146,7 @@ Module MoreInt (Import I:Int). (** A magic (but costly) tactic that goes from [int] back to the [Z] friendly world ... *) - Hint Rewrite -> + Global Hint Rewrite -> i2z_0 i2z_1 i2z_2 i2z_3 i2z_add i2z_opp i2z_sub i2z_mul i2z_max i2z_eqb i2z_ltb i2z_leb : i2z. diff --git a/vernac/printmod.ml b/vernac/printmod.ml index fdf7f6c74a..ba4a7857e7 100644 --- a/vernac/printmod.ml +++ b/vernac/printmod.ml @@ -124,7 +124,7 @@ let print_mutual_inductive env mind mib udecl = let sigma = Evd.from_ctx (UState.of_binders bl) in hov 0 (def keyword ++ spc () ++ prlist_with_sep (fun () -> fnl () ++ str" with ") - (print_one_inductive env sigma mib) inds ++ + (print_one_inductive env sigma mib) inds ++ str "." ++ Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes) let get_fields = @@ -173,7 +173,7 @@ let print_record env mind mib udecl = prlist_with_sep (fun () -> str ";" ++ brk(2,0)) (fun (id,b,c) -> Id.print id ++ str (if b then " : " else " := ") ++ - Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++ + Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }." ++ Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes ) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4f3fc46c12..1c774a35bf 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1401,31 +1401,9 @@ let warn_implicit_core_hint_db = (fun () -> strbrk "Adding and removing hints in the core database implicitly is deprecated. " ++ strbrk"Please specify a hint database.") -let warn_deprecated_hint_without_locality = - CWarnings.create ~name:"deprecated-hint-without-locality" ~category:"deprecated" - (fun () -> strbrk "The default value for hint locality is currently \ - \"local\" in a section and \"global\" otherwise, but is scheduled to change \ - in a future release. For the time being, adding hints outside of sections \ - without specifying an explicit locality is therefore deprecated. It is \ - recommended to use \"export\" whenever possible.") - -let check_hint_locality = function -| OptGlobal -> - if Global.sections_are_opened () then - CErrors.user_err Pp.(str - "This command does not support the global attribute in sections."); -| OptExport -> - if Global.sections_are_opened () then - CErrors.user_err Pp.(str - "This command does not support the export attribute in sections."); -| OptDefault -> - if not @@ Global.sections_are_opened () then - warn_deprecated_hint_without_locality () -| OptLocal -> () - let vernac_remove_hints ~atts dbnames ids = let locality = Attributes.(parse option_locality atts) in - let () = check_hint_locality locality in + let () = Hints.check_hint_locality locality in let dbnames = if List.is_empty dbnames then (warn_implicit_core_hint_db (); ["core"]) @@ -1440,7 +1418,7 @@ let vernac_hints ~atts dbnames h = else dbnames in let locality, poly = Attributes.(parse Notations.(option_locality ++ polymorphic) atts) in - let () = check_hint_locality locality in + let () = Hints.check_hint_locality locality in Hints.add_hints ~locality dbnames (ComHints.interp_hints ~poly h) let vernac_syntactic_definition ~atts lid x only_parsing = |