aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/dune (renamed from plugins/ltac/plugin_base.dune)2
-rw-r--r--plugins/ltac/extratactics.mlg20
-rw-r--r--plugins/ltac/g_auto.mlg2
-rw-r--r--plugins/ltac/g_ltac.mlg16
-rw-r--r--plugins/ltac/rewrite.ml2
-rw-r--r--plugins/ltac/tacentries.ml2
-rw-r--r--plugins/ltac/tacenv.ml2
-rw-r--r--plugins/ltac/tacinterp.ml10
-rw-r--r--plugins/ltac/tactic_option.ml11
9 files changed, 29 insertions, 38 deletions
diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/dune
index 5611f5ba16..6558ecbfe8 100644
--- a/plugins/ltac/plugin_base.dune
+++ b/plugins/ltac/dune
@@ -11,3 +11,5 @@
(synopsis "Coq's tauto tactic")
(modules tauto)
(libraries coq.plugins.ltac))
+
+(coq.pp (modules extratactics g_tactic g_rewrite g_eqdecide g_auto g_obligations g_ltac profile_ltac_tactics coretactics g_class extraargs))
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 9b80cbd803..7754fe401e 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -47,7 +47,7 @@ DECLARE PLUGIN "ltac_plugin"
let with_delayed_uconstr ist c tac =
let flags = {
- Pretyping.use_typeclasses = false;
+ Pretyping.use_typeclasses = Pretyping.NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
@@ -345,8 +345,8 @@ open EConstr
open Vars
let constr_flags () = {
- Pretyping.use_typeclasses = true;
- Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics ();
+ Pretyping.use_typeclasses = Pretyping.UseTC;
+ Pretyping.solve_unification_constraints = Proof.use_unification_heuristics ();
Pretyping.fail_evar = false;
Pretyping.expand_evars = true;
Pretyping.program_mode = false;
@@ -375,22 +375,22 @@ let refine_tac ist simple with_classes c =
TACTIC EXTEND refine
| [ "refine" uconstr(c) ] ->
- { refine_tac ist false true c }
+ { refine_tac ist false Pretyping.UseTC c }
END
TACTIC EXTEND simple_refine
| [ "simple" "refine" uconstr(c) ] ->
- { refine_tac ist true true c }
+ { refine_tac ist true Pretyping.UseTC c }
END
TACTIC EXTEND notcs_refine
| [ "notypeclasses" "refine" uconstr(c) ] ->
- { refine_tac ist false false c }
+ { refine_tac ist false Pretyping.NoUseTC c }
END
TACTIC EXTEND notcs_simple_refine
| [ "simple" "notypeclasses" "refine" uconstr(c) ] ->
- { refine_tac ist true false c }
+ { refine_tac ist true Pretyping.NoUseTC c }
END
(* Solve unification constraints using heuristics or fail if any remain *)
@@ -918,7 +918,7 @@ END
VERNAC COMMAND EXTEND GrabEvars STATE proof
| [ "Grab" "Existential" "Variables" ]
=> { classify_as_proofstep }
- -> { fun ~pstate -> Proof_global.map_proof (fun p -> Proof.V82.grab_evars p) pstate }
+ -> { fun ~pstate -> Declare.Proof.map_proof (fun p -> Proof.V82.grab_evars p) pstate }
END
(* Shelves all the goals under focus. *)
@@ -950,7 +950,7 @@ END
VERNAC COMMAND EXTEND Unshelve STATE proof
| [ "Unshelve" ]
=> { classify_as_proofstep }
- -> { fun ~pstate -> Proof_global.map_proof (fun p -> Proof.unshelve p) pstate }
+ -> { fun ~pstate -> Declare.Proof.map_proof (fun p -> Proof.unshelve p) pstate }
END
(* Gives up on the goals under focus: the goals are considered solved,
@@ -1102,7 +1102,7 @@ END
VERNAC COMMAND EXTEND OptimizeProof
| ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } ->
- { fun ~pstate -> Proof_global.compact_the_proof pstate }
+ { fun ~pstate -> Declare.Proof.compact pstate }
| [ "Optimize" "Heap" ] => { classify_as_proofstep } ->
{ Gc.compact () }
END
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 3c30c881fb..b4527694ae 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -53,7 +53,7 @@ END
let eval_uconstrs ist cs =
let flags = {
- Pretyping.use_typeclasses = false;
+ Pretyping.use_typeclasses = Pretyping.NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 50c3ed1248..e713ab13b2 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -359,23 +359,17 @@ open Vernacextend
open Goptions
open Libnames
-let print_info_trace = ref None
-
-let () = declare_int_option {
- optdepr = false;
- optkey = ["Info" ; "Level"];
- optread = (fun () -> !print_info_trace);
- optwrite = fun n -> print_info_trace := n;
-}
+let print_info_trace =
+ declare_intopt_option_and_ref ~depr:false ~key:["Info" ; "Level"]
let vernac_solve ~pstate n info tcom b =
let open Goal_select in
- let pstate, status = Proof_global.map_fold_proof_endline (fun etac p ->
+ let pstate, status = Declare.Proof.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
+ let info = Option.append info (print_info_trace ()) in
let (p,status) =
- Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
+ Proof.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
in
(* in case a strict subtree was completed,
go back to the top of the prooftree *)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index d72dcf8120..35e131020b 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -639,7 +639,7 @@ let solve_remaining_by env sigma holes by =
let env = Environ.reset_with_named_context evi.evar_hyps env in
let ty = evi.evar_concl in
let name, poly = Id.of_string "rewrite", false in
- let c, sigma = Pfedit.refine_by_tactic ~name ~poly env sigma ty solve_tac in
+ let c, sigma = Proof.refine_by_tactic ~name ~poly env sigma ty solve_tac in
Evd.define evk (EConstr.of_constr c) sigma
in
List.fold_left solve sigma indep
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 4127d28bae..9910796d9c 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -299,7 +299,7 @@ let classify_tactic_notation tacobj = Substitute tacobj
let inTacticGrammar : tactic_grammar_obj -> obj =
declare_object {(default_object "TacticGrammar") with
- open_function = open_tactic_notation;
+ open_function = simple_open open_tactic_notation;
load_function = load_tactic_notation;
cache_function = cache_tactic_notation;
subst_function = subst_tactic_notation;
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index ce9189792e..76d47f5482 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -182,7 +182,7 @@ let inMD : bool * ltac_constant option * bool * glob_tactic_expr *
declare_object {(default_object "TAC-DEFINITION") with
cache_function = cache_md;
load_function = load_md;
- open_function = open_md;
+ open_function = simple_open open_md;
subst_function = subst_md;
classify_function = classify_md}
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 9e0b9d3254..dda7f0742c 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -546,7 +546,7 @@ let interp_gen kind ist pattern_mode flags env sigma c =
(evd,c)
let constr_flags () = {
- use_typeclasses = true;
+ use_typeclasses = UseTC;
solve_unification_constraints = true;
fail_evar = true;
expand_evars = true;
@@ -564,7 +564,7 @@ let interp_constr = interp_constr_gen WithoutTypeConstraint
let interp_type = interp_constr_gen IsType
let open_constr_use_classes_flags () = {
- use_typeclasses = true;
+ use_typeclasses = UseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
@@ -573,7 +573,7 @@ let open_constr_use_classes_flags () = {
}
let open_constr_no_classes_flags () = {
- use_typeclasses = false;
+ use_typeclasses = NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
@@ -582,7 +582,7 @@ let open_constr_no_classes_flags () = {
}
let pure_open_constr_flags = {
- use_typeclasses = false;
+ use_typeclasses = NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = false;
@@ -2070,7 +2070,7 @@ let _ =
*)
let name, poly = Id.of_string "ltac_gen", poly in
let name, poly = Id.of_string "ltac_gen", poly in
- let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in
+ let (c, sigma) = Proof.refine_by_tactic ~name ~poly env sigma ty tac in
(EConstr.of_constr c, sigma)
in
GlobEnv.register_constr_interp0 wit_tactic eval
diff --git a/plugins/ltac/tactic_option.ml b/plugins/ltac/tactic_option.ml
index c72a527537..922d2f7792 100644
--- a/plugins/ltac/tactic_option.ml
+++ b/plugins/ltac/tactic_option.ml
@@ -13,15 +13,11 @@ open Pp
let declare_tactic_option ?(default=Tacexpr.TacId []) name =
let locality = Summary.ref false ~name:(name^"-locality") in
- let default_tactic_expr : Tacexpr.glob_tactic_expr ref =
- Summary.ref default ~name:(name^"-default-tacexpr")
- in
let default_tactic : Tacexpr.glob_tactic_expr ref =
- Summary.ref !default_tactic_expr ~name:(name^"-default-tactic")
+ Summary.ref default ~name:(name^"-default-tactic")
in
let set_default_tactic local t =
locality := local;
- default_tactic_expr := t;
default_tactic := t
in
let cache (_, (local, tac)) = set_default_tactic local tac in
@@ -36,18 +32,17 @@ let declare_tactic_option ?(default=Tacexpr.TacId []) name =
{ (default_object name) with
cache_function = cache;
load_function = (fun _ -> load);
- open_function = (fun _ -> load);
+ open_function = simple_open (fun _ -> load);
classify_function = (fun (local, tac) ->
if local then Dispose else Substitute (local, tac));
subst_function = subst}
in
let put local tac =
- set_default_tactic local tac;
Lib.add_anonymous_leaf (input (local, tac))
in
let get () = !locality, Tacinterp.eval_tactic !default_tactic in
let print () =
- Pptactic.pr_glob_tactic (Global.env ()) !default_tactic_expr ++
+ Pptactic.pr_glob_tactic (Global.env ()) !default_tactic ++
(if !locality then str" (locally defined)" else str" (globally defined)")
in
put, get, print
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 09:11:17 +0000