diff options
| author | Hugo Herbelin | 2020-03-19 13:35:22 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-19 13:35:22 +0100 |
| commit | 3ae4231d30edfa928595b6fa886ce6df1a495089 (patch) | |
| tree | d6c1d749e6435570e3437f012aad8e6d6797c432 /vernac | |
| parent | 1d8698e97dee385151ef92efd924560b296f8d50 (diff) | |
| parent | ea16c402392722a44bf2227aef7ff73faef70d3a (diff) | |
Merge PR #11795: Print implicit arguments in types of references
Ack-by: herbelin
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/prettyp.ml | 4 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 10 |
2 files changed, 10 insertions, 4 deletions
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 52457d15dc..a7170c8e18 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -83,6 +83,8 @@ let print_ref reduce ref udecl = let ctx,ccl = Reductionops.splay_prod_assum env sigma typ in EConstr.it_mkProd_or_LetIn ccl ctx else typ in + let impargs = select_stronger_impargs (implicits_of_global ref) in + let impargs = List.map binding_kind_of_status impargs in let variance = let open GlobRef in match ref with | VarRef _ | ConstRef _ -> None | IndRef (ind,_) | ConstructRef ((ind,_),_) -> @@ -95,7 +97,7 @@ let print_ref reduce ref udecl = else mt () in let priv = None in (* We deliberately don't print private univs in About. *) - hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ + hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma ~impargs typ ++ Printer.pr_abstract_universe_ctx sigma ?variance univs ?priv) (********************************) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e2fdae37fb..b5ecd62dad 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1778,12 +1778,15 @@ let vernac_search ~pstate ~atts s gopt r = let pp = if !search_output_name_only then pr else begin - let pc = pr_lconstr_env env Evd.(from_env env) c in + let open Impargs in + let impargs = select_stronger_impargs (implicits_of_global ref) in + let impargs = List.map binding_kind_of_status impargs in + let pc = pr_ltype_env env Evd.(from_env env) ~impargs c in hov 2 (pr ++ str":" ++ spc () ++ pc) end in Feedback.msg_notice pp in - match s with + (match s with | SearchPattern c -> (Search.search_pattern ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search | SearchRewrite c -> @@ -1796,7 +1799,8 @@ let vernac_search ~pstate ~atts s gopt r = Search.prioritize_search) pr_search | Search sl -> (Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> - Search.prioritize_search) pr_search + Search.prioritize_search) pr_search); + Feedback.msg_notice (str "(use \"About\" for full details on implicit arguments)") let vernac_locate ~pstate = let open Constrexpr in function | LocateAny {v=AN qid} -> Prettyp.print_located_qualid qid |