diff options
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 30 |
1 files changed, 21 insertions, 9 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index da364c8b9e..4840577cbf 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -244,8 +244,19 @@ let pr_abstract_cumulativity_info sigma cumi = let pr_global_env = Nametab.pr_global_env let pr_global = pr_global_env Id.Set.empty +let pr_universe_instance_constraints evd inst csts = + let open Univ in + let prlev = Termops.pr_evd_level evd in + let pcsts = if Constraint.is_empty csts then mt() + else str " |= " ++ + prlist_with_sep (fun () -> str "," ++ spc()) + (fun (u,d,v) -> hov 0 (prlev u ++ pr_constraint_type d ++ prlev v)) + (Constraint.elements csts) + in + str"@{" ++ Instance.pr prlev inst ++ pcsts ++ str"}" + let pr_universe_instance evd inst = - str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}" + pr_universe_instance_constraints evd inst Univ.Constraint.empty let pr_puniverses f env sigma (c,u) = if !Constrextern.print_universes @@ -445,9 +456,9 @@ let pr_predicate pr_elt (b, elts) = let pr_cpred p = pr_predicate (pr_constant (Global.env())) (Cpred.elements p) let pr_idpred p = pr_predicate Id.print (Id.Pred.elements p) -let pr_transparent_state (ids, csts) = - hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++ - str"CONSTANTS: " ++ pr_cpred csts ++ fnl ()) +let pr_transparent_state ts = + hv 0 (str"VARIABLES: " ++ pr_idpred ts.TransparentState.tr_var ++ fnl () ++ + str"CONSTANTS: " ++ pr_cpred ts.TransparentState.tr_cst ++ fnl ()) (* display complete goal og_s has goal+sigma on the previous proof step for diffs @@ -674,10 +685,6 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map | None -> GoalMap.empty in - let map_goal_for_diff ng = (* todo: move to proof_diffs.ml *) - try GoalMap.find ng diff_goal_map with Not_found -> ng - in - (** Printing functions for the extra informations. *) let rec print_stack a = function | [] -> Pp.int a @@ -713,7 +720,12 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map let get_ogs g = match os_map with - | Some (osigma, _) -> Some { it = map_goal_for_diff g; sigma = osigma } + | Some (osigma, _) -> + (* if Not_found, returning None treats the goal as new and it will be 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)")) | None -> None in let rec pr_rec n = function |