diff options
| author | Emilio Jesus Gallego Arias | 2018-07-24 11:03:52 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-07-24 11:03:52 +0200 |
| commit | 4ab54f3cca76632cb6e258c84abc259e15e9e9f8 (patch) | |
| tree | c4374a0986acd6d4f6cac1a03e6bfa5ba7c972c9 /toplevel/coqloop.ml | |
| parent | 580a026070ab74d05f38e1177632be83a8756566 (diff) | |
| parent | 97069f69ab3a58cc4ccbaa1a835912c6c31dde4d (diff) | |
Merge PR #6801: Highlight differences between successive proof steps (color, underline, etc.)
Diffstat (limited to 'toplevel/coqloop.ml')
| -rw-r--r-- | toplevel/coqloop.ml | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 7ae15ac100..7b7e1b16c0 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -318,12 +318,6 @@ let loop_flush_all () = Format.pp_print_flush !Topfmt.std_ft (); Format.pp_print_flush !Topfmt.err_ft () -let pr_open_cur_subgoals () = - try - let proof = Proof_global.give_me_the_proof () in - Printer.pr_open_subgoals ~proof - with Proof_global.NoCurrentProof -> Pp.str "" - (* Goal equality heuristic. *) let pequal cmp1 cmp2 (a1,a2) (b1,b2) = cmp1 a1 b1 && cmp2 a2 b2 let evleq e1 e2 = CList.equal Evar.equal e1 e2 @@ -346,7 +340,7 @@ let top_goal_print oldp newp = let proof_changed = not (Option.equal cproof oldp newp) in let print_goals = not !Flags.quiet && proof_changed && Proof_global.there_are_pending_proofs () in - if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()) + if print_goals then Printer.print_and_diff oldp newp; with | exn -> let (e, info) = CErrors.push exn in |