diff options
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 2bbda279bd..f11c74348d 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -722,11 +722,11 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map let get_ogs g = match os_map with | Some (osigma, _) -> - (* if Not_found, returning None treats the goal as new and it will be highlighted; + (* if Not_found, returning None treats the goal as new and it will be diff highlighted; returning Some { it = g; sigma = sigma } will compare the new goal to itself and it won't be highlighted *) (try Some { it = GoalMap.find g diff_goal_map; sigma = osigma } - with Not_found -> raise (Pp_diff.Diff_Failure "Unable to match goals between old and new proof states (7)")) + with Not_found -> None) | None -> None in let rec pr_rec n = function |