diff options
| author | Maxime Dénès | 2017-12-12 16:48:08 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-07-25 16:27:19 +0200 |
| commit | d389d88a7cec1b30b42c11d0dbff3f566b51e81a (patch) | |
| tree | 240bbce956966d16065f46230bf052ed17fb8978 /vernac | |
| parent | 523de4f878293cf1d582bd70300b34d497e705b3 (diff) | |
Remove himsg.pr_puniverses, use @{} for universe printing in errors
Replaces #6401.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index c49ffe2679..e208d176bb 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -194,12 +194,6 @@ let rec pr_disjunction pr = function | a::l -> pr a ++ str "," ++ spc () ++ pr_disjunction pr l | [] -> assert false -let pr_puniverses f env (c,u) = - f env c ++ - (if Flags.is_universe_polymorphism () && not (Univ.Instance.is_empty u) then - str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)" - else mt()) - let explain_elim_arity env sigma ind sorts c pj okinds = let open EConstr in let env = make_all_name_different env sigma in @@ -262,7 +256,7 @@ let explain_ill_formed_branch env sigma c ci actty expty = let pa, pe = pr_explicit env sigma (simp actty) (simp expty) in strbrk "In pattern-matching on term" ++ brk(1,1) ++ pc ++ spc () ++ strbrk "the branch for constructor" ++ spc () ++ - quote (pr_puniverses pr_constructor env ci) ++ + quote (pr_pconstructor env sigma ci) ++ spc () ++ str "has type" ++ brk(1,1) ++ pa ++ spc () ++ str "which should be" ++ brk(1,1) ++ pe ++ str "." |