diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-01-05 11:09:56 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-01-07 18:39:27 +0100 |
| commit | b185f9917a8b6fcea775925147f24839f81288a7 (patch) | |
| tree | 260d3bf664482e9ecacfe3dabe606df7dfa4fdc0 /kernel/univ.ml | |
| parent | b721d1352e9a2650921ae06aa434ec5e39fa578e (diff) | |
Aligning printing of universe constraints.
Diffstat (limited to 'kernel/univ.ml')
| -rw-r--r-- | kernel/univ.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 6d23d301e..b78cd6a04 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1760,7 +1760,7 @@ struct let pr (univs, cst as ctx) = if is_empty ctx then mt() else - Instance.pr univs ++ str " |= " ++ v 1 (Constraint.pr cst) + Instance.pr univs ++ str " |= " ++ v 0 (Constraint.pr cst) let hcons (univs, cst) = (Instance.hcons univs, hcons_constraints cst) @@ -1828,7 +1828,7 @@ struct let pr (univs, cst as ctx) = if is_empty ctx then mt() else - LSet.pr univs ++ str " |= " ++ v 1 (Constraint.pr cst) + LSet.pr univs ++ str " |= " ++ v 0 (Constraint.pr cst) let constraints (univs, cst) = cst let levels (univs, cst) = univs |