diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-04 14:35:02 -0500 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-04 14:35:02 -0500 |
| commit | 209faf81c432c39d4537f8b1dc5c9947d4349d30 (patch) | |
| tree | 597ccf58342b2b00751d5f777caeaaffe051c0b1 /kernel/univ.ml | |
| parent | acc54398bd244b15d4dbc396836c279eabf3bf6b (diff) | |
Univs: update refman, better printers for universe contexts.
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 064dde3a6..6c2316988 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1768,7 +1768,7 @@ struct let pr prl (univs, cst as ctx) = if is_empty ctx then mt() else - Instance.pr prl univs ++ str " |= " ++ v 0 (Constraint.pr prl cst) + h 0 (Instance.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst)) let hcons (univs, cst) = (Instance.hcons univs, hcons_constraints cst) @@ -1842,7 +1842,7 @@ struct let pr prl (univs, cst as ctx) = if is_empty ctx then mt() else - LSet.pr prl univs ++ str " |= " ++ v 0 (Constraint.pr prl cst) + h 0 (LSet.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst)) let constraints (univs, cst) = cst let levels (univs, cst) = univs |