aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/proofview.ml20
-rw-r--r--engine/proofview.mli2
-rw-r--r--engine/proofview_monad.ml31
-rw-r--r--engine/proofview_monad.mli4
4 files changed, 27 insertions, 30 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 8c15579bb0..cf4224bbdb 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -636,7 +636,7 @@ let shelve =
let open Proof in
Comb.get >>= fun initial ->
Comb.set [] >>
- InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve")) >>
+ InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"shelve")) >>
Shelf.modify (fun gls -> gls @ CList.map drop_state initial)
let shelve_goals l =
@@ -644,7 +644,7 @@ let shelve_goals l =
Comb.get >>= fun initial ->
let comb = CList.filter (fun g -> not (CList.mem (drop_state g) l)) initial in
Comb.set comb >>
- InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_goals")) >>
+ InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"shelve_goals")) >>
Shelf.modify (fun gls -> gls @ l)
(** [depends_on sigma src tgt] checks whether the goal [src] appears
@@ -710,7 +710,7 @@ let shelve_unifiable_informative =
Pv.get >>= fun initial ->
let (u,n) = partition_unifiable initial.solution initial.comb in
Comb.set n >>
- InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_unifiable")) >>
+ InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"shelve_unifiable")) >>
let u = CList.map drop_state u in
Shelf.modify (fun gls -> gls @ u) >>
tclUNIT u
@@ -794,7 +794,7 @@ let goodmod p m =
let cycle n =
let open Proof in
- InfoL.leaf (Info.Tactic (fun () -> Pp.(str"cycle "++int n))) >>
+ InfoL.leaf (Info.Tactic (fun _ _ -> Pp.(str"cycle "++int n))) >>
Comb.modify begin fun initial ->
let l = CList.length initial in
let n' = goodmod n l in
@@ -804,7 +804,7 @@ let cycle n =
let swap i j =
let open Proof in
- InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"swap"++spc()++int i++spc()++int j)))) >>
+ InfoL.leaf (Info.Tactic (fun _ _ -> Pp.(hov 2 (str"swap"++spc()++int i++spc()++int j)))) >>
Comb.modify begin fun initial ->
let l = CList.length initial in
let i = if i>0 then i-1 else i and j = if j>0 then j-1 else j in
@@ -819,7 +819,7 @@ let swap i j =
let revgoals =
let open Proof in
- InfoL.leaf (Info.Tactic (fun () -> Pp.str"revgoals")) >>
+ InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"revgoals")) >>
Comb.modify CList.rev
let numgoals =
@@ -858,7 +858,7 @@ let give_up =
Comb.get >>= fun initial ->
Comb.set [] >>
mark_as_unsafe >>
- InfoL.leaf (Info.Tactic (fun () -> Pp.str"give_up")) >>
+ InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"give_up")) >>
Giveup.put (CList.map drop_state initial)
@@ -1188,9 +1188,9 @@ module Trace = struct
let log m = InfoL.leaf (Info.Msg m)
let name_tactic m t = InfoL.tag (Info.Tactic m) t
- let pr_info ?(lvl=0) info =
+ let pr_info env sigma ?(lvl=0) info =
assert (lvl >= 0);
- Info.(print (collapse lvl info))
+ Info.(print env sigma (collapse lvl info))
end
@@ -1234,7 +1234,7 @@ module V82 = struct
let (goalss,evd) = Evd.Monad.List.map tac initgoals_w_state initevd in
let sgs = CList.flatten goalss in
let sgs = undefined evd sgs in
- InfoL.leaf (Info.Tactic (fun () -> Pp.str"<unknown>")) >>
+ InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"<unknown>")) >>
Pv.set { ps with solution = evd; comb = sgs; }
with e when catchable_exception e ->
let (e, info) = CErrors.push e in
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 28e793f0fc..286703c0dc 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -548,7 +548,7 @@ module Trace : sig
val log : Proofview_monad.lazy_msg -> unit tactic
val name_tactic : Proofview_monad.lazy_msg -> 'a tactic -> 'a tactic
- val pr_info : ?lvl:int -> Proofview_monad.Info.tree -> Pp.t
+ val pr_info : Environ.env -> Evd.evar_map -> ?lvl:int -> Proofview_monad.Info.tree -> Pp.t
end
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index 52bcabf958..69341d97df 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -64,8 +64,7 @@ end
(** We typically label nodes of [Trace.tree] with messages to
print. But we don't want to compute the result. *)
-type lazy_msg = unit -> Pp.t
-let pr_lazy_msg msg = msg ()
+type lazy_msg = Environ.env -> Evd.evar_map -> Pp.t
(** Info trace. *)
module Info = struct
@@ -80,9 +79,7 @@ module Info = struct
type state = tag Trace.incr
type tree = tag Trace.forest
-
-
- let pr_in_comments m = Pp.(str"(* "++pr_lazy_msg m++str" *)")
+ let pr_in_comments env sigma m = Pp.(str"(* "++ m env sigma ++str" *)")
let unbranch = function
| Trace.Seq (DBranch,brs) -> brs
@@ -112,31 +109,31 @@ module Info = struct
(** [with_sep] is [true] when [Tactic m] must be printed with a
trailing semi-colon. *)
- let rec pr_tree with_sep = let open Trace in function
- | Seq (Msg m,[]) -> pr_in_comments m
+ let rec pr_tree env sigma with_sep = let open Trace in function
+ | Seq (Msg m,[]) -> pr_in_comments env sigma m
| Seq (Tactic m,_) ->
let tail = if with_sep then Pp.str";" else Pp.mt () in
- Pp.(pr_lazy_msg m ++ tail)
+ Pp.(m env sigma ++ tail)
| Seq (Dispatch,brs) ->
let tail = if with_sep then Pp.str";" else Pp.mt () in
- Pp.(pr_dispatch brs++tail)
+ Pp.(pr_dispatch env sigma brs++tail)
| Seq (Msg _,_::_) | Seq (DBranch,_) -> assert false
- and pr_dispatch brs =
+ and pr_dispatch env sigma brs =
let open Pp in
let brs = List.map unbranch brs in
match brs with
- | [br] -> pr_forest br
+ | [br] -> pr_forest env sigma br
| _ ->
let sep () = spc()++str"|"++spc() in
- let branches = prlist_with_sep sep pr_forest brs in
+ let branches = prlist_with_sep sep (pr_forest env sigma) brs in
str"[>"++spc()++branches++spc()++str"]"
- and pr_forest = function
+ and pr_forest env sigma = function
| [] -> Pp.mt ()
- | [tr] -> pr_tree false tr
- | tr::l -> Pp.(pr_tree true tr ++ pr_forest l)
+ | [tr] -> pr_tree env sigma false tr
+ | tr::l -> Pp.(pr_tree env sigma true tr ++ pr_forest env sigma l)
- let print f =
- pr_forest (compress f)
+ let print env sigma f =
+ pr_forest env sigma (compress f)
let rec collapse_tree n t =
let open Trace in
diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
index 9d75242175..a08cab3bf6 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -45,7 +45,7 @@ end
(** We typically label nodes of [Trace.tree] with messages to
print. But we don't want to compute the result. *)
-type lazy_msg = unit -> Pp.t
+type lazy_msg = Environ.env -> Evd.evar_map -> Pp.t
(** Info trace. *)
module Info : sig
@@ -60,7 +60,7 @@ module Info : sig
type state = tag Trace.incr
type tree = tag Trace.forest
- val print : tree -> Pp.t
+ val print : Environ.env -> Evd.evar_map -> tree -> Pp.t
(** [collapse n t] flattens the first [n] levels of [Tactic] in an
info trace, effectively forgetting about the [n] top level of
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:45:23 +0000