diff options
| author | Hugo Herbelin | 2020-10-05 22:21:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-08 23:47:14 +0200 |
| commit | db278921c54201a01543953cc0986fc0fb126615 (patch) | |
| tree | 70115f7e9365b34c4464affbb9a8cf71a925317c /vernac | |
| parent | e18ed350f7b5710c382ea1306e7b1e7e2fb0c9f8 (diff) | |
Dropping the misleading int argument of Pp.h.
An h-box inhibits the breaking semantics of any cut/spc/brk in the
enclosed box.
We tentatively replace its occurrence by an h or hv, assuming in
particular that if the indentation is not 0, an hv box was intended.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 6 | ||||
| -rw-r--r-- | vernac/prettyp.ml | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index c16eaac516..a9de01bfd0 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -831,7 +831,7 @@ let pr_constraints printenv env sigma evars cstrs = (fun (ev, evi) -> fnl () ++ pr_existential_key sigma ev ++ str " : " ++ pr_leconstr_env env' sigma evi.evar_concl ++ fnl ()) l in - h 0 (pe ++ evs ++ pr_evar_constraints sigma cstrs) + h (pe ++ evs ++ pr_evar_constraints sigma cstrs) else let filter evk _ = Evar.Map.mem evk evars in pr_evar_map_filter ~with_univs:false filter env sigma @@ -973,8 +973,8 @@ let explain_not_match_error = function (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) ++ + str "incompatible polymorphic binders: got" ++ spc () ++ h (pr_auctx got) ++ spc() ++ + str "but expected" ++ spc() ++ h (pr_auctx expect) ++ (if not (Int.equal (AUContext.size got) (AUContext.size expect)) then mt() else fnl() ++ str "(incompatible constraints)") | IncompatibleVariance -> diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 8b00484b4a..06f7c32cdc 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -216,7 +216,7 @@ let print_polymorphism ref = (if poly then str "universe polymorphic" else if template_poly then str "template universe polymorphic " - ++ h 0 (pr_template_variables template_variables) + ++ h (pr_template_variables template_variables) else str "not universe polymorphic") ] let print_type_in_type ref = |