aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extratactics.mlg4
-rw-r--r--plugins/ltac/g_ltac.mlg2
-rw-r--r--plugins/ltac/rewrite.ml19
-rw-r--r--plugins/ltac/rewrite.mli6
-rw-r--r--plugins/ltac/tacentries.mli9
-rw-r--r--plugins/ltac/tacenv.ml6
-rw-r--r--plugins/ltac/tacenv.mli11
-rw-r--r--plugins/ltac/tacintern.ml15
8 files changed, 32 insertions, 40 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 0ded60d9c7..7691ca225e 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -934,7 +934,7 @@ END
VERNAC COMMAND EXTEND GrabEvars STATE proof
| [ "Grab" "Existential" "Variables" ]
=> { classify_as_proofstep }
- -> { fun ~pstate -> Proof_global.modify_proof (fun p -> Proof.V82.grab_evars p) pstate }
+ -> { fun ~pstate -> Proof_global.map_proof (fun p -> Proof.V82.grab_evars p) pstate }
END
(* Shelves all the goals under focus. *)
@@ -966,7 +966,7 @@ END
VERNAC COMMAND EXTEND Unshelve STATE proof
| [ "Unshelve" ]
=> { classify_as_proofstep }
- -> { fun ~pstate -> Proof_global.modify_proof (fun p -> Proof.unshelve p) pstate }
+ -> { fun ~pstate -> Proof_global.map_proof (fun p -> Proof.unshelve p) pstate }
END
(* Gives up on the goals under focus: the goals are considered solved,
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 960e5b76f8..d10d10a664 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -376,7 +376,7 @@ let () = declare_int_option {
let vernac_solve ~pstate n info tcom b =
let open Goal_select in
- let pstate, status = Proof_global.with_proof (fun etac p ->
+ let pstate, status = Proof_global.map_fold_proof_endline (fun etac p ->
let with_end_tac = if b then Some etac else None in
let global = match n with SelectAll | SelectList _ -> true | _ -> false in
let info = Option.append info !print_info_trace in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 7b286e69dc..2da6584aba 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -946,9 +946,9 @@ let fold_match ?(force=false) env sigma c =
if dep then case_dep_scheme_kind_from_prop
else case_scheme_kind_from_prop
else (
- if dep
- then case_dep_scheme_kind_from_type_in_prop
- else case_scheme_kind_from_type)
+ if dep
+ then case_dep_scheme_kind_from_type_in_prop
+ else case_scheme_kind_from_type)
else ((* sortc <> InProp by typing *)
if dep
then case_dep_scheme_kind_from_type
@@ -1962,7 +1962,6 @@ let add_setoid atts binders a aeq t n =
(qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
(qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]
-
let make_tactic name =
let open Tacexpr in
let tacqid = Libnames.qualid_of_string name in
@@ -1988,14 +1987,14 @@ let add_morphism_as_parameter atts m n : unit =
(PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst));
declare_projection n instance_id (ConstRef cst)
-let add_morphism_interactive atts m n : Proof_global.t =
+let add_morphism_interactive atts m n : Lemmas.t =
warn_add_morphism_deprecated ?loc:m.CAst.loc ();
init_setoid ();
let instance_id = add_suffix n "_Proper" in
let env = Global.env () in
let evd = Evd.from_env env in
let uctx, instance = build_morphism_signature env evd m in
- let kind = Decl_kinds.Global, atts.polymorphic,
+ let kind = Decl_kinds.Global Decl_kinds.ImportDefaultBehavior, atts.polymorphic,
Decl_kinds.DefinitionBody Decl_kinds.Instance
in
let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
@@ -2010,8 +2009,8 @@ let add_morphism_interactive atts m n : Proof_global.t =
let hook = Lemmas.mk_hook hook in
Flags.silently
(fun () ->
- let pstate = Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
- fst Pfedit.(by (Tacinterp.interp tac) pstate)) ()
+ let lemma = Lemmas.start_lemma ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
+ fst (Lemmas.by (Tacinterp.interp tac) lemma)) ()
let add_morphism atts binders m s n =
init_setoid ();
@@ -2023,12 +2022,12 @@ let add_morphism atts binders m s n =
[cHole; s; m])
in
let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
- let _id, pstate = Classes.new_instance_interactive
+ let _id, lemma = Classes.new_instance_interactive
~global:atts.global atts.polymorphic
instance_name binders instance_t
~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info
in
- pstate (* no instance body -> always open proof *)
+ lemma (* no instance body -> always open proof *)
(** Bind to "rewrite" too *)
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 3ef33c6dc9..a5c3782b30 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -101,16 +101,16 @@ val add_setoid
-> Id.t
-> unit
-val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t
+val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Lemmas.t
val add_morphism_as_parameter : rewrite_attributes -> constr_expr -> Id.t -> unit
val add_morphism
- : rewrite_attributes
+ : rewrite_attributes
-> local_binder_expr list
-> constr_expr
-> constr_expr
-> Id.t
- -> Proof_global.t
+ -> Lemmas.t
val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 09:48:05 +0000