diff options
| author | Pierre-Marie Pédrot | 2018-07-25 22:00:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-25 22:00:33 +0200 |
| commit | 535f8ce6edea2e2692f5c9c094d3c6fd07411897 (patch) | |
| tree | 8ce9fab779fe91e6a1fa12eba1718f9eda763efb /printing/printer.ml | |
| parent | e1f7bb0bba093e5e5398bfe5a2a5d0ffabdf1405 (diff) | |
| parent | ca9e02ad1882cc4268ae1bcf0f573d24b92fa695 (diff) | |
Merge PR #7859: Remove himsg.pr_puniverses, use @{} for universe printing in errors
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 16 |
1 files changed, 7 insertions, 9 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index ba094596ff..a77c1ced56 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -290,11 +290,13 @@ let pr_cumulativity_info sigma cumi = let pr_global_env = pr_global_env let pr_global = pr_global_env Id.Set.empty -let pr_puniverses f env (c,u) = - f env c ++ - (if !Constrextern.print_universes then - str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)" - else mt ()) +let pr_universe_instance evd inst = + str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}" + +let pr_puniverses f env sigma (c,u) = + if !Constrextern.print_universes + then f env c ++ pr_universe_instance sigma u + else f env c let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst) let pr_existential_key = Termops.pr_existential_key @@ -1016,10 +1018,6 @@ let pr_polymorphic b = if b then str"Polymorphic " else str"Monomorphic " else mt () -let pr_universe_instance evd ctx = - let inst = Univ.UContext.instance ctx in - str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}" - (* print the proof step, possibly with diffs highlighted, *) let print_and_diff oldp newp = match newp with |