diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-05 16:34:37 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-05 16:34:37 +0100 |
| commit | 55a765faa95d7be9a1e4c37096139f57f288f55a (patch) | |
| tree | 459ac71b1478d69f77f8663c1001c10ca0ae528d /kernel/univ.ml | |
| parent | 35afb42a6bb30634d2eb77a32002ed473633b5f4 (diff) | |
| parent | 0fd6ad21121c7c179375b9a50c3135abab1781b2 (diff) | |
Merge branch 'v8.5'
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 b303a1a5a..4cc34e41e 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -991,7 +991,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) @@ -1065,7 +1065,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 |