aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/scheme.ml2
-rw-r--r--plugins/funind/gen_principle.ml6
-rw-r--r--plugins/ltac/g_ltac.mlg50
-rw-r--r--plugins/ltac/pptactic.ml2
-rw-r--r--plugins/ltac/profile_ltac.ml4
-rw-r--r--plugins/ltac/tacinterp.ml16
-rw-r--r--plugins/ltac/tacinterp.mli6
7 files changed, 38 insertions, 48 deletions
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index ee50476b10..f671860bd5 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -28,7 +28,7 @@ let keywords =
"error"; "delay"; "force"; "_"; "__"]
Id.Set.empty
-let pp_comment s = str";; "++h 0 s++fnl ()
+let pp_comment s = str ";; " ++ h s ++ fnl ()
let pp_header_comment = function
| None -> mt ()
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 1ea803f561..012fcee486 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1860,13 +1860,13 @@ let do_generate_principle_aux pconstants on_error register_built
let warn_cannot_define_graph =
CWarnings.create ~name:"funind-cannot-define-graph" ~category:"funind"
(fun (names, error) ->
- Pp.(strbrk "Cannot define graph(s) for " ++ h 1 names ++ error))
+ Pp.(strbrk "Cannot define graph(s) for " ++ hv 1 names ++ error))
let warn_cannot_define_principle =
CWarnings.create ~name:"funind-cannot-define-principle" ~category:"funind"
(fun (names, error) ->
Pp.(
- strbrk "Cannot define induction principle(s) for " ++ h 1 names ++ error))
+ strbrk "Cannot define induction principle(s) for " ++ hv 1 names ++ error))
let warning_error names e =
let e_explain e =
@@ -1898,7 +1898,7 @@ let error_error names e =
CErrors.user_err
Pp.(
str "Cannot define graph(s) for "
- ++ h 1
+ ++ hv 1
(prlist_with_sep (fun _ -> str "," ++ spc ()) Ppconstr.pr_id names)
++ e_explain e)
| _ -> raise e
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index be0d71ad46..6cf5d30a95 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -355,28 +355,8 @@ GRAMMAR EXTEND Gram
open Stdarg
open Tacarg
open Vernacextend
-open Goptions
open Libnames
-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 = Declare.Proof.map_fold_endline ~f:(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 (p,status) =
- 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 *)
- let p = Proof.maximal_unfocus Vernacentries.command_focus p in
- p,status) pstate in
- if not status then Feedback.feedback Feedback.AddedAxiom;
- pstate
-
let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s
}
@@ -409,34 +389,34 @@ END
{
-let is_anonymous_abstract = function
- | TacAbstract (_,None) -> true
- | TacSolve [TacAbstract (_,None)] -> true
- | _ -> false
let rm_abstract = function
- | TacAbstract (t,_) -> t
- | TacSolve [TacAbstract (t,_)] -> TacSolve [t]
- | x -> x
+ | TacAbstract (t,_) -> t, true
+ | TacSolve [TacAbstract (t,_)] -> TacSolve [t], true
+ | x -> x, false
let is_explicit_terminator = function TacSolve _ -> true | _ -> false
}
VERNAC { tactic_mode } EXTEND VernacSolve STATE proof
-| [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+| [ ltac_selector_opt(g) ltac_info_opt(info) tactic(t) ltac_use_default(with_end_tac) ] =>
{ classify_as_proofstep } -> {
let g = Option.default (Goal_select.get_default_goal_selector ()) g in
- vernac_solve g n t def
+ let global = match g with Goal_select.SelectAll | Goal_select.SelectList _ -> true | _ -> false in
+ let t = ComTactic.I (Tacinterp.hide_interp, { Tacinterp.global; ast = t; }) in
+ ComTactic.solve g ~info t ~with_end_tac
}
-| [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+END
+
+VERNAC { tactic_mode } EXTEND VernacSolveParallel STATE proof
+| [ "par" ":" ltac_info_opt(info) tactic(t) ltac_use_default(with_end_tac) ] =>
{
- let anon_abstracting_tac = is_anonymous_abstract t in
let solving_tac = is_explicit_terminator t in
- let parallel = `Yes (solving_tac,anon_abstracting_tac) in
let pbr = if solving_tac then Some "par" else None in
- VtProofStep{ parallel = parallel; proof_block_detection = pbr }
+ VtProofStep{ proof_block_detection = pbr }
} -> {
- let t = rm_abstract t in
- vernac_solve Goal_select.SelectAll n t def
+ let t, abstract = rm_abstract t in
+ let t = ComTactic.I (Tacinterp.hide_interp, { Tacinterp.global = true; ast = t; }) in
+ ComTactic.solve_parallel ~info t ~abstract ~with_end_tac
}
END
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 85bb901046..cbb53497d3 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -179,7 +179,7 @@ let string_of_genarg_arg (ArgumentType arg) =
| ConstrTypeOf c ->
hov 1 (keyword "type of" ++ spc() ++ prc env sigma c)
| ConstrTerm c when test c ->
- h 0 (str "(" ++ prc env sigma c ++ str ")")
+ h (str "(" ++ prc env sigma c ++ str ")")
| ConstrTerm c ->
prc env sigma c
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 0dbf16a821..9c15d24dd3 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -146,7 +146,7 @@ let header =
fnl ()
let rec print_node ~filter all_total indent prefix (s, e) =
- h 0 (
+ h (
padr_with '-' 40 (prefix ^ s ^ " ")
++ padl 7 (format_ratio (e.local /. all_total))
++ padl 7 (format_ratio (e.total /. all_total))
@@ -212,7 +212,7 @@ let to_string ~filter ?(cutoff=0.0) node =
in
let filter s n = filter s && (all_total <= 0.0 || n /. all_total >= cutoff /. 100.0) in
let msg =
- h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++
+ h (str "total time: " ++ padl 11 (format_sec (all_total))) ++
fnl () ++
fnl () ++
header ++
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index ff6a36a049..eaeae50254 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1996,16 +1996,20 @@ let interp_tac_gen lfun avoid_ids debug t =
let interp t = interp_tac_gen Id.Map.empty Id.Set.empty (get_debug()) t
+(* MUST be marshallable! *)
+type tactic_expr = {
+ global: bool;
+ ast: Tacexpr.raw_tactic_expr;
+}
+
(* Used to hide interpretation for pretty-print, now just launch tactics *)
(* [global] means that [t] should be internalized outside of goals. *)
-let hide_interp global t ot =
+let hide_interp {global;ast} =
let hide_interp env =
let ist = Genintern.empty_glob_sign env in
- let te = intern_pure_tactic ist t in
+ let te = intern_pure_tactic ist ast in
let t = eval_tactic te in
- match ot with
- | None -> t
- | Some t' -> Tacticals.New.tclTHEN t t'
+ t
in
if global then
Proofview.tclENV >>= fun env ->
@@ -2015,6 +2019,8 @@ let hide_interp global t ot =
hide_interp (Proofview.Goal.env gl)
end
+let hide_interp = ComTactic.register_tactic_interpreter "ltac1" hide_interp
+
(***************************************************************************)
(** Register standard arguments *)
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index cbb17bf0fa..01d7306c9d 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -126,8 +126,12 @@ val interp_tac_gen : value Id.Map.t -> Id.Set.t ->
val interp : raw_tactic_expr -> unit Proofview.tactic
(** Hides interpretation for pretty-print *)
+type tactic_expr = {
+ global: bool;
+ ast: Tacexpr.raw_tactic_expr;
+}
-val hide_interp : bool -> raw_tactic_expr -> unit Proofview.tactic option -> unit Proofview.tactic
+val hide_interp : tactic_expr ComTactic.tactic_interpreter
(** Internals that can be useful for syntax extensions. *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 11:27:54 +0000