diff options
| author | Pierre-Marie Pédrot | 2015-01-29 22:40:58 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-01-29 22:40:58 +0100 |
| commit | a340265c9f88df990649481c8ecbe8a513ac4756 (patch) | |
| tree | c9e02defb10bcdb258d75cb6f156657654f65f1f /kernel | |
| parent | 51b15993cb4a9cc2521b6107b7f4195b21040087 (diff) | |
| parent | db293d185f8deb091d4b086f327caa0f376d67d7 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/univ.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 08e9fee051..492762df39 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -2064,7 +2064,7 @@ let explain_universe_inconsistency prl (o,u,v,p) = (spc() ++ str "= " ++ pr_uni u)) in str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++ - pr_rel o ++ spc() ++ pr_uni v ++ reason ++ str")" + pr_rel o ++ spc() ++ pr_uni v ++ reason let compare_levels = Level.compare let eq_levels = Level.equal |