diff options
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 7 |
1 files changed, 5 insertions, 2 deletions
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 |