aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-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
-rw-r--r--plugins/ltac/tacinterp.ml20
-rw-r--r--proofs/pfedit.ml7
-rw-r--r--proofs/refine.ml4
-rw-r--r--tactics/auto.ml33
-rw-r--r--tactics/tactics.ml4
9 files changed, 64 insertions, 61 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
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
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index e2b7df19de..7f1ae6d12b 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -107,11 +107,14 @@ let solve ?with_end_tac gi info_lvl tac pr =
Proofview.tclTHEN tac Refine.solve_constraints
else tac
in
- let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac pr in
+ let env = Global.env () in
+ let (p,(status,info)) = Proof.run_tactic env tac pr in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
let () =
match info_lvl with
| None -> ()
- | Some i -> Feedback.msg_info (hov 0 (Proofview.Trace.pr_info ~lvl:i info))
+ | Some i -> Feedback.msg_info (hov 0 (Proofview.Trace.pr_info env sigma ~lvl:i info))
in
(p,status)
with
diff --git a/proofs/refine.ml b/proofs/refine.ml
index d812a8cad7..1d796fece5 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -107,8 +107,8 @@ let generic_refine ~typecheck f gl =
(* Mark goals *)
let sigma = Proofview.Unsafe.mark_as_goals sigma comb in
let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in
- let trace () = Pp.(hov 2 (str"simple refine"++spc()++
- Termops.Internal.print_constr_env env sigma c)) in
+ let trace env sigma = Pp.(hov 2 (str"simple refine"++spc()++
+ Termops.Internal.print_constr_env env sigma c)) in
Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v ->
Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*>
Proofview.Unsafe.tclEVARS sigma <*>
diff --git a/tactics/auto.ml b/tactics/auto.ml
index f5c3619e64..2619620eb8 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -215,11 +215,15 @@ let tclLOG (dbg,_,depth,trace) pp tac =
let s = String.make (depth+1) '*' in
Proofview.(tclIFCATCH (
tac >>= fun v ->
- Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)");
+ tclENV >>= fun env ->
+ tclEVARMAP >>= fun sigma ->
+ Feedback.msg_debug (str s ++ spc () ++ pp env sigma ++ str ". (*success*)");
tclUNIT v
- ) Proofview.tclUNIT
+ ) tclUNIT
(fun (exn, info) ->
- Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)");
+ tclENV >>= fun env ->
+ tclEVARMAP >>= fun sigma ->
+ Feedback.msg_debug (str s ++ spc () ++ pp env sigma ++ str ". (*fail*)");
tclZERO ~info exn))
| Info ->
(* For "info (trivial/auto)", we store a log trace *)
@@ -248,12 +252,12 @@ and erase_subtree depth = function
| [] -> []
| (d,_) :: l -> if Int.equal d depth then l else erase_subtree depth l
-let pr_info_atom (d,pp) =
- str (String.make d ' ') ++ pp () ++ str "."
+let pr_info_atom env sigma (d,pp) =
+ str (String.make d ' ') ++ pp env sigma ++ str "."
-let pr_info_trace = function
+let pr_info_trace env sigma = function
| (Info,_,_,{contents=(d,Some pp)::l}) ->
- Feedback.msg_info (prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l))
+ Feedback.msg_info (prlist_with_sep fnl (pr_info_atom env sigma) (cleanup_info_trace d [(d,pp)] l))
| _ -> ()
let pr_info_nop = function
@@ -269,8 +273,12 @@ let pr_dbg_header = function
let tclTRY_dbg d tac =
let delay f = Proofview.tclUNIT () >>= fun () -> f () in
- let tac = delay (fun () -> pr_dbg_header d; tac) >>=
- fun () -> pr_info_trace d; Proofview.tclUNIT () in
+ let tac =
+ delay (fun () -> pr_dbg_header d; tac) >>= fun () ->
+ Proofview.tclENV >>= fun env ->
+ Proofview.tclEVARMAP >>= fun sigma ->
+ pr_info_trace env sigma d;
+ Proofview.tclUNIT () in
let after = delay (fun () -> pr_info_nop d; Proofview.tclUNIT ()) in
Tacticals.New.tclORELSE0 tac after
@@ -300,8 +308,8 @@ let exists_evaluable_reference env = function
| EvalConstRef _ -> true
| EvalVarRef v -> try ignore(lookup_named v env); true with Not_found -> false
-let dbg_intro dbg = tclLOG dbg (fun () -> str "intro") intro
-let dbg_assumption dbg = tclLOG dbg (fun () -> str "assumption") assumption
+let dbg_intro dbg = tclLOG dbg (fun _ _ -> str "intro") intro
+let dbg_assumption dbg = tclLOG dbg (fun _ _ -> str "assumption") assumption
let rec trivial_fail_db dbg mod_delta db_list local_db =
let intro_tac =
@@ -385,12 +393,11 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=
| Extern tacast ->
conclPattern concl p tacast
in
- let pr_hint () =
+ let pr_hint env sigma =
let origin = match dbname with
| None -> mt ()
| Some n -> str " (in " ++ str n ++ str ")"
in
- let sigma, env = Pfedit.get_current_context () in
pr_hint env sigma t ++ origin
in
tclLOG dbg pr_hint (run_hint t tactic)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b1f2ceee57..1043c50f00 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -891,10 +891,6 @@ let reduce redexp cl =
let pr = (pr_econstr_env, pr_leconstr_env, pr_evaluable_reference, pr_constr_pattern_env) in
Pp.(hov 2 (Ppred.pr_red_expr_env env sigma pr str redexp))
in
- let trace () =
- let sigma, env = Pfedit.get_current_context () in
- trace env sigma
- in
Proofview.Trace.name_tactic trace begin
Proofview.Goal.enter begin fun gl ->
let cl' = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:15:38 +0000