diff options
| -rw-r--r-- | doc/changelog/07-commands-and-options/09530-rm-unknown.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 15 | ||||
| -rw-r--r-- | doc/sphinx/changes.rst | 7 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 2 | ||||
| -rw-r--r-- | test-suite/success/Typeclasses.v | 4 | ||||
| -rw-r--r-- | theories/Compat/Coq89.v | 1 | ||||
| -rw-r--r-- | vernac/classes.ml | 18 | ||||
| -rw-r--r-- | vernac/classes.mli | 1 |
8 files changed, 16 insertions, 38 deletions
diff --git a/doc/changelog/07-commands-and-options/09530-rm-unknown.rst b/doc/changelog/07-commands-and-options/09530-rm-unknown.rst new file mode 100644 index 0000000000..78874cadb1 --- /dev/null +++ b/doc/changelog/07-commands-and-options/09530-rm-unknown.rst @@ -0,0 +1,6 @@ +- Deprecated flag `Refine Instance Mode` has been removed. + (`#09530 <https://github.com/coq/coq/pull/09530>`_, fixes + `#3632 <https://github.com/coq/coq/issues/3632>`_, `#3890 + <https://github.com/coq/coq/issues/3890>`_ and `#4638 + <https://github.com/coq/coq/issues/4638>`_ + by Maxime Dénès, review by Gaëtan Gilbert). diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index ee417f269d..65934efaa6 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -316,7 +316,7 @@ Summary of the commands This command is used to declare a typeclass instance named :token:`ident` of the class :n:`@term__0` with parameters :token:`term` and fields defined by :token:`field_def`, where each field must be a declared field of - the class. Missing fields must be filled in interactive proof mode. + the class. An arbitrary context of :token:`binders` can be put after the name of the instance and before the colon to declare a parameterized instance. An @@ -563,19 +563,6 @@ Settings of goals. Setting this option to 1 or 2 turns on :flag:`Typeclasses Debug`; setting this option to 0 turns that option off. -.. flag:: Refine Instance Mode - - .. deprecated:: 8.10 - - This flag allows to switch the behavior of instance declarations made through - the Instance command. - - + When it is off (the default), they fail with an error instead. - - + When it is on, instances that have unsolved holes in - their proof-term silently open the proof mode with the remaining - obligations to prove. - Typeclasses eauto `:=` ~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 5e337bcef0..cc2c43e7dd 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -486,10 +486,9 @@ Other changes in 8.10+beta1 - :cmd:`Declare Instance` now requires an instance name. - The flag :flag:`Refine Instance Mode` has been turned off by default, - meaning that :cmd:`Instance` no longer opens a proof when a body is - provided. The flag has been deprecated and will be removed in the next - version. + The flag `Refine Instance Mode` has been turned off by default, meaning that + :cmd:`Instance` no longer opens a proof when a body is provided. The flag + has been deprecated and will be removed in the next version. (`#9270 <https://github.com/coq/coq/pull/9270>`_, and `#9825 <https://github.com/coq/coq/pull/9825>`_, diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index a68efa4713..963b7189f9 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1800,7 +1800,7 @@ let anew_instance ~pstate atts binders instance fields = let program_mode = atts.program in new_instance ~pstate ~program_mode atts.polymorphic binders instance (Some (true, CAst.make @@ CRecord (fields))) - ~global:atts.global ~generalize:false ~refine:false Hints.empty_hint_info + ~global:atts.global ~generalize:false Hints.empty_hint_info let declare_instance_refl ~pstate atts binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 3888cafed3..736d05fefc 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -198,9 +198,7 @@ Module UniqueInstances. for it. *) Set Typeclasses Unique Instances. Class Eq (A : Type) : Set. - Set Refine Instance Mode. - Instance eqa : Eq nat := _. constructor. Qed. - Unset Refine Instance Mode. + Instance eqa : Eq nat. Qed. Instance eqb : Eq nat := {}. Class Foo (A : Type) (e : Eq A) : Set. Instance fooa : Foo _ eqa := {}. diff --git a/theories/Compat/Coq89.v b/theories/Compat/Coq89.v index 05d63d9a47..49e0af9b2c 100644 --- a/theories/Compat/Coq89.v +++ b/theories/Compat/Coq89.v @@ -14,4 +14,3 @@ Local Set Warnings "-deprecated". Require Export Coq.Compat.Coq810. Unset Private Polymorphic Universes. -Set Refine Instance Mode. diff --git a/vernac/classes.ml b/vernac/classes.ml index ece9fc8937..05a75ab435 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -31,16 +31,6 @@ module NamedDecl = Context.Named.Declaration open Decl_kinds open Entries -let refine_instance = ref false - -let () = Goptions.(declare_bool_option { - optdepr = true; - optname = "definition of instances by refining"; - optkey = ["Refine";"Instance";"Mode"]; - optread = (fun () -> !refine_instance); - optwrite = (fun b -> refine_instance := b) -}) - let set_typeclass_transparency c local b = Hints.add_hints ~local [typeclasses_db] (Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b)) @@ -419,7 +409,7 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po | None -> pstate) ()) -let do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props = +let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props = let props = match props with | Some (true, { CAst.v = CRecord fs }) -> @@ -503,7 +493,7 @@ let do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program let term = to_constr sigma (Option.get term) in (declare_instance_constant k pri global imps ?hook id decl poly sigma term termtype; None) - else if program_mode || refine || Option.is_empty props then + else if program_mode || Option.is_empty props then declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype else CErrors.user_err Pp.(str "Unsolved obligations remaining.") in id, pstate @@ -550,7 +540,7 @@ let interp_instance_context ~program_mode env ctx ?(generalize=false) pl bk cl = sigma, cl, u, c', ctx', ctx, imps, args, decl -let new_instance ~pstate ?(global=false) ?(refine= !refine_instance) ~program_mode +let new_instance ~pstate ?(global=false) ~program_mode poly ctx (instid, bk, cl) props ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = let env = Global.env() in @@ -566,7 +556,7 @@ let new_instance ~pstate ?(global=false) ?(refine= !refine_instance) ~program_mo Namegen.next_global_ident_away i (Termops.vars_of_env env) in let env' = push_rel_context ctx env in - do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode + do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props let declare_new_instance ?(global=false) ~program_mode poly ctx (instid, bk, cl) pri = diff --git a/vernac/classes.mli b/vernac/classes.mli index e7f90ff306..57bb9ce312 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -48,7 +48,6 @@ val declare_instance_constant : val new_instance : pstate:Proof_global.t option -> ?global:bool (** Not global by default. *) -> - ?refine:bool (** Allow refinement *) -> program_mode:bool -> Decl_kinds.polymorphic -> local_binder_expr list -> |