diff options
| author | Gaëtan Gilbert | 2018-11-13 16:25:23 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-16 15:09:52 +0100 |
| commit | 3d49ce63bd1aa35ef2e8abc9cc359ad6031c21bb (patch) | |
| tree | c3750e4aae2d3c0b14879090e001b6cbc1b8c769 /vernac | |
| parent | 744a07e53fb99652b2b30520cfe3dfe701bbde18 (diff) | |
Print universe names in subtyping error instead of Var(x).
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index ad70f2067b..6c7117b513 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -894,17 +894,20 @@ let explain_not_match_error = function quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t2) | IncompatibleConstraints { got; expect } -> let open Univ in - (** FIXME: provide a proper naming for the bound variables *) let pr_auctx auctx = + let sigma = Evd.from_ctx + (UState.of_binders + (UnivNames.universe_binders_with_opt_names auctx None)) + in let uctx = AUContext.repr auctx in - Printer.pr_universe_instance_constraints Evd.empty + Printer.pr_universe_instance_constraints sigma (UContext.instance uctx) (UContext.constraints uctx) in str "incompatible polymorphic binders: got" ++ spc () ++ h 0 (pr_auctx got) ++ spc() ++ str "but expected" ++ spc() ++ h 0 (pr_auctx expect) ++ (if not (Int.equal (AUContext.size got) (AUContext.size expect)) then mt() else - spc() ++ str "(incompatible constraints)") + fnl() ++ str "(incompatible constraints)") let explain_signature_mismatch l spec why = str "Signature components for label " ++ Label.print l ++ |