diff options
| author | Pierre-Marie Pédrot | 2018-05-22 17:22:52 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-05-22 17:22:52 +0200 |
| commit | c792c9fc500cbc1cab14271ebc6a98cd516451b3 (patch) | |
| tree | a3ef08574a31fe1eec2ac6a5194d667789c33625 /engine/termops.ml | |
| parent | c3838b204d3db7a58246d960a3da7efb7d1cc2f2 (diff) | |
| parent | 748a33cee41900d285897b24b4d8e29dd9eb2a3d (diff) | |
Merge PR #7384: Split Universes
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index df43be28e5..c271d9d999 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -47,7 +47,7 @@ let pr_fix pr_constr ((t,i),(lna,tl,bl)) = let pr_puniverses p u = if Univ.Instance.is_empty u then p - else p ++ str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)" + else p ++ str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)" let rec pr_constr c = match kind c with | Rel n -> str "#"++int n @@ -306,7 +306,7 @@ let pr_evar_universe_context ctx = str"ALGEBRAIC UNIVERSES:"++brk(0,1)++ h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++ str"UNDEFINED UNIVERSES:"++brk(0,1)++ - h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl() ++ + h 0 (UnivSubst.pr_universe_opt_subst (UState.subst ctx)) ++ fnl() ++ str "WEAK CONSTRAINTS:"++brk(0,1)++ h 0 (UState.pr_weak prl ctx) ++ fnl ()) |