diff options
| author | Gaëtan Gilbert | 2018-11-02 12:55:21 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-16 15:09:52 +0100 |
| commit | 14c5b4bb8a9c5f62081594d2beaca274eaa0b8f3 (patch) | |
| tree | a8093604c95ccd1081aedab2de45d01920af1334 /printing/printer.ml | |
| parent | 778213b89d893b55e572fc1813c7209d647ed6b0 (diff) | |
Print full binders in subtyping incompatible polymorphism error.
Close #8891
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index da364c8b9e..8227933433 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -244,8 +244,19 @@ let pr_abstract_cumulativity_info sigma cumi = let pr_global_env = Nametab.pr_global_env let pr_global = pr_global_env Id.Set.empty +let pr_universe_instance_constraints evd inst csts = + let open Univ in + let prlev = Termops.pr_evd_level evd in + let pcsts = if Constraint.is_empty csts then mt() + else str " |= " ++ + prlist_with_sep (fun () -> str "," ++ spc()) + (fun (u,d,v) -> prlev u ++ pr_constraint_type d ++ prlev v) + (Constraint.elements csts) + in + str"@{" ++ Instance.pr prlev inst ++ pcsts ++ str"}" + let pr_universe_instance evd inst = - str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}" + pr_universe_instance_constraints evd inst Univ.Constraint.empty let pr_puniverses f env sigma (c,u) = if !Constrextern.print_universes |