diff options
Diffstat (limited to 'toplevel/coqloop.ml')
| -rw-r--r-- | toplevel/coqloop.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 86fd3be4f5..2c5faa4df7 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -375,7 +375,7 @@ let exit_on_error = point we should consolidate the code *) let show_proof_diff_to_pp pstate = let p = Option.get pstate in - let sigma, env = Declare.get_proof_context p in + let sigma, env = Proof.get_proof_context p in let pprf = Proof.partial_proof p in Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf @@ -392,7 +392,7 @@ let show_proof_diff_cmd ~state removed = let show_removed = Some removed in Pp_diff.diff_pp_combined ~tokenize_string ?show_removed o_pp n_pp with - | Declare.NoSuchGoal + | Proof.NoSuchGoal _ | Option.IsNone -> n_pp | Pp_diff.Diff_Failure msg -> begin (* todo: print the unparsable string (if we know it) *) @@ -403,7 +403,7 @@ let show_proof_diff_cmd ~state removed = else n_pp with - | Declare.NoSuchGoal + | Proof.NoSuchGoal _ | Option.IsNone -> CErrors.user_err (str "No goals to show.") |