aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/07-commands-and-options/09530-rm-unknown.rst6
-rw-r--r--doc/sphinx/addendum/type-classes.rst15
-rw-r--r--doc/sphinx/changes.rst7
-rw-r--r--plugins/ltac/g_rewrite.mlg2
-rw-r--r--plugins/ltac/rewrite.ml2
-rw-r--r--stm/stm.ml51
-rw-r--r--stm/vernac_classifier.ml36
-rw-r--r--test-suite/bugs/closed/bug_3890.v12
-rw-r--r--test-suite/bugs/closed/bug_4580.v1
-rw-r--r--test-suite/bugs/closed/bug_4638.v12
-rw-r--r--test-suite/bugs/opened/bug_3890.v22
-rw-r--r--test-suite/success/Typeclasses.v4
-rw-r--r--theories/Compat/Coq89.v1
-rw-r--r--vernac/classes.ml18
-rw-r--r--vernac/classes.mli1
-rw-r--r--vernac/vernacextend.ml1
-rw-r--r--vernac/vernacextend.mli1
17 files changed, 63 insertions, 129 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/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 469551809c..12b12bc7b0 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -278,7 +278,7 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
}
| #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ]
(* This command may or may not open a goal *)
- => { VtUnknown, VtNow }
+ => { (if Lib.is_modtype() then VtSideff([n]) else VtStartProof(GuaranteesOpacity, [n])), VtLater }
-> {
add_morphism_infer atts m n
}
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/stm/stm.ml b/stm/stm.ml
index 21618bc044..6f7cefb582 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -364,7 +364,6 @@ module VCS : sig
val set_parsing_state : id -> Vernacstate.Parser.state -> unit
val get_parsing_state : id -> Vernacstate.Parser.state option
val get_proof_mode : id -> Pvernac.proof_mode option
- val set_proof_mode : id -> Pvernac.proof_mode option -> unit
(* cuts from start -> stop, raising Expired if some nodes are not there *)
val slice : block_start:id -> block_stop:id -> vcs
@@ -572,6 +571,7 @@ end = struct (* {{{ *)
(match Vernacprop.under_control x with
| VernacDefinition (_,({CAst.v=Name i},_),_) -> Id.to_string i
| VernacStartTheoremProof (_,[({CAst.v=i},_),_]) -> Id.to_string i
+ | VernacInstance (_,(({CAst.v=Name i},_),_,_),_,_) -> Id.to_string i
| _ -> "branch")
let edit_branch = Branch.make "edit"
let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind
@@ -611,7 +611,6 @@ end = struct (* {{{ *)
info.state <- new_state
let get_proof_mode id = (get_info id).proof_mode
- let set_proof_mode id pm = (get_info id).proof_mode <- pm
let reached id =
let info = get_info id in
@@ -3050,53 +3049,6 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
VCS.set_parsing_state id parsing_state) new_ids;
`Ok
- (* Unknown: we execute it, check for open goals and propagate sideeff *)
- | VtUnknown, VtNow ->
- let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
- if not (get_allow_nested_proofs ()) && in_proof then
- "Commands which may open proofs are not allowed in a proof unless you turn option Nested Proofs Allowed on."
- |> Pp.str
- |> (fun s -> (UserError (None, s), Exninfo.null))
- |> State.exn_on ~valid:Stateid.dummy newtip
- |> Exninfo.iraise
- else
- let id = VCS.new_node ~id:newtip proof_mode () in
- let head_id = VCS.get_branch_pos head in
- let _st : unit = Reach.known_state ~doc ~cache:true head_id in (* ensure it is ok *)
- let step () =
- VCS.checkout VCS.Branch.master;
- let mid = VCS.get_branch_pos VCS.Branch.master in
- let _st' : unit = Reach.known_state ~doc ~cache:(VCS.is_interactive ()) mid in
- let st = Vernacstate.freeze_interp_state ~marshallable:false in
- ignore(stm_vernac_interp id st x);
- (* Vernac x may or may not start a proof *)
- if not in_proof && PG_compat.there_are_pending_proofs () then
- begin
- let bname = VCS.mk_branch_name x in
- let opacity_of_produced_term = function
- (* This AST is ambiguous, hence we check it dynamically *)
- | VernacInstance (_,_ , None, _) -> GuaranteesOpacity
- | _ -> Doesn'tGuaranteeOpacity in
- VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[]));
- VCS.set_proof_mode id (Some (Vernacentries.get_default_proof_mode ()));
- VCS.branch bname (`Proof (VCS.proof_nesting () + 1));
- end else begin
- begin match (VCS.get_branch head).VCS.kind with
- | `Edit _ -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
- | `Master -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
- | `Proof _ ->
- VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
- (* We hope it can be replayed, but we can't really know *)
- ignore(VCS.propagate_sideff ~action:(ReplayCommand x));
- end;
- VCS.checkout_shallowest_proof_branch ();
- end in
- State.define ~doc ~safe_id:head_id ~cache:true step id;
- Backtrack.record (); `Ok
-
- | VtUnknown, VtLater ->
- anomaly(str"classifier: VtUnknown must imply VtNow.")
-
| VtProofMode pm, VtNow ->
let proof_mode = Pvernac.lookup_proof_mode pm in
let id = VCS.new_node ~id:newtip proof_mode () in
@@ -3106,7 +3058,6 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
| VtProofMode _, VtLater ->
anomaly(str"classifier: VtProofMode must imply VtNow.")
-
end in
let pr_rc rc = match rc with
| `Ok -> Pp.(seq [str "newtip ("; str (Stateid.to_string (VCS.cur_tip ())); str ")"])
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 4a4c5c94e9..7cecd801e4 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -21,7 +21,6 @@ let string_of_parallel = function
| `No -> ""
let string_of_vernac_type = function
- | VtUnknown -> "Unknown"
| VtStartProof _ -> "StartProof"
| VtSideff _ -> "Sideff"
| VtQed (VtKeep VtKeepAxiom) -> "Qed(admitted)"
@@ -61,7 +60,7 @@ let options_affecting_stm_scheduling =
]
let classify_vernac e =
- let static_classifier ~poly e = match e with
+ let static_classifier ~atts e = match e with
(* Univ poly compatibility: we run it now, so that we can just
* look at Flags in stm.ml. Would be nicer to have the stm
* look at the entire dag to detect this option. *)
@@ -97,15 +96,18 @@ let classify_vernac e =
VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i), VtLater
| VernacDefinition (_,({v=i},_),ProveBody _) ->
- let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
- VtStartProof(guarantee, idents_of_name i), VtLater
+ let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
+ let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+ VtStartProof(guarantee, idents_of_name i), VtLater
| VernacStartTheoremProof (_,l) ->
- let ids = List.map (fun (({v=i}, _), _) -> i) l in
- let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
- VtStartProof (guarantee,ids), VtLater
+ let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
+ let ids = List.map (fun (({v=i}, _), _) -> i) l in
+ let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+ VtStartProof (guarantee,ids), VtLater
| VernacFixpoint (discharge,l) ->
+ let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
let guarantee =
- if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity
+ if discharge = Decl_kinds.DoDischarge || polymorphic then Doesn'tGuaranteeOpacity
else GuaranteesOpacity
in
let ids, open_proof =
@@ -115,8 +117,9 @@ let classify_vernac e =
then VtStartProof (guarantee,ids), VtLater
else VtSideff ids, VtLater
| VernacCoFixpoint (discharge,l) ->
+ let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
let guarantee =
- if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity
+ if discharge = Decl_kinds.DoDischarge || polymorphic then Doesn'tGuaranteeOpacity
else GuaranteesOpacity
in
let ids, open_proof =
@@ -185,8 +188,12 @@ let classify_vernac e =
| VernacDeclareMLModule _
| VernacContext _ (* TASSI: unsure *) -> VtSideff [], VtNow
| VernacProofMode pm -> VtProofMode pm, VtNow
- (* These are ambiguous *)
- | VernacInstance _ -> VtUnknown, VtNow
+ | VernacInstance (_,((name,_),_,_),None,_) when not (Attributes.parse_drop_extra Attributes.program atts) ->
+ let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
+ let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+ VtStartProof (guarantee, idents_of_name name.CAst.v), VtLater
+ | VernacInstance (_,((name,_),_,_),_,_) ->
+ VtSideff (idents_of_name name.CAst.v), VtLater
(* Stm will install a new classifier to handle these *)
| VernacBack _ | VernacAbortAll
| VernacUndoTo _ | VernacUndo _
@@ -201,9 +208,8 @@ let classify_vernac e =
with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
in
let rec static_control_classifier v = v |> CAst.with_val (function
- | VernacExpr (f, e) ->
- let poly = Attributes.(parse_drop_extra polymorphic_nowarn f) in
- static_classifier ~poly e
+ | VernacExpr (atts, e) ->
+ static_classifier ~atts e
| VernacTimeout (_,e) -> static_control_classifier e
| VernacTime (_,e) | VernacRedirect (_, e) ->
static_control_classifier e
@@ -214,6 +220,6 @@ let classify_vernac e =
| VtQed _, _ ->
VtProofStep { parallel = `No; proof_block_detection = None },
VtLater
- | (VtStartProof _ | VtUnknown | VtProofMode _), _ -> VtQuery, VtLater))
+ | (VtStartProof _ | VtProofMode _), _ -> VtQuery, VtLater))
in
static_control_classifier e
diff --git a/test-suite/bugs/closed/bug_3890.v b/test-suite/bugs/closed/bug_3890.v
new file mode 100644
index 0000000000..e1823ac54c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_3890.v
@@ -0,0 +1,12 @@
+Set Nested Proofs Allowed.
+
+Class Foo.
+Class Bar := b : Type.
+
+Instance foo : Foo.
+
+Instance bar : Bar.
+exact Type.
+Defined.
+
+Defined.
diff --git a/test-suite/bugs/closed/bug_4580.v b/test-suite/bugs/closed/bug_4580.v
index a8a446cc9b..3f40569d61 100644
--- a/test-suite/bugs/closed/bug_4580.v
+++ b/test-suite/bugs/closed/bug_4580.v
@@ -2,6 +2,5 @@ Require Import Program.
Class Foo (A : Type) := foo : A.
-Unset Refine Instance Mode.
Program Instance f1 : Foo nat := S _.
Next Obligation. exact 0. Defined.
diff --git a/test-suite/bugs/closed/bug_4638.v b/test-suite/bugs/closed/bug_4638.v
new file mode 100644
index 0000000000..951fe5302b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4638.v
@@ -0,0 +1,12 @@
+Set Nested Proofs Allowed.
+
+Class Foo.
+
+Goal True.
+
+Instance foo: Foo.
+Qed.
+
+trivial.
+
+Qed.
diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v
deleted file mode 100644
index 9d83743b2a..0000000000
--- a/test-suite/bugs/opened/bug_3890.v
+++ /dev/null
@@ -1,22 +0,0 @@
-Set Nested Proofs Allowed.
-
-Class Foo.
-Class Bar := b : Type.
-
-Set Refine Instance Mode.
-Instance foo : Foo := _.
-Unset Refine Instance Mode.
-(* 1 subgoals, subgoal 1 (ID 4)
-
- ============================
- Foo *)
-
-Instance bar : Bar.
-exact Type.
-Defined.
-(* bar is defined *)
-
-About foo.
-(* foo not a defined object. *)
-
-Fail Defined.
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 ->
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index ef06e59316..730f5fd6da 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -36,7 +36,6 @@ type vernac_type =
| VtProofMode of string
(* To be removed *)
| VtMeta
- | VtUnknown
and vernac_start = opacity_guarantee * Names.Id.t list
and vernac_sideff_type = Names.Id.t list
and opacity_guarantee =
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 4d89eaffd9..54e08d0e95 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -52,7 +52,6 @@ type vernac_type =
| VtProofMode of string
(* To be removed *)
| VtMeta
- | VtUnknown
and vernac_start = opacity_guarantee * Names.Id.t list
and vernac_sideff_type = Names.Id.t list
and opacity_guarantee =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:35:47 +0000