From 7aa8c15d7884a0bc77453e0078b8e02392ca68a6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Sat, 20 Jul 2024 10:36:18 +0200 Subject: [PATCH] Show Universes print weak above_prop constraints (used by minimization) --- engine/uState.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/engine/uState.ml b/engine/uState.ml index eb0128487b1c..7a1a0ee47687 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -1247,9 +1247,12 @@ let check_uctx_impl ~fail uctx uctx' = (* XXX print above_prop too *) -let pr_weak prl {minim_extra={UnivMinim.weak_constraints=weak}} = +let pr_weak prl {minim_extra={UnivMinim.weak_constraints=weak; above_prop}} = let open Pp in - prlist_with_sep fnl (fun (u,v) -> prl u ++ str " ~ " ++ prl v) (UPairSet.elements weak) + v 0 ( + prlist_with_sep cut (fun (u,v) -> h (prl u ++ str " ~ " ++ prl v)) (UPairSet.elements weak) + ++ if UPairSet.is_empty weak || Level.Set.is_empty above_prop then mt() else cut () ++ + prlist_with_sep cut (fun u -> h (str "Prop <= " ++ prl u)) (Level.Set.elements above_prop)) let pr_sort_opt_subst uctx = QState.pr (pr_uctx_qvar uctx) uctx.sort_variables