diff options
| author | Pierre-Marie Pédrot | 2019-07-14 13:53:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-07-14 13:53:25 +0200 |
| commit | 76dfd0b95a7fd2de99f65de9fc10925d58777cd4 (patch) | |
| tree | 9a80f38a78b75d21b0fdd84b0a0f54a767adc290 /printing/printer.ml | |
| parent | 3bd2722fb53552f45a25e6bc0a03a9ab0517485f (diff) | |
| parent | 2576fee1798b753161a730244c8d4d701e8a4641 (diff) | |
Merge PR #10496: [proof] Minor cleanup in proof.ml
Reviewed-by: ppedrot
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 97b3233d12..ec1b9b8e49 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -825,9 +825,9 @@ let pr_nth_open_subgoal ~proof n = let pr_goal_by_id ~proof id = try - Proof.in_proof proof (fun sigma -> - let g = Evd.evar_key id sigma in - pr_selected_subgoal (pr_id id) sigma g) + let { Proof.sigma } = Proof.data proof in + let g = Evd.evar_key id sigma in + pr_selected_subgoal (pr_id id) sigma g with Not_found -> user_err Pp.(str "No such goal.") (** print a goal identified by the goal id as it appears in -emacs mode. @@ -843,7 +843,8 @@ let pr_goal_emacs ~proof gid sid = ++ pr_goal gs) in try - Proof.in_proof proof (fun sigma -> pr {it=(Evar.unsafe_of_int gid);sigma=sigma;}) + let { Proof.sigma } = Proof.data proof in + pr { it = Evar.unsafe_of_int gid ; sigma } with Not_found -> user_err Pp.(str "No such goal.") (* Printer function for sets of Assumptions.assumptions. |