diff options
| -rw-r--r-- | printing/printer.ml | 1 | ||||
| -rw-r--r-- | proofs/proofview.ml | 15 | ||||
| -rw-r--r-- | proofs/proofview.mli | 4 |
3 files changed, 20 insertions, 0 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 75cce2755a..1880d90ee9 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -51,6 +51,7 @@ let pr_lconstr_core goal_concl_style env sigma t = let pr_lconstr_env env = pr_lconstr_core false env let pr_constr_env env = pr_constr_core false env +let _ = Hook.set Proofview.Refine.pr_constr pr_constr_env let pr_lconstr_goal_style_env env = pr_lconstr_core true env let pr_constr_goal_style_env env = pr_constr_core true env diff --git a/proofs/proofview.ml b/proofs/proofview.ml index e03249ca56..ba61bf7a5f 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -533,6 +533,7 @@ let shelve = let open Proof in Comb.get >>= fun initial -> Comb.set [] >> + InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve")) >> Shelf.put initial @@ -571,6 +572,7 @@ let shelve_unifiable = 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")) >> Shelf.put u (** [guard_no_unifiable] fails with error [UnresolvedBindings] if some @@ -604,6 +606,8 @@ let goodmod p m = if p' < 0 then p'+m else p' let cycle n = + let open Proof in + InfoL.leaf (Info.Tactic (fun () -> Pp.(str"cycle"++spc()++int n))) >> Comb.modify begin fun initial -> let l = CList.length initial in let n' = goodmod n l in @@ -612,6 +616,8 @@ let cycle n = end let swap i j = + let open Proof in + InfoL.leaf (Info.Tactic (fun () -> Pp.(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 @@ -625,6 +631,8 @@ let swap i j = end let revgoals = + let open Proof in + InfoL.leaf (Info.Tactic (fun () -> Pp.str"revgoals")) >> Comb.modify CList.rev let numgoals = @@ -663,6 +671,7 @@ let give_up = Comb.get >>= fun initial -> Comb.set [] >> mark_as_unsafe >> + InfoL.leaf (Info.Tactic (fun () -> Pp.str"give_up")) >> Giveup.put initial @@ -920,6 +929,9 @@ struct let () = Typing.check env evdref c concl in !evdref + let (pr_constrv,pr_constr) = + Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") () + let refine ?(unsafe = false) f = Goal.enter begin fun gl -> let sigma = Goal.sigma gl in let env = Goal.env gl in @@ -949,6 +961,8 @@ struct (** Select the goals *) let comb = undefined sigma (CList.rev evs) in let sigma = CList.fold_left mark_as_goal sigma comb in + let open Proof in + InfoL.leaf (Info.Tactic (fun () -> Pp.(str"refine"++spc()++ Hook.get pr_constrv env sigma c))) >> Pv.set { solution = sigma; comb; } end @@ -1024,6 +1038,7 @@ module V82 = struct in let (goalss,evd) = Evd.Monad.List.map tac initgoals initevd in let sgs = CList.flatten goalss in + InfoL.leaf (Info.Tactic (fun () -> Pp.str"<unknown>")) >> Pv.set { solution = evd; comb = sgs; } with e when catchable_exception e -> let e = Errors.push e in diff --git a/proofs/proofview.mli b/proofs/proofview.mli index cc8706ab2e..52b9d3c11a 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -450,6 +450,10 @@ end module Refine : sig + (** Printer used to print the constr which refine refines. *) + val pr_constr : + (Environ.env -> Evd.evar_map -> Term.constr -> Pp.std_ppcmds) Hook.t + (** {7 Refinement primitives} *) val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * Constr.t) -> unit tactic |