diff options
Diffstat (limited to 'engine/proofview.ml')
| -rw-r--r-- | engine/proofview.ml | 20 |
1 files changed, 10 insertions, 10 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 |