diff options
68 files changed, 493 insertions, 338 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 8cf26ffaa6..a8ddb09a5d 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -10,7 +10,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2019-04-20-V1" + CACHEKEY: "bionic_coq-V2019-06-11-V1" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -50,10 +50,15 @@ WHAT DO YOU NEED ? findlib/ocamlfind as Coq's makefile will use it to locate the libraries during the build. + Debian / Ubuntu users can get the necessary system packages for + CoqIDE with: + + $ sudo apt-get install libgtksourceview-3.0-dev + Opam (https://opam.ocaml.org/) is recommended to install OCaml and the corresponding packages. - $ opam install num ocamlfind lablgtk conf-gtksourceview + $ opam install num ocamlfind lablgtk3-sourceview3 should get you a reasonable OCaml environment to compile Coq. diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index bba17314f7..e8c8d22678 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -11,7 +11,7 @@ git_download fiat_crypto # c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241 fiat_crypto_CI_TARGETS1="c-files printlite lite" -fiat_crypto_CI_TARGETS2="print-nobigmem nobigmem" +fiat_crypto_CI_TARGETS2="coq" ( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ ulimit -s 32768 && \ diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 8eebb3af64..818454dbbc 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2019-04-20-V1" +# CACHEKEY: "bionic_coq-V2019-06-11-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -38,7 +38,7 @@ ENV COMPILER="4.05.0" # `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.6.2 ounit.2.0.8 odoc.1.4.0" \ - CI_OPAM="menhir.20181113 elpi.1.2.0 ocamlgraph.1.8.8" + CI_OPAM="menhir.20181113 elpi.1.3.1 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. ENV COQIDE_OPAM="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5" diff --git a/dev/ci/user-overlays/10334-ppedrot-rm-kernel-sideeff-role.sh b/dev/ci/user-overlays/10334-ppedrot-rm-kernel-sideeff-role.sh new file mode 100644 index 0000000000..2c3f490c03 --- /dev/null +++ b/dev/ci/user-overlays/10334-ppedrot-rm-kernel-sideeff-role.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10334" ] || [ "$CI_BRANCH" = "rm-kernel-sideeff-role" ]; then + + equations_CI_REF=rm-kernel-sideeff-role + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/10358-gares-elpi13.sh b/dev/ci/user-overlays/10358-gares-elpi13.sh new file mode 100644 index 0000000000..d2ba9b5ddf --- /dev/null +++ b/dev/ci/user-overlays/10358-gares-elpi13.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10358" ] || [ "$CI_BRANCH" = "elpi-13-coq" ]; then + + elpi_CI_REF="elpi-13-coq" + elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi + +fi diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py index ff9b32fe78..0338cd42c7 100755 --- a/dev/tools/update-compat.py +++ b/dev/tools/update-compat.py @@ -73,8 +73,6 @@ FLAGS_ML_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.ml') COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'toplevel', 'coqargs.ml') G_VERNAC_PATH = os.path.join(ROOT_PATH, 'vernac', 'g_vernac.mlg') DOC_INDEX_PATH = os.path.join(ROOT_PATH, 'doc', 'stdlib', 'index-list.html.template') -BUG_4798_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', 'bug_4798.v') -BUG_9166_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', 'bug_9166.v') TEST_SUITE_RUN_PATH = os.path.join(ROOT_PATH, 'test-suite', 'tools', 'update-compat', 'run.sh') TEST_SUITE_PATHS = tuple(os.path.join(ROOT_PATH, 'test-suite', 'success', i) for i in ('CompatOldOldFlag.v', 'CompatOldFlag.v', 'CompatPreviousFlag.v', 'CompatCurrentFlag.v')) @@ -401,34 +399,6 @@ dev/tools/update-compat.py --assert-unchanged %s || exit $? ''' % ' '.join([('--master' if args['master'] else ''), ('--release' if args['release'] else '')]).strip() update_if_changed(contents, new_contents, TEST_SUITE_RUN_PATH, pass_through_shebang=True, **args) -def update_bug_4789(new_versions, **args): - # we always update this compat notation to oldest - # currently-supported compat version, which should never be the - # current version - with open(BUG_4798_PATH, 'r') as f: contents = f.read() - new_contents = BUG_HEADER + r"""Check match 2 with 0 => 0 | S n => n end. -Notation "|" := 1 (compat "%s"). -Check match 2 with 0 => 0 | S n => n end. (* fails *) -""" % new_versions[0] - update_if_changed(contents, new_contents, BUG_4798_PATH, **args) - -def update_bug_9166(new_versions, **args): - # we always update this compat notation to oldest - # currently-supported compat version, which should never be the - # current version - with open(BUG_9166_PATH, 'r') as f: contents = f.read() - new_contents = BUG_HEADER + r"""Set Warnings "+deprecated". - -Notation bar := option (compat "%s"). - -Definition foo (x: nat) : nat := - match x with - | 0 => 0 - | S bar => bar - end. -""" % new_versions[0] - update_if_changed(contents, new_contents, BUG_9166_PATH, **args) - def update_compat_notations_in(old_versions, new_versions, contents): for v in old_versions: if v not in new_versions: @@ -508,7 +478,5 @@ if __name__ == '__main__': update_test_suite(new_versions, **args) update_test_suite_run(**args) update_doc_index(new_versions, **args) - update_bug_4789(new_versions, **args) - update_bug_9166(new_versions, **args) update_compat_notations(known_versions, new_versions, **args) display_git_grep(known_versions, new_versions) diff --git a/doc/changelog/03-notations/10180-deprecate-notations.rst b/doc/changelog/03-notations/10180-deprecate-notations.rst new file mode 100644 index 0000000000..01f2e893ed --- /dev/null +++ b/doc/changelog/03-notations/10180-deprecate-notations.rst @@ -0,0 +1,6 @@ +- The :cmd:`Notation` and :cmd:`Infix` commands now support the `deprecated` + attribute. The former `compat` annotation for notations is + deprecated, and its semantics changed. It is now made equivalent to using + a `deprecated` attribute, and is no longer connected with the `-compat` + command-line flag. + (`#10180 <https://github.com/coq/coq/pull/10180>`_, by Maxime Dénès). diff --git a/doc/changelog/06-ssreflect/10302-case-HoTT.rst b/doc/changelog/06-ssreflect/10302-case-HoTT.rst new file mode 100644 index 0000000000..686b3c3cca --- /dev/null +++ b/doc/changelog/06-ssreflect/10302-case-HoTT.rst @@ -0,0 +1,7 @@ +- Make the ``case E: t`` tactic work together with + :flag:`Universe Polymorphism` and equality in :g:`Type`. + This makes tacn:`case` compatible with the HoTT + library https://github.com/HoTT/HoTT. + (`#10302 <https://github.com/coq/coq/pull/10302>`_, + fixes `#10301 <https://github.com/coq/coq/issues/10301>`_, + by Andreas Lynge, review by Enrico Tassi) diff --git a/doc/changelog/06-ssreflect/10305-unfold-HoTT.rst b/doc/changelog/06-ssreflect/10305-unfold-HoTT.rst new file mode 100644 index 0000000000..b82de1a879 --- /dev/null +++ b/doc/changelog/06-ssreflect/10305-unfold-HoTT.rst @@ -0,0 +1,7 @@ +- Make the ``rewrite /t`` tactic work together with + :flag:`Universe Polymorphism`. + This makes tacn:`rewrite` compatible with the HoTT + library https://github.com/HoTT/HoTT. + (`#10305 <https://github.com/coq/coq/pull/10305>`_, + fixes `#9336 <https://github.com/coq/coq/issues/9336>`_, + by Andreas Lynge, review by Enrico Tassi) diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index db4ebd5e38..ce3e10896c 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -120,7 +120,9 @@ reference manual. Here are the most important user-visible changes: - CoqIDE: - - CoqIDE now depends on gtk+3 and lablgtk3 instead of gtk+2 and lablgtk2 + - CoqIDE now depends on gtk+3 and lablgtk3 instead of gtk+2 and lablgtk2. + The INSTALL file available in the Coq sources has been updated to list + the new dependencies (`#9279 <https://github.com/coq/coq/pull/9279>`_, by Hugo Herbelin, with help from Jacques Garrigue, Emilio Jesús Gallego Arias, Michael Sogetrop and Vincent Laporte). diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index ebaa6fde66..38f6714f46 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1508,7 +1508,10 @@ the following attributes names are recognized: Takes as value the optional attributes ``since`` and ``note``; both have a string value. - This attribute can trigger the following warnings: + This attribute is supported by the following commands: :cmd:`Ltac`, + :cmd:`Tactic Notation`, :cmd:`Notation`, :cmd:`Infix`. + + It can trigger the following warnings: .. warn:: Tactic @qualid is deprecated since @string. @string. :undocumented: @@ -1516,6 +1519,11 @@ the following attributes names are recognized: .. warn:: Tactic Notation @qualid is deprecated since @string. @string. :undocumented: + .. warn:: Notation @string__1 is deprecated since @string__2. @string__3. + + :n:`@string__1` is the actual notation, :n:`@string__2` is the version number, + :n:`@string__3` is the note. + .. example:: .. coqtop:: all reset warn diff --git a/engine/evd.ml b/engine/evd.ml index 15b4c31851..34de2f41bb 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -430,6 +430,14 @@ type evar_flags = restricted_evars : Evar.t Evar.Map.t; typeclass_evars : Evar.Set.t } +type side_effect_role = +| Schema of inductive * string + +type side_effects = { + seff_private : Safe_typing.private_constants; + seff_roles : side_effect_role Cmap.t; +} + type evar_map = { (* Existential variables *) defn_evars : evar_info EvMap.t; @@ -444,7 +452,7 @@ type evar_map = { metas : clbinding Metamap.t; evar_flags : evar_flags; (** Interactive proofs *) - effects : Safe_typing.private_constants; + effects : side_effects; future_goals : Evar.t list; (** list of newly created evars, to be eventually turned into goals if not solved.*) principal_future_goal : Evar.t option; (** if [Some e], [e] must be @@ -672,6 +680,11 @@ let empty_evar_flags = restricted_evars = Evar.Map.empty; typeclass_evars = Evar.Set.empty } +let empty_side_effects = { + seff_private = Safe_typing.empty_private_constants; + seff_roles = Cmap.empty; +} + let empty = { defn_evars = EvMap.empty; undf_evars = EvMap.empty; @@ -680,7 +693,7 @@ let empty = { last_mods = Evar.Set.empty; evar_flags = empty_evar_flags; metas = Metamap.empty; - effects = Safe_typing.empty_private_constants; + effects = empty_side_effects; evar_names = EvNames.empty; (* id<->key for undefined evars *) future_goals = []; principal_future_goal = None; @@ -1011,12 +1024,17 @@ exception UniversesDiffer = UState.UniversesDiffer (**********************************************************) (* Side effects *) +let concat_side_effects eff eff' = { + seff_private = Safe_typing.concat_private eff.seff_private eff'.seff_private; + seff_roles = Cmap.fold Cmap.add eff.seff_roles eff'.seff_roles; +} + let emit_side_effects eff evd = - { evd with effects = Safe_typing.concat_private eff evd.effects; - universes = UState.emit_side_effects eff evd.universes } + let effects = concat_side_effects eff evd.effects in + { evd with effects; universes = UState.emit_side_effects eff.seff_private evd.universes } let drop_side_effects evd = - { evd with effects = Safe_typing.empty_private_constants; } + { evd with effects = empty_side_effects; } let eval_side_effects evd = evd.effects diff --git a/engine/evd.mli b/engine/evd.mli index 587a1de044..5478431e14 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -307,10 +307,22 @@ val dependent_evar_ident : Evar.t -> evar_map -> Id.t (** {5 Side-effects} *) -val emit_side_effects : Safe_typing.private_constants -> evar_map -> evar_map +type side_effect_role = +| Schema of inductive * string + +type side_effects = { + seff_private : Safe_typing.private_constants; + seff_roles : side_effect_role Cmap.t; +} + +val empty_side_effects : side_effects + +val concat_side_effects : side_effects -> side_effects -> side_effects + +val emit_side_effects : side_effects -> evar_map -> evar_map (** Push a side-effect into the evar map. *) -val eval_side_effects : evar_map -> Safe_typing.private_constants +val eval_side_effects : evar_map -> side_effects (** Return the effects contained in the evar map. *) val drop_side_effects : evar_map -> evar_map diff --git a/engine/proofview.mli b/engine/proofview.mli index 60697c1611..22e67357cd 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -381,7 +381,7 @@ val tclENV : Environ.env tactic (** {7 Put-like primitives} *) (** [tclEFFECTS eff] add the effects [eff] to the current state. *) -val tclEFFECTS : Safe_typing.private_constants -> unit tactic +val tclEFFECTS : Evd.side_effects -> unit tactic (** [mark_as_unsafe] declares the current tactic is unsafe. *) val mark_as_unsafe : unit tactic diff --git a/engine/uState.mli b/engine/uState.mli index 3df7f9e8e9..a34d4db8a6 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -100,7 +100,7 @@ val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t universes are preserved. *) val restrict : t -> Univ.LSet.t -> t -val demote_seff_univs : Safe_typing.private_constants Entries.definition_entry -> t -> t +val demote_seff_univs : 'a Entries.definition_entry -> t -> t type rigid = | UnivRigid diff --git a/interp/declare.ml b/interp/declare.ml index 7de92ded59..17de06ed57 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -42,7 +42,7 @@ type constant_obj = { cst_locl : import_status; } -type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind +type constant_declaration = Evd.side_effects constant_entry * logical_kind (* At load-time, the segment starting from the module name to the discharge *) (* section (if Remark or Fact) is needed to access a construction *) @@ -140,12 +140,12 @@ let register_constant kn kind local = let register_side_effect (c, role) = let () = register_constant c (IsProof Theorem) ImportDefaultBehavior in match role with - | Subproof -> () - | Schema (ind, kind) -> !declare_scheme kind [|ind,c|] + | None -> () + | Some (Evd.Schema (ind, kind)) -> !declare_scheme kind [|ind,c|] let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types - ?(univs=default_univ_entry) ?(eff=Safe_typing.empty_private_constants) body = + ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body = { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); const_entry_secctx = None; const_entry_type = types; @@ -154,7 +154,14 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types const_entry_feedback = None; const_entry_inline_code = inline} -let define_constant ?role ?(export_seff=false) id cd = +let get_roles export eff = + let map c = + let role = try Some (Cmap.find c eff.Evd.seff_roles) with Not_found -> None in + (c, role) + in + List.map map export + +let define_constant ~side_effect ?(export_seff=false) id cd = (* Logically define the constant and its subproofs, no libobject tampering *) let is_poly de = match de.const_entry_universes with | Monomorphic_entry _ -> false @@ -168,26 +175,39 @@ let define_constant ?role ?(export_seff=false) id cd = not de.const_entry_opaque || is_poly de -> (* This globally defines the side-effects in the environment. *) - let body, export = Global.export_private_constants ~in_section (Future.force de.const_entry_body) in + let body, eff = Future.force de.const_entry_body in + let body, export = Global.export_private_constants ~in_section (body, eff.Evd.seff_private) in + let export = get_roles export eff in let de = { de with const_entry_body = Future.from_val (body, ()) } in export, ConstantEntry (PureEntry, DefinitionEntry de) - | _ -> [], ConstantEntry (EffectEntry, cd) + | DefinitionEntry de -> + let map (body, eff) = body, eff.Evd.seff_private in + let body = Future.chain de.const_entry_body map in + let de = { de with const_entry_body = body } in + [], ConstantEntry (EffectEntry, DefinitionEntry de) + | ParameterEntry _ | PrimitiveEntry _ as cd -> + [], ConstantEntry (PureEntry, cd) in - let kn, eff = Global.add_constant ?role ~in_section id decl in + let kn, eff = Global.add_constant ~side_effect ~in_section id decl in kn, eff, export let declare_constant ?(internal = UserIndividualRequest) ?(local = ImportDefaultBehavior) id ?(export_seff=false) (cd, kind) = let () = check_exists id in - let kn, _eff, export = define_constant ~export_seff id cd in + let kn, (), export = define_constant ~side_effect:PureEntry ~export_seff id cd in (* Register the libobjects attached to the constants and its subproofs *) let () = List.iter register_side_effect export in let () = register_constant kn kind local in kn -let declare_private_constant ~role ?(internal=UserIndividualRequest) ?(local = ImportDefaultBehavior) id (cd, kind) = - let kn, eff, export = define_constant ~role id cd in +let declare_private_constant ?role ?(internal=UserIndividualRequest) ?(local = ImportDefaultBehavior) id (cd, kind) = + let kn, eff, export = define_constant ~side_effect:EffectEntry id cd in let () = assert (List.is_empty export) in let () = register_constant kn kind local in + let seff_roles = match role with + | None -> Cmap.empty + | Some r -> Cmap.singleton kn r + in + let eff = { Evd.seff_private = eff; Evd.seff_roles; } in kn, eff let declare_definition ?(internal=UserIndividualRequest) @@ -201,7 +221,7 @@ let declare_definition ?(internal=UserIndividualRequest) (** Declaration of section variables and local definitions *) type section_variable_entry = - | SectionLocalDef of Safe_typing.private_constants definition_entry + | SectionLocalDef of Evd.side_effects definition_entry | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) type variable_declaration = DirPath.t * section_variable_entry * logical_kind @@ -222,7 +242,9 @@ let cache_variable ((sp,_),o) = | SectionLocalDef (de) -> (* The body should already have been forced upstream because it is a section-local definition, but it's not enforced by typing *) - let ((body, uctx), eff) = Global.export_private_constants ~in_section:true (Future.force de.const_entry_body) in + let (body, eff) = Future.force de.const_entry_body in + let ((body, uctx), export) = Global.export_private_constants ~in_section:true (body, eff.Evd.seff_private) in + let eff = get_roles export eff in let () = List.iter register_side_effect eff in let poly, univs = match de.const_entry_universes with | Monomorphic_entry uctx -> false, uctx diff --git a/interp/declare.mli b/interp/declare.mli index 4120a82ca0..e2485d7cf0 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -23,7 +23,7 @@ open Decl_kinds (** Declaration of local constructions (Variable/Hypothesis/Local) *) type section_variable_entry = - | SectionLocalDef of Safe_typing.private_constants definition_entry + | SectionLocalDef of Evd.side_effects definition_entry | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) type variable_declaration = DirPath.t * section_variable_entry * logical_kind @@ -33,7 +33,7 @@ val declare_variable : variable -> variable_declaration -> Libobject.object_name (** Declaration of global constructions i.e. Definition/Theorem/Axiom/Parameter/... *) -type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind +type constant_declaration = Evd.side_effects constant_entry * logical_kind type internal_flag = | UserAutomaticRequest @@ -44,7 +44,7 @@ type internal_flag = val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:types -> ?univs:Entries.universes_entry -> - ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry + ?eff:Evd.side_effects -> constr -> Evd.side_effects definition_entry (** [declare_constant id cd] declares a global declaration (constant/parameter) with name [id] in the current section; it returns @@ -56,7 +56,7 @@ val declare_constant : ?internal:internal_flag -> ?local:import_status -> Id.t -> ?export_seff:bool -> constant_declaration -> Constant.t val declare_private_constant : - role:side_effect_role -> ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Safe_typing.private_constants + ?role:Evd.side_effect_role -> ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> diff --git a/interp/deprecation.ml b/interp/deprecation.ml new file mode 100644 index 0000000000..b6f0dceb89 --- /dev/null +++ b/interp/deprecation.ml @@ -0,0 +1,21 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +type t = { since : string option ; note : string option } + +let make ?since ?note () = { since ; note } + +let create_warning ~object_name ~warning_name name_printer = + let open Pp in + CWarnings.create ~name:warning_name ~category:"deprecated" + (fun (qid,depr) -> str object_name ++ spc () ++ name_printer qid ++ + strbrk " is deprecated" ++ + pr_opt (fun since -> str "since " ++ str since) depr.since ++ + str "." ++ pr_opt (fun note -> str note) depr.note) diff --git a/interp/deprecation.mli b/interp/deprecation.mli new file mode 100644 index 0000000000..aab87c11a2 --- /dev/null +++ b/interp/deprecation.mli @@ -0,0 +1,16 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +type t = { since : string option ; note : string option } + +val make : ?since:string -> ?note:string -> unit -> t + +val create_warning : object_name:string -> warning_name:string -> + ('b -> Pp.t) -> ?loc:Loc.t -> 'b * t -> unit diff --git a/interp/interp.mllib b/interp/interp.mllib index b65a171ef9..52978a2ab6 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -1,3 +1,4 @@ +Deprecation NumTok Constrexpr Tactypes diff --git a/interp/notation.ml b/interp/notation.ml index a7bac96d31..cc06d5abfc 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -72,6 +72,7 @@ type notation_location = (DirPath.t * DirPath.t) * string type notation_data = { not_interp : interpretation; not_location : notation_location; + not_deprecation : Deprecation.t option; } type scope = { @@ -1095,7 +1096,7 @@ let warn_notation_overridden = str "Notation" ++ spc () ++ pr_notation ntn ++ spc () ++ strbrk "was already used" ++ which_scope ++ str ".") -let declare_notation_interpretation ntn scopt pat df ~onlyprint = +let declare_notation_interpretation ntn scopt pat df ~onlyprint deprecation = let scope = match scopt with Some s -> s | None -> default_scope in let sc = find_scope scope in if not onlyprint then begin @@ -1109,6 +1110,7 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint = let notdata = { not_interp = pat; not_location = df; + not_deprecation = deprecation; } in let sc = { sc with notations = NotationMap.add ntn notdata sc.notations } in scope_map := String.Map.add scope sc !scope_map @@ -1125,10 +1127,10 @@ let declare_uninterpretation rule (metas,c as pat) = let rec find_interpretation ntn find = function | [] -> raise Not_found | Scope scope :: scopes -> - (try let (pat,df) = find scope in pat,(df,Some scope) + (try let n = find scope in (n,Some scope) with Not_found -> find_interpretation ntn find scopes) | SingleNotation ntn'::scopes when notation_eq ntn' ntn -> - (try let (pat,df) = find default_scope in pat,(df,None) + (try let n = find default_scope in (n,None) with Not_found -> (* e.g. because single notation only for constr, not cases_pattern *) find_interpretation ntn find scopes) @@ -1136,8 +1138,7 @@ let rec find_interpretation ntn find = function find_interpretation ntn find scopes let find_notation ntn sc = - let n = NotationMap.find ntn (find_scope sc).notations in - (n.not_interp, n.not_location) + NotationMap.find ntn (find_scope sc).notations let notation_of_prim_token = function | Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.to_string n @@ -1147,7 +1148,9 @@ let notation_of_prim_token = function let find_prim_token check_allowed ?loc p sc = (* Try for a user-defined numerical notation *) try - let (_,c),df = find_notation (notation_of_prim_token p) sc in + let n = find_notation (notation_of_prim_token p) sc in + let (_,c) = n.not_interp in + let df = n.not_location in let pat = Notation_ops.glob_constr_of_notation_constr ?loc c in check_allowed pat; pat, df @@ -1167,7 +1170,9 @@ let find_prim_token check_allowed ?loc p sc = let interp_prim_token_gen ?loc g p local_scopes = let scopes = make_current_scopes local_scopes in let p_as_ntn = try notation_of_prim_token p with Not_found -> InConstrEntrySomeLevel,"" in - try find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes + try + let (pat,loc), sc = find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes in + pat, (loc,sc) with Not_found -> user_err ?loc ~hdr:"interp_prim_token" ((match p with @@ -1192,11 +1197,18 @@ let rec check_allowed_ref_in_pat looked_for = DAst.(with_val (function let interp_prim_token_cases_pattern_expr ?loc looked_for p = interp_prim_token_gen ?loc (check_allowed_ref_in_pat looked_for) p +let warn_deprecated_notation = + Deprecation.create_warning ~object_name:"Notation" ~warning_name:"deprecated-notation" + pr_notation + let interp_notation ?loc ntn local_scopes = let scopes = make_current_scopes local_scopes in - try find_interpretation ntn (find_notation ntn) scopes + try + let (n,sc) = find_interpretation ntn (find_notation ntn) scopes in + Option.iter (fun d -> warn_deprecated_notation (ntn,d)) n.not_deprecation; + n.not_interp, (n.not_location, sc) with Not_found -> - user_err ?loc + user_err ?loc (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".") let uninterp_notations c = diff --git a/interp/notation.mli b/interp/notation.mli index a67948a778..b32561d908 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -217,7 +217,8 @@ type interp_rule = | SynDefRule of KerName.t val declare_notation_interpretation : notation -> scope_name option -> - interpretation -> notation_location -> onlyprint:bool -> unit + interpretation -> notation_location -> onlyprint:bool -> + Deprecation.t option -> unit val declare_uninterpretation : interp_rule -> interpretation -> unit diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index a7e1de736c..8df04187f1 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -19,20 +19,24 @@ open Notation_term (* Syntactic definitions. *) -type version = Flags.compat_version option +type syndef = + { syndef_pattern : interpretation; + syndef_onlyparsing : bool; + syndef_deprecation : Deprecation.t option; + } let syntax_table = - Summary.ref (KNmap.empty : (interpretation*version) KNmap.t) - ~name:"SYNTAXCONSTANT" + Summary.ref (KNmap.empty : syndef KNmap.t) + ~name:"SYNDEFS" -let add_syntax_constant kn c onlyparse = - syntax_table := KNmap.add kn (c,onlyparse) !syntax_table +let add_syntax_constant kn syndef = + syntax_table := KNmap.add kn syndef !syntax_table -let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = +let load_syntax_constant i ((sp,kn),(_local,syndef)) = if Nametab.exists_cci sp then user_err ~hdr:"cache_syntax_constant" (Id.print (basename sp) ++ str " already exists"); - add_syntax_constant kn pat onlyparse; + add_syntax_constant kn syndef; Nametab.push_syndef (Nametab.Until i) sp kn let is_alias_of_already_visible_name sp = function @@ -42,30 +46,29 @@ let is_alias_of_already_visible_name sp = function | _ -> false -let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = +let open_syntax_constant i ((sp,kn),(_local,syndef)) = + let pat = syndef.syndef_pattern in if not (Int.equal i 1 && is_alias_of_already_visible_name sp pat) then begin Nametab.push_syndef (Nametab.Exactly i) sp kn; - match onlyparse with - | None -> + if not syndef.syndef_onlyparsing then (* Redeclare it to be used as (short) name in case an other (distfix) notation was declared in between *) Notation.declare_uninterpretation (Notation.SynDefRule kn) pat - | _ -> () end let cache_syntax_constant d = load_syntax_constant 1 d; open_syntax_constant 1 d -let subst_syntax_constant (subst,(local,pat,onlyparse)) = - (local,Notation_ops.subst_interpretation subst pat,onlyparse) +let subst_syntax_constant (subst,(local,syndef)) = + let syndef_pattern = Notation_ops.subst_interpretation subst syndef.syndef_pattern in + (local, { syndef with syndef_pattern }) -let classify_syntax_constant (local,_,_ as o) = +let classify_syntax_constant (local,_ as o) = if local then Dispose else Substitute o -let in_syntax_constant - : bool * interpretation * Flags.compat_version option -> obj = - declare_object {(default_object "SYNTAXCONSTANT") with +let in_syntax_constant : (bool * syndef) -> obj = + declare_object {(default_object "SYNDEF") with cache_function = cache_syntax_constant; load_function = load_syntax_constant; open_function = open_syntax_constant; @@ -79,36 +82,31 @@ type syndef_interpretation = (Id.t * subscopes) list * notation_constr let in_pat (ids,ac) = (List.map (fun (id,sc) -> (id,((Constrexpr.InConstrEntrySomeLevel,sc),NtnTypeConstr))) ids,ac) let out_pat (ids,ac) = (List.map (fun (id,((_,sc),typ)) -> (id,sc)) ids,ac) -let declare_syntactic_definition local id onlyparse pat = - let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in () - -let pr_syndef kn = pr_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) - -let pr_compat_warning (kn, def, v) = - let pp_def = match def with - | [], NRef r -> spc () ++ str "is" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r - | _ -> strbrk " is a compatibility notation" +let declare_syntactic_definition ~local deprecation id ~onlyparsing pat = + let syndef = + { syndef_pattern = in_pat pat; + syndef_onlyparsing = onlyparsing; + syndef_deprecation = deprecation; + } in - pr_syndef kn ++ pp_def + let _ = add_leaf id (in_syntax_constant (local,syndef)) in () -let warn_compatibility_notation = - CWarnings.(create ~name:"compatibility-notation" - ~category:"deprecated" ~default:Enabled pr_compat_warning) +let pr_syndef kn = pr_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) -let verbose_compat ?loc kn def = function - | Some v when Flags.version_strictly_greater v -> - warn_compatibility_notation ?loc (kn, def, v) - | _ -> () +let warn_deprecated_syntactic_definition = + Deprecation.create_warning ~object_name:"Notation" ~warning_name:"deprecated-syntactic-definition" + pr_syndef let search_syntactic_definition ?loc kn = - let pat,v = KNmap.find kn !syntax_table in - let def = out_pat pat in - verbose_compat ?loc kn def v; + let syndef = KNmap.find kn !syntax_table in + let def = out_pat syndef.syndef_pattern in + Option.iter (fun d -> warn_deprecated_syntactic_definition (kn,d)) syndef.syndef_deprecation; def let search_filtered_syntactic_definition ?loc filter kn = - let pat,v = KNmap.find kn !syntax_table in - let def = out_pat pat in + let syndef = KNmap.find kn !syntax_table in + let def = out_pat syndef.syndef_pattern in let res = filter def in - (match res with Some _ -> verbose_compat ?loc kn def v | None -> ()); + if Option.has_some res then + Option.iter (fun d -> warn_deprecated_syntactic_definition (kn,d)) syndef.syndef_deprecation; res diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index 77873f8f67..e6e3b9cffa 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -15,8 +15,8 @@ open Notation_term type syndef_interpretation = (Id.t * subscopes) list * notation_constr -val declare_syntactic_definition : bool -> Id.t -> - Flags.compat_version option -> syndef_interpretation -> unit +val declare_syntactic_definition : local:bool -> Deprecation.t option -> Id.t -> + onlyparsing:bool -> syndef_interpretation -> unit val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> syndef_interpretation diff --git a/kernel/entries.ml b/kernel/entries.ml index adb3f6bd29..45b11e97ba 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -107,8 +107,3 @@ type module_entry = | MType of module_params_entry * module_struct_entry | MExpr of module_params_entry * module_struct_entry * module_struct_entry option - -(** Not used by the kernel. *) -type side_effect_role = - | Subproof - | Schema of inductive * string diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 824400b4e3..0b0f14eee7 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -232,7 +232,6 @@ type side_effect = { from_env : Declarations.structure_body CEphemeron.key; seff_constant : Constant.t; seff_body : Constr.t Declarations.constant_body; - seff_role : Entries.side_effect_role; } module SideEffects : @@ -536,8 +535,7 @@ type 'a effect_entry = type global_declaration = | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration -type exported_private_constant = - Constant.t * Entries.side_effect_role +type exported_private_constant = Constant.t let add_constant_aux ~in_section senv (kn, cb) = let l = Constant.label kn in @@ -699,7 +697,7 @@ let constant_entry_of_side_effect eff = const_entry_inline_code = cb.const_inline_code } let export_eff eff = - (eff.seff_constant, eff.seff_body, eff.seff_role) + (eff.seff_constant, eff.seff_body) let export_side_effects mb env (b_ctx, eff) = let not_exists e = @@ -750,9 +748,9 @@ let n_univs cb = match cb.const_universes with let export_private_constants ~in_section ce senv = let exported, ce = export_side_effects senv.revstruct senv.env ce in - let map (kn, cb, _) = (kn, map_constant (fun p -> Opaqueproof.create ~univs:(n_univs cb) (Future.from_val (p, Univ.ContextSet.empty))) cb) in + let map (kn, cb) = (kn, map_constant (fun p -> Opaqueproof.create ~univs:(n_univs cb) (Future.from_val (p, Univ.ContextSet.empty))) cb) in let bodies = List.map map exported in - let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in + let exported = List.map (fun (kn, _) -> kn) exported in let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in (ce, exported), senv @@ -762,7 +760,7 @@ let add_recipe ~in_section l r senv = let senv = add_constant_aux ~in_section senv (kn, cb) in kn, senv -let add_constant ?role ~in_section l decl senv = +let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl senv : (Constant.t * a) * safe_environment = let kn = Constant.make2 senv.modpath l in let cb = match decl with @@ -786,9 +784,9 @@ let add_constant ?role ~in_section l decl senv = add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv | _ -> senv in - let eff = match role with - | None -> empty_private_constants - | Some role -> + let eff : a = match side_effect with + | PureEntry -> () + | EffectEntry -> let body, univs = match cb.const_body with | (Primitive _ | Undef _) -> assert false | Def c -> (Def c, cb.const_universes) @@ -808,7 +806,6 @@ let add_constant ?role ~in_section l decl senv = from_env = from_env; seff_constant = kn; seff_body = cb; - seff_role = role; } in SideEffects.add eff empty_private_constants in diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 770caf5406..3e902303c3 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -87,18 +87,16 @@ type 'a effect_entry = type global_declaration = | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration -type exported_private_constant = - Constant.t * Entries.side_effect_role +type exported_private_constant = Constant.t val export_private_constants : in_section:bool -> private_constants Entries.proof_output -> (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer -(** returns the main constant plus a list of auxiliary constants (empty - unless one requires the side effects to be exported) *) +(** returns the main constant plus a certificate of its validity *) val add_constant : - ?role:Entries.side_effect_role -> in_section:bool -> Label.t -> global_declaration -> - (Constant.t * private_constants) safe_transformer + side_effect:'a effect_entry -> in_section:bool -> Label.t -> global_declaration -> + (Constant.t * 'a) safe_transformer val add_recipe : in_section:bool -> Label.t -> Cooking.recipe -> Constant.t safe_transformer diff --git a/library/global.ml b/library/global.ml index d5ffae7716..3f30a63808 100644 --- a/library/global.ml +++ b/library/global.ml @@ -94,7 +94,7 @@ let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b) let sprop_allowed () = Environ.sprop_allowed (env()) let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd) -let add_constant ?role ~in_section id d = globalize (Safe_typing.add_constant ?role ~in_section (i2l id) d) +let add_constant ~side_effect ~in_section id d = globalize (Safe_typing.add_constant ~side_effect ~in_section (i2l id) d) let add_recipe ~in_section id d = globalize (Safe_typing.add_recipe ~in_section (i2l id) d) let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie) let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) diff --git a/library/global.mli b/library/global.mli index eaa76c3117..c36cec3511 100644 --- a/library/global.mli +++ b/library/global.mli @@ -46,7 +46,7 @@ val export_private_constants : in_section:bool -> Constr.constr Univ.in_universe_context_set * Safe_typing.exported_private_constant list val add_constant : - ?role:Entries.side_effect_role -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * Safe_typing.private_constants + side_effect:'a Safe_typing.effect_entry -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * 'a val add_recipe : in_section:bool -> Id.t -> Cooking.recipe -> Constant.t val add_mind : Id.t -> Entries.mutual_inductive_entry -> MutInd.t diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 79d1c7520f..aad3967f6d 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -12,8 +12,8 @@ open Constr open Context open Context.Named.Declaration -let map_const_entry_body (f:constr->constr) (x:Safe_typing.private_constants Entries.const_entry_body) - : Safe_typing.private_constants Entries.const_entry_body = +let map_const_entry_body (f:constr->constr) (x: Evd.side_effects Entries.const_entry_body) + : Evd.side_effects Entries.const_entry_body = Future.chain x begin fun ((b,ctx),fx) -> (f b , ctx) , fx end diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index d1e540cceb..5363dc9a02 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -471,7 +471,7 @@ let get_funs_constant mp = exception No_graph_found exception Found_type of int -let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_constants definition_entry list = +let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects definition_entry list = let env = Global.env () in let funs = List.map fst fas in let first_fun = List.hd funs in @@ -597,7 +597,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ in {const with const_entry_body = - (Future.from_val (Safe_typing.mk_pure_proof princ_body)); + (Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects)); const_entry_type = Some scheme_type } ) diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index 97f9acdb3a..759c522820 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -34,7 +34,7 @@ val generate_functional_principle : exception No_graph_found val make_scheme : Evd.evar_map ref -> - (pconstant*Sorts.family) list -> Safe_typing.private_constants Entries.definition_entry list + (pconstant*Sorts.family) list -> Evd.side_effects Entries.definition_entry list val build_scheme : (Id.t*Libnames.qualid*Sorts.family) list -> unit val build_case_scheme : (Id.t*Libnames.qualid*Sorts.family) -> unit diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 9670cf1fa7..4078c34331 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -44,7 +44,7 @@ val jmeq_refl : unit -> EConstr.constr val save : Id.t - -> Safe_typing.private_constants Entries.definition_entry + -> Evd.side_effects Entries.definition_entry -> ?hook:Lemmas.declaration_hook -> UState.t -> Decl_kinds.goal_kind diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 309db539d0..2cc6f9a279 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -12,11 +12,10 @@ open Vernacexpr open Tacexpr -open Attributes (** {5 Tactic Definitions} *) -val register_ltac : locality_flag -> ?deprecation:deprecation -> +val register_ltac : locality_flag -> ?deprecation:Deprecation.t -> Tacexpr.tacdef_body list -> unit (** Adds new Ltac definitions to the environment. *) @@ -36,7 +35,7 @@ type argument = Genarg.ArgT.any Extend.user_symbol leaves. *) val add_tactic_notation : - locality_flag -> int -> ?deprecation:deprecation -> raw_argument + locality_flag -> int -> ?deprecation:Deprecation.t -> raw_argument grammar_tactic_prod_item_expr list -> raw_tactic_expr -> unit (** [add_tactic_notation local level prods expr] adds a tactic notation in the environment at level [level] with locality [local] made of the grammar @@ -49,7 +48,7 @@ val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type - to finding an argument by name (as in {!Genarg}) if there is none matching. *) -val add_ml_tactic_notation : ml_tactic_name -> level:int -> ?deprecation:deprecation -> +val add_ml_tactic_notation : ml_tactic_name -> level:int -> ?deprecation:Deprecation.t -> argument grammar_tactic_prod_item_expr list list -> unit (** A low-level variant of {!add_tactic_notation} used by the TACTIC EXTEND ML-side macro. *) @@ -80,7 +79,7 @@ type _ ty_sig = type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml val tactic_extend : string -> string -> level:Int.t -> - ?deprecation:deprecation -> ty_ml list -> unit + ?deprecation:Deprecation.t -> ty_ml list -> unit (** {5 ARGUMENT EXTEND} *) diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index d5f22b2c72..3347f594d2 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -55,7 +55,7 @@ type alias = KerName.t type alias_tactic = { alias_args: Id.t list; alias_body: glob_tactic_expr; - alias_deprecation: Attributes.deprecation option; + alias_deprecation: Deprecation.t option; } let alias_map = Summary.ref ~name:"tactic-alias" @@ -121,7 +121,7 @@ type ltac_entry = { tac_for_ml : bool; tac_body : glob_tactic_expr; tac_redef : ModPath.t list; - tac_deprecation : Attributes.deprecation option + tac_deprecation : Deprecation.t option } let mactab = @@ -178,7 +178,7 @@ let subst_md (subst, (local, id, b, t, deprecation)) = let classify_md (local, _, _, _, _ as o) = Substitute o let inMD : bool * ltac_constant option * bool * glob_tactic_expr * - Attributes.deprecation option -> obj = + Deprecation.t option -> obj = declare_object {(default_object "TAC-DEFINITION") with cache_function = cache_md; load_function = load_md; diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli index 5b98daf383..2fc45760d1 100644 --- a/plugins/ltac/tacenv.mli +++ b/plugins/ltac/tacenv.mli @@ -12,7 +12,6 @@ open Names open Libnames open Tacexpr open Geninterp -open Attributes (** This module centralizes the various ways of registering tactics. *) @@ -33,7 +32,7 @@ type alias = KerName.t type alias_tactic = { alias_args: Id.t list; alias_body: glob_tactic_expr; - alias_deprecation: deprecation option; + alias_deprecation: Deprecation.t option; } (** Contents of a tactic notation *) @@ -48,7 +47,7 @@ val check_alias : alias -> bool (** {5 Coq tactic definitions} *) -val register_ltac : bool -> bool -> ?deprecation:deprecation -> Id.t -> +val register_ltac : bool -> bool -> ?deprecation:Deprecation.t -> Id.t -> glob_tactic_expr -> unit (** Register a new Ltac with the given name and body. @@ -57,7 +56,7 @@ val register_ltac : bool -> bool -> ?deprecation:deprecation -> Id.t -> definition. It also puts the Ltac name in the nametab, so that it can be used unqualified. *) -val redefine_ltac : bool -> ?deprecation:deprecation -> KerName.t -> +val redefine_ltac : bool -> ?deprecation:Deprecation.t -> KerName.t -> glob_tactic_expr -> unit (** Replace a Ltac with the given name and body. If the boolean flag is set to true, then this is a local redefinition. *) @@ -68,7 +67,7 @@ val interp_ltac : KerName.t -> glob_tactic_expr val is_ltac_for_ml_tactic : KerName.t -> bool (** Whether the tactic is defined from ML-side *) -val tac_deprecation : KerName.t -> deprecation option +val tac_deprecation : KerName.t -> Deprecation.t option (** The tactic deprecation notice, if any *) type ltac_entry = { @@ -78,7 +77,7 @@ type ltac_entry = { (** The current body of the tactic *) tac_redef : ModPath.t list; (** List of modules redefining the tactic in reverse chronological order *) - tac_deprecation : deprecation option; + tac_deprecation : Deprecation.t option; (** Deprecation notice to be printed when the tactic is used *) } diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index c1f7fab123..7434f81946 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -119,18 +119,13 @@ let intern_constr_reference strict ist qid = (* Internalize an isolated reference in position of tactic *) let warn_deprecated_tactic = - CWarnings.create ~name:"deprecated-tactic" ~category:"deprecated" - (fun (qid,depr) -> str "Tactic " ++ pr_qualid qid ++ - strbrk " is deprecated" ++ - pr_opt (fun since -> str "since " ++ str since) depr.Attributes.since ++ - str "." ++ pr_opt (fun note -> str note) depr.Attributes.note) + Deprecation.create_warning ~object_name:"Tactic" ~warning_name:"deprecated-tactic" + pr_qualid let warn_deprecated_alias = - CWarnings.create ~name:"deprecated-tactic-notation" ~category:"deprecated" - (fun (kn,depr) -> str "Tactic Notation " ++ Pptactic.pr_alias_key kn ++ - strbrk " is deprecated since" ++ - pr_opt (fun since -> str "since " ++ str since) depr.Attributes.since ++ - str "." ++ pr_opt (fun note -> str note) depr.Attributes.note) + Deprecation.create_warning ~object_name:"Tactic Notation" + ~warning_name:"deprecated-tactic-notation" + Pptactic.pr_alias_key let intern_isolated_global_tactic_reference qid = let loc = qid.CAst.loc in diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 5df223215d..0662354daf 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -141,10 +141,10 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = let gk = Global ImportDefaultBehavior, poly, Proof Theorem in let ce, status, univs = build_constant_by_tactic id sigma sign ~goal_kind:gk typ tac in - let body = Future.force ce.const_entry_body in + let body, eff = Future.force ce.const_entry_body in let (cb, ctx) = - if side_eff then Safe_typing.inline_private_constants env body - else fst body + if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) + else body in let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in cb, status, univs @@ -195,5 +195,6 @@ let refine_by_tactic ~name ~poly env sigma ty tac = other goals that were already present during its invocation, so that those goals rely on effects that are not present anymore. Hopefully, this hack will work in most cases. *) + let neff = neff.Evd.seff_private in let (ans, _) = Safe_typing.inline_private_constants env ((ans, Univ.ContextSet.empty), neff) in ans, sigma diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 77d701b41f..63d5adfcd2 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -61,7 +61,7 @@ val use_unification_heuristics : unit -> bool val build_constant_by_tactic : Id.t -> UState.t -> named_context_val -> ?goal_kind:goal_kind -> EConstr.types -> unit Proofview.tactic -> - Safe_typing.private_constants Entries.definition_entry * bool * + Evd.side_effects Entries.definition_entry * bool * UState.t val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:polymorphic -> diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 8e1d16175f..96d90e9252 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -29,7 +29,7 @@ type lemma_possible_guards = int list list type proof_object = { id : Names.Id.t; - entries : Safe_typing.private_constants Entries.definition_entry list; + entries : Evd.side_effects Entries.definition_entry list; persistence : Decl_kinds.goal_kind; universes: UState.t; } @@ -134,7 +134,7 @@ let get_open_goals ps = (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) + List.length shelf -type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t +type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t let private_poly_univs = let b = ref true in @@ -172,7 +172,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now let body = c in let allow_deferred = not poly && (keep_body_ucst_separate || - not (Safe_typing.empty_private_constants = eff)) + not (Safe_typing.empty_private_constants = eff.Evd.seff_private)) in let typ = if allow_deferred then t else nf t in let used_univs_body = Vars.universes_of_constr body in diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index fd0ad6fb50..f84ec27df7 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -35,7 +35,7 @@ type lemma_possible_guards = int list list type proof_object = { id : Names.Id.t; - entries : Safe_typing.private_constants Entries.definition_entry list; + entries : Evd.side_effects Entries.definition_entry list; persistence : Decl_kinds.goal_kind; universes: UState.t; } @@ -80,7 +80,7 @@ val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future. * Both access the current proof state. The former is supposed to be * chained with a computation that completed the proof *) -type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t +type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t (* If allow_partial is set (default no) then an incomplete proof * is allowed (no error), and a warn is given if the proof is complete. *) diff --git a/proofs/refine.ml b/proofs/refine.ml index 8439156e65..d0e89183a8 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -60,7 +60,7 @@ let generic_refine ~typecheck f gl = let evs = Evd.save_future_goals sigma in (* Redo the effects in sigma in the monad's env *) let privates_csts = Evd.eval_side_effects sigma in - let env = Safe_typing.push_private_constants env privates_csts in + let env = Safe_typing.push_private_constants env privates_csts.Evd.seff_private in (* Check that the introduced evars are well-typed *) let fold accu ev = typecheck_evar ev env accu in let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in diff --git a/tactics/abstract.ml b/tactics/abstract.ml index e91fe5067c..967b0ef418 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -158,7 +158,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = (* do not compute the implicit arguments, it may be costly *) let () = Impargs.make_implicit_args false in (* ppedrot: seems legit to have abstracted subproofs as local*) - Declare.declare_private_constant ~role:Entries.Subproof ~internal:Declare.InternalTacticRequest ~local:ImportNeedQualified id decl + Declare.declare_private_constant ~internal:Declare.InternalTacticRequest ~local:ImportNeedQualified id decl in let cst, eff = Impargs.with_implicit_protection cst () in let inst = match const.Entries.const_entry_universes with @@ -173,8 +173,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = in let lem = mkConstU (cst, inst) in let evd = Evd.set_universe_context evd ectx in - let open Safe_typing in - let effs = concat_private eff + let effs = Evd.concat_side_effects eff Entries.(snd (Future.force const.const_entry_body)) in let solve = Proofview.tclEFFECTS effs <*> diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 8ead050262..06449c38a8 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -51,7 +51,7 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = else let sigma, pind = Evd.fresh_inductive_instance env sigma ind in let sigma, c = build_induction_scheme env sigma pind dep sort in - (c, Evd.evar_universe_context sigma), Safe_typing.empty_private_constants + (c, Evd.evar_universe_context sigma), Evd.empty_side_effects let build_induction_scheme_in_type dep sort ind = let env = Global.env () in @@ -62,15 +62,15 @@ let build_induction_scheme_in_type dep sort ind = let rect_scheme_kind_from_type = declare_individual_scheme_object "_rect_nodep" - (fun _ x -> build_induction_scheme_in_type false InType x, Safe_typing.empty_private_constants) + (fun _ x -> build_induction_scheme_in_type false InType x, Evd.empty_side_effects) let rect_scheme_kind_from_prop = declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop" - (fun _ x -> build_induction_scheme_in_type false InType x, Safe_typing.empty_private_constants) + (fun _ x -> build_induction_scheme_in_type false InType x, Evd.empty_side_effects) let rect_dep_scheme_kind_from_type = declare_individual_scheme_object "_rect" ~aux:"_rect_from_type" - (fun _ x -> build_induction_scheme_in_type true InType x, Safe_typing.empty_private_constants) + (fun _ x -> build_induction_scheme_in_type true InType x, Evd.empty_side_effects) let rec_scheme_kind_from_type = declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type" @@ -90,7 +90,7 @@ let ind_scheme_kind_from_type = let sind_scheme_kind_from_type = declare_individual_scheme_object "_sind_nodep" - (fun _ x -> build_induction_scheme_in_type false InSProp x, Safe_typing.empty_private_constants) + (fun _ x -> build_induction_scheme_in_type false InSProp x, Evd.empty_side_effects) let ind_dep_scheme_kind_from_type = declare_individual_scheme_object "_ind" ~aux:"_ind_from_type" @@ -98,7 +98,7 @@ let ind_dep_scheme_kind_from_type = let sind_dep_scheme_kind_from_type = declare_individual_scheme_object "_sind" ~aux:"_sind_from_type" - (fun _ x -> build_induction_scheme_in_type true InSProp x, Safe_typing.empty_private_constants) + (fun _ x -> build_induction_scheme_in_type true InSProp x, Evd.empty_side_effects) let ind_scheme_kind_from_prop = declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop" @@ -106,7 +106,7 @@ let ind_scheme_kind_from_prop = let sind_scheme_kind_from_prop = declare_individual_scheme_object "_sind" ~aux:"_sind_from_prop" - (fun _ x -> build_induction_scheme_in_type false InSProp x, Safe_typing.empty_private_constants) + (fun _ x -> build_induction_scheme_in_type false InSProp x, Evd.empty_side_effects) let nondep_elim_scheme from_kind to_kind = match from_kind, to_kind with @@ -130,24 +130,24 @@ let build_case_analysis_scheme_in_type dep sort ind = let case_scheme_kind_from_type = declare_individual_scheme_object "_case_nodep" - (fun _ x -> build_case_analysis_scheme_in_type false InType x, Safe_typing.empty_private_constants) + (fun _ x -> build_case_analysis_scheme_in_type false InType x, Evd.empty_side_effects) let case_scheme_kind_from_prop = declare_individual_scheme_object "_case" ~aux:"_case_from_prop" - (fun _ x -> build_case_analysis_scheme_in_type false InType x, Safe_typing.empty_private_constants) + (fun _ x -> build_case_analysis_scheme_in_type false InType x, Evd.empty_side_effects) let case_dep_scheme_kind_from_type = declare_individual_scheme_object "_case" ~aux:"_case_from_type" - (fun _ x -> build_case_analysis_scheme_in_type true InType x, Safe_typing.empty_private_constants) + (fun _ x -> build_case_analysis_scheme_in_type true InType x, Evd.empty_side_effects) let case_dep_scheme_kind_from_type_in_prop = declare_individual_scheme_object "_casep_dep" - (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Safe_typing.empty_private_constants) + (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Evd.empty_side_effects) let case_dep_scheme_kind_from_prop = declare_individual_scheme_object "_case_dep" - (fun _ x -> build_case_analysis_scheme_in_type true InType x, Safe_typing.empty_private_constants) + (fun _ x -> build_case_analysis_scheme_in_type true InType x, Evd.empty_side_effects) let case_dep_scheme_kind_from_prop_in_prop = declare_individual_scheme_object "_casep" - (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Safe_typing.empty_private_constants) + (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Evd.empty_side_effects) diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli index f60e6c137a..2b8a053cc0 100644 --- a/tactics/elimschemes.mli +++ b/tactics/elimschemes.mli @@ -18,7 +18,7 @@ val optimize_non_type_induction_scheme : Sorts.family -> 'b -> Names.inductive -> - (Constr.constr * UState.t) * Safe_typing.private_constants + (Constr.constr * UState.t) * Evd.side_effects val rect_scheme_kind_from_prop : individual scheme_kind val ind_scheme_kind_from_prop : individual scheme_kind diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 3fdd97616f..d66ae9cb24 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -229,7 +229,7 @@ let sym_scheme_kind = declare_individual_scheme_object "_sym_internal" (fun _ ind -> let c, ctx = build_sym_scheme (Global.env() (* side-effect! *)) ind in - (c, ctx), Safe_typing.empty_private_constants) + (c, ctx), Evd.empty_side_effects) (**********************************************************************) (* Build the involutivity of symmetry for an inductive type *) @@ -455,7 +455,7 @@ let build_l2r_rew_scheme dep env ind kind = else main_body)))))) in (c, UState.of_context_set ctx), - Safe_typing.concat_private eff' eff + Evd.concat_side_effects eff' eff (**********************************************************************) (* Build the left-to-right rewriting lemma for hypotheses associated *) @@ -708,7 +708,7 @@ let rew_l2r_dep_scheme_kind = (**********************************************************************) let rew_r2l_dep_scheme_kind = declare_individual_scheme_object "_rew_dep" - (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants) + (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Evd.empty_side_effects) (**********************************************************************) (* Dependent rewrite from right-to-left in hypotheses *) @@ -718,7 +718,7 @@ let rew_r2l_dep_scheme_kind = (**********************************************************************) let rew_r2l_forward_dep_scheme_kind = declare_individual_scheme_object "_rew_fwd_dep" - (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants) + (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Evd.empty_side_effects) (**********************************************************************) (* Dependent rewrite from left-to-right in hypotheses *) @@ -728,7 +728,7 @@ let rew_r2l_forward_dep_scheme_kind = (**********************************************************************) let rew_l2r_forward_dep_scheme_kind = declare_individual_scheme_object "_rew_fwd_r_dep" - (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants) + (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Evd.empty_side_effects) (**********************************************************************) (* Non-dependent rewrite from either left-to-right in conclusion or *) @@ -742,7 +742,7 @@ let rew_l2r_forward_dep_scheme_kind = let rew_l2r_scheme_kind = declare_individual_scheme_object "_rew_r" (fun _ ind -> fix_r2l_forward_rew_scheme - (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Safe_typing.empty_private_constants) + (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Evd.empty_side_effects) (**********************************************************************) (* Non-dependent rewrite from either right-to-left in conclusion or *) @@ -752,7 +752,7 @@ let rew_l2r_scheme_kind = (**********************************************************************) let rew_r2l_scheme_kind = declare_individual_scheme_object "_rew" - (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Safe_typing.empty_private_constants) + (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Evd.empty_side_effects) (* End of rewriting schemes *) @@ -836,4 +836,4 @@ let congr_scheme_kind = declare_individual_scheme_object "_congr" (fun _ ind -> (* May fail if equality is not defined *) build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, - Safe_typing.empty_private_constants) + Evd.empty_side_effects) diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli index 4749aebd96..c15fa146d4 100644 --- a/tactics/eqschemes.mli +++ b/tactics/eqschemes.mli @@ -27,7 +27,7 @@ val rew_r2l_scheme_kind : individual scheme_kind val build_r2l_rew_scheme : bool -> env -> inductive -> Sorts.family -> constr Evd.in_evar_universe_context val build_l2r_rew_scheme : bool -> env -> inductive -> Sorts.family -> - constr Evd.in_evar_universe_context * Safe_typing.private_constants + constr Evd.in_evar_universe_context * Evd.side_effects val build_r2l_forward_rew_scheme : bool -> env -> inductive -> Sorts.family -> constr Evd.in_evar_universe_context val build_l2r_forward_rew_scheme : @@ -39,7 +39,7 @@ val build_sym_scheme : env -> inductive -> constr Evd.in_evar_universe_context val sym_scheme_kind : individual scheme_kind val build_sym_involutive_scheme : env -> inductive -> - constr Evd.in_evar_universe_context * Safe_typing.private_constants + constr Evd.in_evar_universe_context * Evd.side_effects val sym_involutive_scheme_kind : individual scheme_kind (** Builds a congruence scheme for an equality type *) diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index b9485b8823..539fe31416 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -31,9 +31,9 @@ open Pp (* Registering schemes in the environment *) type mutual_scheme_object_function = - internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants + internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects type individual_scheme_object_function = - internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants + internal_flag -> inductive -> constr Evd.in_evar_universe_context * Evd.side_effects type 'a scheme_kind = string @@ -124,7 +124,7 @@ let define internal role id c poly univs = let entry = { const_entry_body = Future.from_val ((c,Univ.ContextSet.empty), - Safe_typing.empty_private_constants); + Evd.empty_side_effects); const_entry_secctx = None; const_entry_type = None; const_entry_universes = univs; @@ -145,10 +145,10 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = let id = match idopt with | Some id -> id | None -> add_suffix mib.mind_packets.(i).mind_typename suff in - let role = Entries.Schema (ind, kind) in + let role = Evd.Schema (ind, kind) in let const, neff = define mode role id c (Declareops.inductive_is_polymorphic mib) ctx in declare_scheme kind [|ind,const|]; - const, Safe_typing.concat_private neff eff + const, Evd.concat_side_effects neff eff let define_individual_scheme kind mode names (mind,i as ind) = match Hashtbl.find scheme_object_table kind with @@ -163,9 +163,9 @@ let define_mutual_scheme_base kind suff f mode names mind = try Int.List.assoc i names with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in let fold i effs id cl = - let role = Entries.Schema ((mind, i), kind)in + let role = Evd.Schema ((mind, i), kind)in let cst, neff = define mode role id cl (Declareops.inductive_is_polymorphic mib) ctx in - (Safe_typing.concat_private neff effs, cst) + (Evd.concat_side_effects neff effs, cst) in let (eff, consts) = Array.fold_left2_map_i fold eff ids cl in let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in @@ -180,7 +180,7 @@ let define_mutual_scheme kind mode names mind = let find_scheme_on_env_too kind ind = let s = String.Map.find kind (Indmap.find ind !scheme_map) in - s, Safe_typing.empty_private_constants + s, Evd.empty_side_effects let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) = try find_scheme_on_env_too kind ind diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli index 0eb4e47aeb..460b1f1b07 100644 --- a/tactics/ind_tables.mli +++ b/tactics/ind_tables.mli @@ -22,9 +22,9 @@ type individual type 'a scheme_kind type mutual_scheme_object_function = - internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants + internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects type individual_scheme_object_function = - internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants + internal_flag -> inductive -> constr Evd.in_evar_universe_context * Evd.side_effects (** Main functions to register a scheme builder *) @@ -39,13 +39,13 @@ val declare_individual_scheme_object : string -> ?aux:string -> val define_individual_scheme : individual scheme_kind -> internal_flag (** internal *) -> - Id.t option -> inductive -> Constant.t * Safe_typing.private_constants + Id.t option -> inductive -> Constant.t * Evd.side_effects val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) -> - (int * Id.t) list -> MutInd.t -> Constant.t array * Safe_typing.private_constants + (int * Id.t) list -> MutInd.t -> Constant.t array * Evd.side_effects (** Main function to retrieve a scheme in the cache or to generate it *) -val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t * Safe_typing.private_constants +val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t * Evd.side_effects val check_scheme : 'a scheme_kind -> inductive -> bool diff --git a/test-suite/bugs/closed/bug_4798.v b/test-suite/bugs/closed/bug_4798.v deleted file mode 100644 index f238086633..0000000000 --- a/test-suite/bugs/closed/bug_4798.v +++ /dev/null @@ -1,5 +0,0 @@ -(* DO NOT MODIFY THIS FILE DIRECTLY *) -(* It is autogenerated by dev/tools/update-compat.py. *) -Check match 2 with 0 => 0 | S n => n end. -Notation "|" := 1 (compat "8.8"). -Check match 2 with 0 => 0 | S n => n end. (* fails *) diff --git a/test-suite/bugs/closed/bug_9166.v b/test-suite/bugs/closed/bug_9166.v index 21cd770cbb..cd594c660f 100644 --- a/test-suite/bugs/closed/bug_9166.v +++ b/test-suite/bugs/closed/bug_9166.v @@ -1,8 +1,7 @@ -(* DO NOT MODIFY THIS FILE DIRECTLY *) -(* It is autogenerated by dev/tools/update-compat.py. *) Set Warnings "+deprecated". -Notation bar := option (compat "8.8"). +#[deprecated(since = "X", note = "Y")] +Notation bar := option. Definition foo (x: nat) : nat := match x with diff --git a/test-suite/success/NotationDeprecation.v b/test-suite/success/NotationDeprecation.v new file mode 100644 index 0000000000..d313ba0aa4 --- /dev/null +++ b/test-suite/success/NotationDeprecation.v @@ -0,0 +1,62 @@ +Module Syndefs. + +#[deprecated(since = "8.8", note = "Do not use.")] +Notation foo := Prop. + +Notation bar := Prop (compat "8.8"). + +Fail +#[deprecated(since = "8.8", note = "Do not use.")] +Notation zar := Prop (compat "8.8"). + +Check foo. +Check bar. + +Set Warnings "+deprecated". + +Fail Check foo. +Fail Check bar. + +End Syndefs. + +Module Notations. + +#[deprecated(since = "8.8", note = "Do not use.")] +Notation "!!" := Prop. + +Notation "##" := Prop (compat "8.8"). + +Fail +#[deprecated(since = "8.8", note = "Do not use.")] +Notation "**" := Prop (compat "8.8"). + +Check !!. +Check ##. + +Set Warnings "+deprecated". + +Fail Check !!. +Fail Check ##. + +End Notations. + +Module Infix. + +#[deprecated(since = "8.8", note = "Do not use.")] +Infix "!!" := plus (at level 1). + +Infix "##" := plus (at level 1, compat "8.8"). + +Fail +#[deprecated(since = "8.8", note = "Do not use.")] +Infix "**" := plus (at level 1, compat "8.8"). + +Check (_ !! _). +Check (_ ## _). + +Set Warnings "+deprecated". + +Fail Check (_ !! _). +Fail Check (_ ## _). + +End Infix. diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index 4576ff4cbe..bb4ed10bc9 100644 --- a/theories/Logic/Berardi.v +++ b/theories/Logic/Berardi.v @@ -149,6 +149,7 @@ apply AC_IF. Qed. -Notation classical_proof_irrelevence := classical_proof_irrelevance (compat "8.8"). +#[deprecated(since = "8.8", note = "Use classical_proof_irrelevance instead.")] +Notation classical_proof_irrelevence := classical_proof_irrelevance. End Berardis_paradox. diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 1ad5862d5d..ab14974598 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -73,11 +73,6 @@ module Notations = struct end open Notations -type deprecation = { since : string option ; note : string option } - -let mk_deprecation ?(since=None) ?(note=None) () = - { since ; note } - let assert_empty k v = if v <> VernacFlagEmpty then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments") @@ -213,19 +208,16 @@ let polymorphic = universe_transform ~warn_unqualified:true >> qualify_attribute ukey polymorphic_base -let deprecation_parser : deprecation key_parser = fun orig args -> +let deprecation_parser : Deprecation.t key_parser = fun orig args -> assert_once ~name:"deprecation" orig; match args with | VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ] | VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] -> - let since = Some since and note = Some note in - mk_deprecation ~since ~note () + Deprecation.make ~since ~note () | VernacFlagList [ "since", VernacFlagLeaf since ] -> - let since = Some since in - mk_deprecation ~since () + Deprecation.make ~since () | VernacFlagList [ "note", VernacFlagLeaf note ] -> - let note = Some note in - mk_deprecation ~note () + Deprecation.make ~note () | _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute") let deprecation = attribute_of_list ["deprecated",deprecation_parser] diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 44688ddafc..53caf49efd 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -43,15 +43,11 @@ end (** Definitions for some standard attributes. *) -type deprecation = { since : string option ; note : string option } - -val mk_deprecation : ?since: string option -> ?note: string option -> unit -> deprecation - val polymorphic : bool attribute val program : bool attribute val template : bool option attribute val locality : bool option attribute -val deprecation : deprecation option attribute +val deprecation : Deprecation.t option attribute val canonical : bool attribute val program_mode_option_name : string list diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 5aec5cac2c..2e84c3275b 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -195,7 +195,7 @@ let build_beq_scheme mode kn = let (c,a) = Reductionops.whd_betaiota_stack Evd.empty EConstr.(of_constr c) in let (c,a) = EConstr.Unsafe.(to_constr c, List.map to_constr a) in match Constr.kind c with - | Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants + | Rel x -> mkRel (x-nlist+ndx), Evd.empty_side_effects | Var x -> (* Support for working in a context with "eq_x : x -> x -> bool" *) let eid = Id.of_string ("eq_"^(Id.to_string x)) in @@ -203,11 +203,11 @@ let build_beq_scheme mode kn = try ignore (Environ.lookup_named eid env) with Not_found -> raise (ParameterWithoutEquality (VarRef x)) in - mkVar eid, Safe_typing.empty_private_constants + mkVar eid, Evd.empty_side_effects | Cast (x,_,_) -> aux (Term.applist (x,a)) | App _ -> assert false | Ind ((kn',i as ind'),u) (*FIXME: universes *) -> - if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Safe_typing.empty_private_constants + if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Evd.empty_side_effects else begin try let eq, eff = @@ -216,7 +216,7 @@ let build_beq_scheme mode kn = let eqa, eff = let eqa, effs = List.split (List.map aux a) in Array.of_list eqa, - List.fold_left Safe_typing.concat_private eff (List.rev effs) + List.fold_left Evd.concat_side_effects eff (List.rev effs) in let args = Array.append @@ -239,7 +239,7 @@ let build_beq_scheme mode kn = let kneq = Constant.change_label kn eq_lbl in try let _ = Environ.constant_opt_value_in env (kneq, u) in Term.applist (mkConst kneq,a), - Safe_typing.empty_private_constants + Evd.empty_side_effects with Not_found -> raise (ParameterWithoutEquality (ConstRef kn))) | Proj _ -> raise (EqUnknown "projection") | Construct _ -> raise (EqUnknown "constructor") @@ -270,7 +270,7 @@ let build_beq_scheme mode kn = let constrsi = constrs (3+nparrec) in let n = Array.length constrsi in let ar = Array.make n (ff ()) in - let eff = ref Safe_typing.empty_private_constants in + let eff = ref Evd.empty_side_effects in for i=0 to n-1 do let nb_cstr_args = List.length constrsi.(i).cs_args in let ar2 = Array.make n (ff ()) in @@ -288,7 +288,7 @@ let build_beq_scheme mode kn = (nb_cstr_args+ndx+1) cc in - eff := Safe_typing.concat_private eff' !eff; + eff := Evd.concat_side_effects eff' !eff; Array.set eqs ndx (mkApp (eqA, [|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|] @@ -320,7 +320,7 @@ let build_beq_scheme mode kn = let names = Array.make nb_ind (make_annot Anonymous Sorts.Relevant) and types = Array.make nb_ind mkSet and cores = Array.make nb_ind mkSet in - let eff = ref Safe_typing.empty_private_constants in + let eff = ref Evd.empty_side_effects in let u = Univ.Instance.empty in for i=0 to (nb_ind-1) do names.(i) <- make_annot (Name (Id.of_string (rec_name i))) Sorts.Relevant; @@ -328,7 +328,7 @@ let build_beq_scheme mode kn = (mkArrow (mkFullInd ((kn,i),u) 1) Sorts.Relevant (bb ())); let c, eff' = make_one_eq i in cores.(i) <- c; - eff := Safe_typing.concat_private eff' !eff + eff := Evd.concat_side_effects eff' !eff done; (Array.init nb_ind (fun i -> let kelim = Inductive.elim_sort (mib,mib.mind_packets.(i)) in @@ -938,7 +938,7 @@ let compute_dec_tact ind lnamesparrec nparrec = Not_found -> Tacticals.New.tclZEROMSG (str "Error during the decidability part, leibniz to boolean equality is required.") end >>= fun (lbI,eff'') -> - let eff = (Safe_typing.concat_private eff'' (Safe_typing.concat_private eff' eff)) in + let eff = (Evd.concat_side_effects eff'' (Evd.concat_side_effects eff' eff)) in Tacticals.New.tclTHENLIST [ Proofview.tclEFFECTS eff; intros_using fresh_first_intros; @@ -1005,7 +1005,7 @@ let make_eq_decidability mode mind = (EConstr.of_constr (compute_dec_goal (ind,u) lnamesparrec nparrec)) (compute_dec_tact ind lnamesparrec nparrec) in - ([|ans|], ctx), Safe_typing.empty_private_constants + ([|ans|], ctx), Evd.empty_side_effects let eq_dec_scheme_kind = declare_mutual_scheme_object "_eq_dec" make_eq_decidability diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 4cae4b8a74..1046e354a7 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -86,7 +86,7 @@ let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt = if program_mode then let env = Global.env () in let (c,ctx), sideff = Future.force ce.const_entry_body in - assert(Safe_typing.empty_private_constants = sideff); + assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private); assert(Univ.ContextSet.is_empty ctx); Obligations.check_evars env evd; let c = EConstr.of_constr c in diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index c3575594b6..0d9df47ee8 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -41,5 +41,5 @@ val interp_definition -> red_expr option -> constr_expr -> constr_expr option - -> Safe_typing.private_constants definition_entry * + -> Evd.side_effects definition_entry * Evd.evar_map * UState.universe_decl * Impargs.manual_implicits diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 3a25cb496c..6068cd90f1 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -286,7 +286,8 @@ let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximp let evd = Evd.restrict_universe_context evd vars in let ctx = Evd.check_univ_decl ~poly evd pl in let pl = Evd.universe_binders evd in - let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in + let mk_pure c = (c, Univ.ContextSet.empty), Evd.empty_side_effects in + let fixdecls = List.map mk_pure fixdecls in ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) @@ -316,7 +317,8 @@ let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fixi let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in let vars = Vars.universes_of_constr (List.hd fixdecls) in - let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in + let mk_pure c = (c, Univ.ContextSet.empty), Evd.empty_side_effects in + let fixdecls = List.map mk_pure fixdecls in let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 2b9d9567cd..909aa41a30 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -15,7 +15,7 @@ val declare_definition : Id.t -> definition_kind -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list) - -> Safe_typing.private_constants Entries.definition_entry + -> Evd.side_effects Entries.definition_entry -> UnivNames.universe_binders -> Impargs.manual_implicits -> GlobRef.t @@ -27,7 +27,7 @@ val declare_fix -> UnivNames.universe_binders -> Entries.universes_entry -> Id.t - -> Safe_typing.private_constants Entries.proof_output + -> Evd.side_effects Entries.proof_output -> Constr.types -> Impargs.manual_implicits -> GlobRef.t @@ -36,7 +36,7 @@ val prepare_definition : allow_evars:bool -> ?opaque:bool -> ?inline:bool -> poly:bool -> Evd.evar_map -> UState.universe_decl -> types:EConstr.t option -> body:EConstr.t -> - Evd.evar_map * Safe_typing.private_constants Entries.definition_entry + Evd.evar_map * Evd.side_effects Entries.definition_entry val prepare_parameter : allow_evars:bool -> poly:bool -> Evd.evar_map -> UState.universe_decl -> EConstr.types -> diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index de7d2fd49a..f18cf17bf9 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -414,7 +414,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort = let declare decl fi lrecref = let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in let decltype = EConstr.to_constr sigma decltype in - let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in + let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Evd.empty_side_effects) in let cst = define ~poly fi UserIndividualRequest sigma proof_output (Some decltype) in ConstRef cst :: lrecref in @@ -536,7 +536,7 @@ let do_combined_scheme name schemes = schemes in let sigma,body,typ = build_combined_scheme (Global.env ()) csts in - let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in + let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Evd.empty_side_effects) in (* It is possible for the constants to have different universe polymorphism from each other, however that is only when the user manually defined at least one of them (as Scheme would pick the diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 4e346a9564..a7366b2c56 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -112,7 +112,7 @@ let adjust_guardness_conditions const = function List.interval 0 (List.length ((lam_assum c)))) lemma_guard (Array.to_list fixdefs) in *) - let env = Safe_typing.push_private_constants env eff in + let env = Safe_typing.push_private_constants env eff.Evd.seff_private in let indexes = search_guard env possible_indexes fixdecls in diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 50914959dc..b96f500beb 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -732,13 +732,8 @@ type syntax_extension = { synext_notgram : notation_grammar; synext_unparsing : unparsing list; synext_extra : (string * string) list; - synext_compat : Flags.compat_version option; } -let is_active_compat = function -| None -> true -| Some v -> 0 <= Flags.version_compare v !Flags.compat_version - type syntax_extension_obj = locality_flag * syntax_extension let check_and_extend_constr_grammar ntn rule = @@ -759,7 +754,7 @@ let cache_one_syntax_extension se = let oldprec = Notgram_ops.level_of_notation ~onlyprint ntn in if not (Notgram_ops.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec; with Not_found -> - if is_active_compat se.synext_compat then begin + begin (* Reserve the notation level *) Notgram_ops.declare_notation_level ntn prec ~onlyprint; (* Declare the parsing rule *) @@ -934,10 +929,6 @@ let is_only_printing mods = let test = function SetOnlyPrinting -> true | _ -> false in List.exists test mods -let get_compat_version mods = - let test = function SetCompatVersion v -> Some v | _ -> None in - try Some (List.find_map test mods) with Not_found -> None - (* Compute precedences from modifiers (or find default ones) *) let set_entry_type from etyps (x,typ) = @@ -1177,7 +1168,7 @@ module SynData = struct (* Fields coming from the vernac-level modifiers *) only_parsing : bool; only_printing : bool; - compat : Flags.compat_version option; + deprecation : Deprecation.t option; format : lstring option; extra : (string * string) list; @@ -1222,12 +1213,32 @@ let check_locality_compatibility local custom i_typs = strbrk " which is local.")) (List.uniquize allcustoms) -let compute_syntax_data local df modifiers = +let warn_deprecated_compat = + CWarnings.create ~name:"deprecated-compat" ~category:"deprecated" + (fun () -> Pp.(str"The \"compat\" modifier is deprecated." ++ spc () ++ + str"Please use the \"deprecated\" attributed instead.")) + +(* Returns the new deprecation and the onlyparsing status. This should be +removed together with the compat syntax modifier. *) +let merge_compat_deprecation compat deprecation = + match compat, deprecation with + | Some Flags.Current, _ -> deprecation, true + | Some _, Some _ -> + CErrors.user_err Pp.(str"The \"compat\" modifier cannot be used with the \"deprecated\" attribute." + ++ spc () ++ str"Please use only the latter.") + | Some v, None -> + warn_deprecated_compat (); + Some (Deprecation.make ~since:(Flags.pr_version v) ()), true + | None, Some _ -> deprecation, true + | None, None -> deprecation, false + +let compute_syntax_data ~local deprecation df modifiers = let open SynData in let open NotationMods in let mods = interp_modifiers modifiers in let onlyprint = mods.only_printing in let onlyparse = mods.only_parsing in + let deprecation, _ = merge_compat_deprecation mods.compat deprecation in if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'."); let assoc = Option.append mods.assoc (Some Gramlib.Gramext.NonA) in let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint df in @@ -1265,7 +1276,7 @@ let compute_syntax_data local df modifiers = only_parsing = mods.only_parsing; only_printing = mods.only_printing; - compat = mods.compat; + deprecation; format = mods.format; extra = mods.extra; @@ -1281,9 +1292,9 @@ let compute_syntax_data local df modifiers = not_data = sy_fulldata; } -let compute_pure_syntax_data local df mods = +let compute_pure_syntax_data ~local df mods = let open SynData in - let sd = compute_syntax_data local df mods in + let sd = compute_syntax_data ~local None df mods in let msgs = if sd.only_parsing then (Feedback.msg_warning ?loc:None, @@ -1301,7 +1312,7 @@ type notation_obj = { notobj_coercion : entry_coercion_kind option; notobj_onlyparse : bool; notobj_onlyprint : bool; - notobj_compat : Flags.compat_version option; + notobj_deprecation : Deprecation.t option; notobj_notation : notation * notation_location; } @@ -1323,11 +1334,11 @@ let open_notation i (_, nobj) = let (ntn, df) = nobj.notobj_notation in let pat = nobj.notobj_interp in let onlyprint = nobj.notobj_onlyprint in + let deprecation = nobj.notobj_deprecation in let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in - let active = is_active_compat nobj.notobj_compat in - if Int.equal i 1 && fresh && active then begin + if Int.equal i 1 && fresh then begin (* Declare the interpretation *) - let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint in + let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in (* Declare the uninterpretation *) if not nobj.notobj_onlyparse then Notation.declare_uninterpretation (NotationRule (scope, ntn)) pat; @@ -1388,7 +1399,6 @@ let recover_notation_syntax ntn = synext_notgram = pa_rule; synext_unparsing = pp_rule; synext_extra = pp_extra_rules; - synext_compat = None; } with Not_found -> raise NoSyntaxRule @@ -1437,7 +1447,6 @@ let make_syntax_rules (sd : SynData.syn_data) = let open SynData in synext_notgram = { notgram_onlyprinting = sd.only_printing; notgram_rules = pa_rule }; synext_unparsing = pp_rule; synext_extra = sd.extra; - synext_compat = sd.compat; } (**********************************************************************) @@ -1447,9 +1456,9 @@ let to_map l = let fold accu (x, v) = Id.Map.add x v accu in List.fold_left fold Id.Map.empty l -let add_notation_in_scope local df env c mods scope = +let add_notation_in_scope ~local deprecation df env c mods scope = let open SynData in - let sd = compute_syntax_data local df mods in + let sd = compute_syntax_data ~local deprecation df mods in (* Prepare the interpretation *) (* Prepare the parsing and printing rules *) let sy_rules = make_syntax_rules sd in @@ -1470,7 +1479,7 @@ let add_notation_in_scope local df env c mods scope = notobj_onlyparse = onlyparse; notobj_coercion = coe; notobj_onlyprint = sd.only_printing; - notobj_compat = sd.compat; + notobj_deprecation = sd.deprecation; notobj_notation = sd.info; } in (* Ready to change the global state *) @@ -1479,7 +1488,7 @@ let add_notation_in_scope local df env c mods scope = Lib.add_anonymous_leaf (inNotation notation); sd.info -let add_notation_interpretation_core local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat = +let add_notation_interpretation_core ~local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint deprecation = let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint df in (* Recover types of variables and pa/pp rules; redeclare them if needed *) let level, i_typs, onlyprint = if not (is_numeral symbs) then begin @@ -1510,7 +1519,7 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_ notobj_onlyparse = onlyparse; notobj_coercion = coe; notobj_onlyprint = onlyprint; - notobj_compat = compat; + notobj_deprecation = deprecation; notobj_notation = df'; } in Lib.add_anonymous_leaf (inNotation notation); @@ -1518,41 +1527,40 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_ (* Notations without interpretation (Reserved Notation) *) -let add_syntax_extension local ({CAst.loc;v=df},mods) = let open SynData in - let psd = compute_pure_syntax_data local df mods in - let sy_rules = make_syntax_rules {psd with compat = None} in +let add_syntax_extension ~local ({CAst.loc;v=df},mods) = let open SynData in + let psd = compute_pure_syntax_data ~local df mods in + let sy_rules = make_syntax_rules {psd with deprecation = None} in Flags.if_verbose (List.iter (fun (f,x) -> f x)) psd.msgs; Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules)) (* Notations with only interpretation *) let add_notation_interpretation env ({CAst.loc;v=df},c,sc) = - let df' = add_notation_interpretation_core false df env c sc false false None in + let df' = add_notation_interpretation_core ~local:false df env c sc false false None in Dumpglob.dump_notation (loc,df') sc true let set_notation_for_interpretation env impls ({CAst.v=df},c,sc) = (try ignore - (Flags.silently (fun () -> add_notation_interpretation_core false df env ~impls c sc false false None) ()); + (Flags.silently (fun () -> add_notation_interpretation_core ~local:false df env ~impls c sc false false None) ()); with NoSyntaxRule -> user_err Pp.(str "Parsing rule for this notation has to be previously declared.")); Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc (* Main entry point *) -let add_notation local env c ({CAst.loc;v=df},modifiers) sc = +let add_notation ~local deprecation env c ({CAst.loc;v=df},modifiers) sc = let df' = if no_syntax_modifiers modifiers then (* No syntax data: try to rely on a previously declared rule *) let onlyparse = is_only_parsing modifiers in let onlyprint = is_only_printing modifiers in - let compat = get_compat_version modifiers in - try add_notation_interpretation_core local df env c sc onlyparse onlyprint compat + try add_notation_interpretation_core ~local df env c sc onlyparse onlyprint deprecation with NoSyntaxRule -> (* Try to determine a default syntax rule *) - add_notation_in_scope local df env c modifiers sc + add_notation_in_scope ~local deprecation df env c modifiers sc else (* Declare both syntax and interpretation *) - add_notation_in_scope local df env c modifiers sc + add_notation_in_scope ~local deprecation df env c modifiers sc in Dumpglob.dump_notation (loc,df') sc true @@ -1566,7 +1574,7 @@ let add_notation_extra_printing_rule df k v = let inject_var x = CAst.make @@ CRef (qualid_of_ident x,None) -let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc = +let add_infix ~local deprecation env ({CAst.loc;v=inf},modifiers) pr sc = check_infix_modifiers modifiers; (* check the precedence *) let vars = names_of_constr_expr pr in @@ -1575,7 +1583,7 @@ let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc = let metas = [inject_var x; inject_var y] in let c = mkAppC (pr,metas) in let df = CAst.make ?loc @@ Id.to_string x ^" "^(quote_notation_token inf)^" "^Id.to_string y in - add_notation local env c (df,modifiers) sc + add_notation ~local deprecation env c (df,modifiers) sc (**********************************************************************) (* Scopes, delimiters and classes bound to scopes *) @@ -1651,7 +1659,7 @@ let try_interp_name_alias = function | [], { CAst.v = CRef (ref,_) } -> intern_reference ref | _ -> raise Not_found -let add_syntactic_definition env ident (vars,c) local onlyparse = +let add_syntactic_definition ~local deprecation env ident (vars,c) compat = let vars,reversibility,pat = try [], APrioriReversible, NRef (try_interp_name_alias (vars,c)) with Not_found -> @@ -1665,11 +1673,9 @@ let add_syntactic_definition env ident (vars,c) local onlyparse = let map id = let (_,sc) = Id.Map.find id nvars in (id, sc) in List.map map vars, reversibility, pat in - let onlyparse = match onlyparse with - | None when fst (printability None false reversibility pat) -> Some Flags.Current - | p -> p - in - Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat) + let deprecation, onlyparsing = merge_compat_deprecation compat deprecation in + let onlyparsing = onlyparsing || fst (printability None false reversibility pat) in + Syntax_def.declare_syntactic_definition ~local deprecation ident ~onlyparsing (vars,pat) (**********************************************************************) (* Declaration of custom entry *) diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index 6435df23c7..6532cee367 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -19,10 +19,10 @@ val add_token_obj : string -> unit (** Adding a (constr) notation in the environment*) -val add_infix : locality_flag -> env -> (lstring * syntax_modifier list) -> +val add_infix : local:bool -> Deprecation.t option -> env -> (lstring * syntax_modifier list) -> constr_expr -> scope_name option -> unit -val add_notation : locality_flag -> env -> constr_expr -> +val add_notation : local:bool -> Deprecation.t option -> env -> constr_expr -> (lstring * syntax_modifier list) -> scope_name option -> unit val add_notation_extra_printing_rule : string -> string -> string -> unit @@ -47,12 +47,12 @@ val set_notation_for_interpretation : env -> Constrintern.internalization_env -> (** Add only the parsing/printing rule of a notation *) val add_syntax_extension : - locality_flag -> (lstring * syntax_modifier list) -> unit + local:bool -> (lstring * syntax_modifier list) -> unit (** Add a syntactic definition (as in "Notation f := ...") *) -val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr -> - bool -> Flags.compat_version option -> unit +val add_syntactic_definition : local:bool -> Deprecation.t option -> env -> + Id.t -> Id.t list * constr_expr -> Flags.compat_version option -> unit (** Print the Camlp5 state of a grammar *) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 6c9ec95c5f..50d24c20c9 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -497,7 +497,7 @@ let compute_possible_guardness_evidences n fixbody fixtype = let ctx = fst (decompose_prod_n_assum m fixtype) in List.map_i (fun i _ -> i) 0 ctx -let mk_proof c = ((c, Univ.ContextSet.empty), Safe_typing.empty_private_constants) +let mk_proof c = ((c, Univ.ContextSet.empty), Evd.empty_side_effects) let declare_mutual_definition l = let len = List.length l in @@ -632,7 +632,7 @@ let declare_obligation prg obl body ty uctx = if get_shrink_obligations () && not poly then shrink_body body ty else [], body, ty, [||] in - let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in + let body = ((body,Univ.ContextSet.empty), Evd.empty_side_effects) in let ce = { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body; const_entry_secctx = None; @@ -822,8 +822,8 @@ let solve_by_tac ?loc name evi t poly ctx = Pfedit.build_constant_by_tactic id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl t in let env = Global.env () in - let body = Future.force entry.const_entry_body in - let body = Safe_typing.inline_private_constants env body in + let (body, eff) = Future.force entry.const_entry_body in + let body = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body)); Some (fst body, entry.const_entry_type, Evd.evar_universe_context ctx') @@ -848,8 +848,8 @@ let obligation_terminator ?hook name num guard auto pf = | Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin let env = Global.env () in let ty = entry.Entries.const_entry_type in - let body = Future.force entry.const_entry_body in - let (body, cstr) = Safe_typing.inline_private_constants env body in + let body, eff = Future.force entry.const_entry_body in + let (body, cstr) = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in let sigma = Evd.from_ctx uctx in let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body); diff --git a/vernac/record.ml b/vernac/record.ml index 6101e13edd..c777ef2c2b 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -344,7 +344,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name flags f try let entry = { const_entry_body = - Future.from_val (Safe_typing.mk_pure_proof proj); + Future.from_val ((proj, Univ.ContextSet.empty), Evd.empty_side_effects); const_entry_secctx = None; const_entry_type = Some projtyp; const_entry_universes = ctx; diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index d206165e88..112c4b6451 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -81,7 +81,7 @@ module DefAttributes = struct locality : bool option; polymorphic : bool; program : bool; - deprecated : deprecation option; + deprecated : Deprecation.t option; } let parse f = @@ -92,6 +92,8 @@ module DefAttributes = struct { polymorphic; program; locality; deprecated } end +let module_locality = Attributes.Notations.(locality >>= fun l -> return (make_module_locality l)) + let with_locality ~atts f = let local = Attributes.(parse locality atts) in f ~local @@ -102,8 +104,7 @@ let with_section_locality ~atts f = f ~section_local let with_module_locality ~atts f = - let local = Attributes.(parse locality atts) in - let module_local = make_module_locality local in + let module_local = Attributes.(parse module_locality atts) in f ~module_local let with_def_attributes ~atts f = @@ -504,7 +505,7 @@ let dump_global r = let vernac_syntax_extension ~module_local infix l = if infix then Metasyntax.check_infix_modifiers (snd l); - Metasyntax.add_syntax_extension module_local l + Metasyntax.add_syntax_extension ~local:module_local l let vernac_declare_scope ~module_local sc = Metasyntax.declare_scope module_local sc @@ -523,11 +524,13 @@ let vernac_open_close_scope ~section_local (b,s) = let vernac_arguments_scope ~section_local r scl = Notation.declare_arguments_scope section_local (smart_global r) scl -let vernac_infix ~module_local = - Metasyntax.add_infix module_local (Global.env()) +let vernac_infix ~atts = + let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in + Metasyntax.add_infix ~local:module_local deprecation (Global.env()) -let vernac_notation ~module_local = - Metasyntax.add_notation module_local (Global.env()) +let vernac_notation ~atts = + let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in + Metasyntax.add_notation ~local:module_local deprecation (Global.env()) let vernac_custom_entry ~module_local s = Metasyntax.declare_custom_entry module_local s @@ -1265,9 +1268,10 @@ let vernac_hints ~atts dbnames h = let local = enforce_module_locality local in Hints.add_hints ~local dbnames (Hints.interp_hints poly h) -let vernac_syntactic_definition ~module_local lid x y = +let vernac_syntactic_definition ~atts lid x compat = + let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in Dumpglob.dump_definition lid false "syndef"; - Metasyntax.add_syntactic_definition (Global.env()) lid.v x module_local y + Metasyntax.add_syntactic_definition ~local:module_local deprecation (Global.env()) lid.v x compat let cache_bidi_hints (_name, (gr, ohint)) = match ohint with @@ -2379,9 +2383,9 @@ let translate_vernac ~atts v = let open Vernacextend in match v with | VernacOpenCloseScope (b, s) -> VtDefault(fun () -> with_section_locality ~atts vernac_open_close_scope (b,s)) | VernacInfix (mv,qid,sc) -> - VtDefault(fun () -> with_module_locality ~atts vernac_infix mv qid sc) + VtDefault(fun () -> vernac_infix ~atts mv qid sc) | VernacNotation (c,infpl,sc) -> - VtDefault(fun () -> with_module_locality ~atts vernac_notation c infpl sc) + VtDefault(fun () -> vernac_notation ~atts c infpl sc) | VernacNotationAddFormat(n,k,v) -> VtDefault(fun () -> unsupported_attributes atts; @@ -2559,8 +2563,7 @@ let translate_vernac ~atts v = let open Vernacextend in match v with VtDefault(fun () -> vernac_hints ~atts dbnames hints) | VernacSyntacticDefinition (id,c,b) -> - VtDefault(fun () -> - with_module_locality ~atts vernac_syntactic_definition id c b) + VtDefault(fun () -> vernac_syntactic_definition ~atts id c b) | VernacArguments (qid, args, more_implicits, nargs, bidi, flags) -> VtDefault(fun () -> with_section_locality ~atts (vernac_arguments qid args more_implicits nargs bidi flags)) |