diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 2 | ||||
| -rw-r--r-- | printing/printer.ml | 8 |
2 files changed, 6 insertions, 4 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index af105f4d63..267f5e0b5f 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -467,7 +467,7 @@ let tag_var = tag Tag.variable let pr_record_body_gen pr l = spc () ++ prlist_with_sep pr_semicolon - (fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr ltop c)) l + (fun (id, c) -> pr_reference id ++ str" :=" ++ pr ltop c) l let pr_forall n = keyword "forall" ++ pr_com_at n ++ spc () diff --git a/printing/printer.ml b/printing/printer.ml index c5cb6ffad8..a1a2d9ae51 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -780,17 +780,19 @@ let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof = straightforward, but seriously, [Proof.proof] should return [evar_info]-s instead. *) let p = proof in - let Proof.{goals; stack; shelf; given_up; sigma} = Proof.data p in + let Proof.{goals; stack; sigma} = Proof.data p in + let shelf = Evd.shelf sigma in + let given_up = Evd.given_up sigma in let stack = List.map (fun (l,r) -> List.length l + List.length r) stack in let seeds = Proof.V82.top_evars p in begin match goals with | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in begin match bgoals,shelf,given_up with - | [] , [] , [] -> pr_subgoals None sigma ~seeds ~shelf ~stack ~unfocused:[] ~goals + | [] , [] , g when Evar.Set.is_empty g -> pr_subgoals None sigma ~seeds ~shelf ~stack ~unfocused:[] ~goals | [] , [] , _ -> Feedback.msg_info (str "No more subgoals, but there are some goals you gave up:"); fnl () - ++ pr_subgoals ~pr_first:false None bsigma ~seeds ~shelf:[] ~stack:[] ~unfocused:[] ~goals:given_up + ++ pr_subgoals ~pr_first:false None bsigma ~seeds ~shelf:[] ~stack:[] ~unfocused:[] ~goals:(Evar.Set.elements given_up) ++ fnl () ++ str "You need to go back and solve them." | [] , _ , _ -> Feedback.msg_info (str "All the remaining goals are on the shelf."); |