diff options
| author | coqbot-app[bot] | 2020-10-09 14:43:02 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-09 14:43:02 +0000 |
| commit | ac7c197c3b8a9b66956f35e364221938f91e2a23 (patch) | |
| tree | dac9632d48449cfe77977e209803ebb9d19b9805 /vernac | |
| parent | cc3ef68a475140bf7d3ca7a2fd3bc593508eb42c (diff) | |
| parent | f7fabd34526135daccce2630670905fc39e0c3db (diff) | |
Merge PR #13143: Drop misleading argument of Pp.h box
Reviewed-by: ejgallego
Reviewed-by: silene
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 = |