aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extraargs.mlg2
-rw-r--r--plugins/ltac/pptactic.ml14
-rw-r--r--plugins/ltac/pptactic.mli3
-rw-r--r--plugins/ltac/tacexpr.ml5
-rw-r--r--plugins/ltac/tacexpr.mli5
-rw-r--r--plugins/ltac/tacinterp.ml20
6 files changed, 18 insertions, 31 deletions
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index 156ee94a66..5d5d45c58f 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -314,7 +314,7 @@ END
let pr_by_arg_tac prtac opt_c = pr_by_arg_tac () () prtac opt_c
-let pr_in_clause _ _ _ cl = Pptactic.pr_in_clause Ppconstr.pr_lident cl
+let pr_in_clause _ _ _ cl = Pptactic.pr_in_clause Pputils.pr_lident cl
let pr_in_top_clause _ _ _ cl = Pptactic.pr_in_clause Id.print cl
let in_clause' = Pltac.in_clause
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 2267d43d93..5e3f4df192 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -22,8 +22,8 @@ open Tactypes
open Locus
open Decl_kinds
open Genredexpr
-open Pputils
open Ppconstr
+open Pputils
open Printer
open Genintern
@@ -159,8 +159,8 @@ let string_of_genarg_arg (ArgumentType arg) =
end
| _ -> default
- let pr_with_occurrences pr c = pr_with_occurrences pr keyword c
- let pr_red_expr pr c = pr_red_expr pr keyword c
+ let pr_with_occurrences pr c = Ppred.pr_with_occurrences pr keyword c
+ let pr_red_expr pr c = Ppred.pr_red_expr pr keyword c
let pr_may_eval test prc prlc pr2 pr3 = function
| ConstrEval (r,c) ->
@@ -186,12 +186,6 @@ let string_of_genarg_arg (ArgumentType arg) =
let pr_and_short_name pr (c,_) = pr c
- let pr_or_by_notation f = CAst.with_val (function
- | AN v -> f v
- | ByNotation (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc)
-
- let pr_located pr (_,x) = pr x
-
let pr_evaluable_reference = function
| EvalVarRef id -> pr_id id
| EvalConstRef sp -> pr_global (Globnames.ConstRef sp)
@@ -694,7 +688,7 @@ let pr_goal_selector ~toplevel s =
(* match t with
| CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal
| _ ->*)
- let s = prlist_with_sep spc Ppconstr.pr_lname nal ++ str ":" ++ pr.pr_lconstr t in
+ let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in
spc() ++ hov 1 (str"(" ++ s ++ str")") in
let pr_fix_tac (id,n,c) =
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 0ab9e501bc..bc47036d92 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -98,8 +98,7 @@ val pr_may_eval :
('a -> Pp.t) -> ('a -> Pp.t) -> ('b -> Pp.t) ->
('c -> Pp.t) -> ('a,'b,'c) Genredexpr.may_eval -> Pp.t
-val pr_and_short_name : ('a -> Pp.t) -> 'a Stdarg.and_short_name -> Pp.t
-val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t
+val pr_and_short_name : ('a -> Pp.t) -> 'a Genredexpr.and_short_name -> Pp.t
val pr_evaluable_reference_env : env -> evaluable_global_reference -> Pp.t
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 83f563e2ab..30e316b36d 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -270,7 +270,7 @@ constraint 'a = <
type g_trm = Genintern.glob_constr_and_expr
type g_pat = Genintern.glob_constr_pattern_and_expr
-type g_cst = evaluable_global_reference Stdarg.and_short_name or_var
+type g_cst = evaluable_global_reference Genredexpr.and_short_name or_var
type g_ref = ltac_constant located or_var
type g_nam = lident
@@ -296,9 +296,6 @@ type glob_tactic_arg =
(** Raw tactics *)
-type r_trm = constr_expr
-type r_pat = constr_pattern_expr
-type r_cst = qualid or_by_notation
type r_ref = qualid
type r_nam = lident
type r_lev = rlevel
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index da0ecfc449..8b6b14322b 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -269,7 +269,7 @@ constraint 'a = <
type g_trm = Genintern.glob_constr_and_expr
type g_pat = Genintern.glob_constr_pattern_and_expr
-type g_cst = evaluable_global_reference Stdarg.and_short_name or_var
+type g_cst = evaluable_global_reference Genredexpr.and_short_name or_var
type g_ref = ltac_constant located or_var
type g_nam = lident
@@ -295,9 +295,6 @@ type glob_tactic_arg =
(** Raw tactics *)
-type r_trm = constr_expr
-type r_pat = constr_pattern_expr
-type r_cst = qualid or_by_notation
type r_ref = qualid
type r_nam = lident
type r_lev = rlevel
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 816741b894..ae4cd06022 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -104,7 +104,7 @@ let pr_appl h vs =
let rec name_with_list appl t =
match appl with
| [] -> t
- | (h,vs)::l -> Proofview.Trace.name_tactic (fun () -> pr_appl h vs) (name_with_list l t)
+ | (h,vs)::l -> Proofview.Trace.name_tactic (fun _ _ -> pr_appl h vs) (name_with_list l t)
let name_if_glob appl t =
match appl with
| UnnamedAppl -> t
@@ -1050,7 +1050,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
return (hov 0 msg , hov 0 msg)
in
let print (_,msgnl) = Proofview.(tclLIFT (NonLogical.print_info msgnl)) in
- let log (msg,_) = Proofview.Trace.log (fun () -> msg) in
+ let log (msg,_) = Proofview.Trace.log (fun _ _ -> msg) in
let break = Proofview.tclLIFT (db_breakpoint (curr_debug ist) s) in
Ftactic.run msgnl begin fun msgnl ->
print msgnl <*> log msgnl <*> break
@@ -1132,7 +1132,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
in
let tac =
Ftactic.with_env interp_vars >>= fun (env, lr) ->
- let name () = Pptactic.pr_alias (fun v -> print_top_val env v) 0 s lr in
+ let name _ _ = Pptactic.pr_alias (fun v -> print_top_val env v) 0 s lr in
Proofview.Trace.name_tactic name (tac lr)
(* spiwack: this use of name_tactic is not robust to a
change of implementation of [Ftactic]. In such a situation,
@@ -1153,7 +1153,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
let tac = Tacenv.interp_ml_tactic opn in
let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in
let tac args =
- let name () = Pptactic.pr_extend (fun v -> print_top_val () v) 0 opn args in
+ let name _ _ = Pptactic.pr_extend (fun v -> print_top_val () v) 0 opn args in
Proofview.Trace.name_tactic name (catch_error_tac trace (tac args ist))
in
Ftactic.run args tac
@@ -1539,7 +1539,7 @@ and name_atomic ?env tacexpr tac : unit Proofview.tactic =
| None -> Proofview.tclENV
end >>= fun env ->
Proofview.tclEVARMAP >>= fun sigma ->
- let name () = Pptactic.pr_atomic_tactic env sigma tacexpr in
+ let name _ _ = Pptactic.pr_atomic_tactic env sigma tacexpr in
Proofview.Trace.name_tactic name tac
(* Interprets a primitive tactic *)
@@ -1560,7 +1560,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
end
| TacApply (a,ev,cb,cl) ->
(* spiwack: until the tactic is in the monad *)
- Proofview.Trace.name_tactic (fun () -> Pp.str"<apply>") begin
+ Proofview.Trace.name_tactic (fun _ _ -> Pp.str"<apply>") begin
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = project gl in
@@ -1601,7 +1601,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
end
| TacMutualFix (id,n,l) ->
(* spiwack: until the tactic is in the monad *)
- Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual fix>") begin
+ Proofview.Trace.name_tactic (fun _ _ -> Pp.str"<mutual fix>") begin
Proofview.Goal.enter begin fun gl ->
let env = pf_env gl in
let f sigma (id,n,c) =
@@ -1616,7 +1616,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
end
| TacMutualCofix (id,l) ->
(* spiwack: until the tactic is in the monad *)
- Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual cofix>") begin
+ Proofview.Trace.name_tactic (fun _ _ -> Pp.str"<mutual cofix>") begin
Proofview.Goal.enter begin fun gl ->
let env = pf_env gl in
let f sigma (id,c) =
@@ -1731,7 +1731,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
end
| TacChange (None,c,cl) ->
(* spiwack: until the tactic is in the monad *)
- Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin
+ Proofview.Trace.name_tactic (fun _ _ -> Pp.str"<change>") begin
Proofview.Goal.enter begin fun gl ->
let is_onhyps = match cl.onhyps with
| None | Some [] -> true
@@ -1756,7 +1756,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
end
| TacChange (Some op,c,cl) ->
(* spiwack: until the tactic is in the monad *)
- Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin
+ Proofview.Trace.name_tactic (fun _ _ -> Pp.str"<change>") begin
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = project gl in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 05:36:37 +0000