Print implicit arguments in types of references

9 files changed, 38 insertions, 23 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index e8129938a1..2df602967b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -82,7 +82,7 @@ let ppsconstr x = ppconstr (Mod_subst.force_constr x)
 let ppconstr_univ x = Constrextern.with_universes ppconstr x
 let ppglob_constr = (fun x -> pp(pr_lglob_constr_env (Global.env()) x))
 let pppattern = (fun x -> pp(envpp pr_constr_pattern_env x))
-let pptype = (fun x -> try pp(envpp pr_ltype_env x) with e -> pp (str (Printexc.to_string e)))
+let pptype = (fun x -> try pp(envpp (fun env evm t -> pr_ltype_env env evm t) x) with e -> pp (str (Printexc.to_string e)))
 let ppfconstr c = ppconstr (CClosure.term_of_fconstr c)
 
 let ppbigint n = pp (str (Bigint.to_string n));;
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 44aacd62d8..5dee732af7 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -926,7 +926,7 @@ let extern_ref vars ref us =
 
 let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None)
 
-let rec extern inctx scopes vars r =
+let rec extern inctx ?impargs scopes vars r =
   match remove_one_coercion inctx (flatten_application r) with
   | Some (nargs,inctx,r') ->
     (try extern_notations scopes vars (Some nargs) r
@@ -990,10 +990,10 @@ let rec extern inctx scopes vars r =
   | GLetIn (na,b,t,c) ->
       CLetIn (make ?loc na,sub_extern false scopes vars b,
               Option.map (extern_typ scopes vars) t,
-              extern inctx scopes (add_vname vars na) c)
+              extern inctx ?impargs scopes (add_vname vars na) c)
 
   | GProd (na,bk,t,c) ->
-      factorize_prod scopes vars na bk t c
+      factorize_prod ?impargs scopes vars na bk t c
 
   | GLambda (na,bk,t,c) ->
       factorize_lambda inctx scopes vars na bk t c
@@ -1092,12 +1092,12 @@ let rec extern inctx scopes vars r =
 
   in insert_coercion coercion (CAst.make ?loc c)
 
-and extern_typ (subentry,(_,scopes)) =
-  extern true (subentry,(Notation.current_type_scope_name (),scopes))
+and extern_typ ?impargs (subentry,(_,scopes)) =
+  extern true ?impargs (subentry,(Notation.current_type_scope_name (),scopes))
 
 and sub_extern inctx (subentry,(_,scopes)) = extern inctx (subentry,(None,scopes))
 
-and factorize_prod scopes vars na bk t c =
+and factorize_prod ?impargs scopes vars na bk t c =
   let implicit_type = is_reserved_type na t in
   let aty = extern_typ scopes vars t in
   let vars = add_vname vars na in
@@ -1117,7 +1117,13 @@ and factorize_prod scopes vars na bk t c =
       | _ -> CProdN ([binder],b))
      | _ -> assert false)
   | _, _ ->
-      let c' = extern_typ scopes vars c in
+      let impargs_hd, impargs_tl =
+        match impargs with
+        | Some [hd] -> Some hd, None
+        | Some (hd::tl) -> Some hd, Some tl
+        | _ -> None, None in
+      let bk = Option.default Explicit impargs_hd in
+      let c' = extern_typ ?impargs:impargs_tl scopes vars c in
       match na, c'.v with
       | Name id, CProdN (CLocalAssum(nal,Default bk',ty)::bl,b)
            when binding_kind_eq bk bk'
@@ -1306,8 +1312,8 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
 let extern_glob_constr vars c =
   extern false (InConstrEntrySomeLevel,(None,[])) vars c
 
-let extern_glob_type vars c =
-  extern_typ (InConstrEntrySomeLevel,(None,[])) vars c
+let extern_glob_type ?impargs vars c =
+  extern_typ ?impargs (InConstrEntrySomeLevel,(None,[])) vars c
 
 (******************************************************************)
 (* Main translation function from constr -> constr_expr *)
@@ -1320,7 +1326,7 @@ let extern_constr ?lax ?(inctx=false) ?scope env sigma t =
 let extern_constr_in_scope ?lax ?inctx scope env sigma t =
   extern_constr ?lax ?inctx ~scope env sigma t
 
-let extern_type ?lax ?(goal_concl_style=false) env sigma t =
+let extern_type ?lax ?(goal_concl_style=false) env sigma ?impargs t =
   (* "goal_concl_style" means do alpha-conversion using the "goal" convention *)
   (* i.e.: avoid using the names of goal/section/rel variables and the short *)
   (* names of global definitions of current module when computing names for *)
@@ -1330,7 +1336,7 @@ let extern_type ?lax ?(goal_concl_style=false) env sigma t =
   (* consideration; see namegen.ml for further details *)
   let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in
   let r = Detyping.detype Detyping.Later ?lax goal_concl_style avoid env sigma t in
-  extern_glob_type (vars_of_env env) r
+  extern_glob_type ?impargs (vars_of_env env) r
 
 let extern_sort sigma s = extern_glob_sort (detype_sort sigma s)
 
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 0eca287c1d..5c31acd0d7 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -25,7 +25,7 @@ open Ltac_pretype
 
 val extern_cases_pattern : Id.Set.t -> 'a cases_pattern_g -> cases_pattern_expr
 val extern_glob_constr : Id.Set.t -> 'a glob_constr_g -> constr_expr
-val extern_glob_type : Id.Set.t -> 'a glob_constr_g -> constr_expr
+val extern_glob_type : ?impargs:Glob_term.binding_kind list -> Id.Set.t -> 'a glob_constr_g -> constr_expr
 val extern_constr_pattern : names_context -> Evd.evar_map ->
   constr_pattern -> constr_expr
 val extern_closed_glob : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name ->
@@ -42,7 +42,7 @@ val extern_constr : ?lax:bool -> ?inctx:bool -> ?scope:scope_name ->
 val extern_constr_in_scope : ?lax:bool -> ?inctx:bool -> scope_name ->
   env -> Evd.evar_map -> constr -> constr_expr
 val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
-val extern_type : ?lax:bool -> ?goal_concl_style:bool -> env -> Evd.evar_map -> types -> constr_expr
+val extern_type : ?lax:bool -> ?goal_concl_style:bool -> env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> types -> constr_expr
 val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort
 val extern_rel_context : constr option -> env -> Evd.evar_map ->
   rel_context -> local_binder_expr list
diff --git a/printing/printer.ml b/printing/printer.ml
index b376616b61..88ca0616dd 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -106,8 +106,8 @@ let pr_letype_env = Proof_diffs.pr_letype_env
 
 let pr_type_env ?lax ?goal_concl_style env sigma c =
   pr_etype_env ?lax ?goal_concl_style env sigma (EConstr.of_constr c)
-let pr_ltype_env ?lax ?goal_concl_style env sigma c =
-  pr_letype_env ?lax ?goal_concl_style env sigma (EConstr.of_constr c)
+let pr_ltype_env ?lax ?goal_concl_style env sigma ?impargs c =
+  pr_letype_env ?lax ?goal_concl_style env sigma ?impargs (EConstr.of_constr c)
 
 let pr_ljudge_env env sigma j =
   (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type)
diff --git a/printing/printer.mli b/printing/printer.mli
index 24d0a8cf6a..dd6d944fe8 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -45,6 +45,10 @@ val enable_goal_names_printing     : bool ref
     intended to be printed in scope [some_scope_name]. It defaults to
     [None].
 
+    [~impargs:some_list_of_binding_kind] indicates the implicit arguments
+    of the external quatification. Only used for printing types (not
+    terms), and at toplevel (only "l" versions). It defaults to [None].
+
     [~lax:true] is for debugging purpose. It defaults to [~lax:false]. *)
 
 
@@ -66,7 +70,7 @@ val pr_leconstr_env     : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -
 val pr_econstr_n_env    : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> EConstr.t -> Pp.t
 
 val pr_etype_env        : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t
-val pr_letype_env       : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t
+val pr_letype_env       : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> ?impargs:Glob_term.binding_kind list -> EConstr.types -> Pp.t
 
 val pr_open_constr_env  : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> open_constr -> Pp.t
 val pr_open_lconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> open_constr -> Pp.t
@@ -97,7 +101,7 @@ val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp
 
     [~lax:true] is for debugging purpose. *)
 
-val pr_ltype_env           : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t
+val pr_ltype_env           : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> ?impargs:Glob_term.binding_kind list -> types -> Pp.t
 val pr_type_env            : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t
 
 val pr_closed_glob_n_env   : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> closed_glob_constr -> Pp.t
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index c3ee5968dc..e9ff06d04e 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -244,9 +244,9 @@ let process_goal sigma g : EConstr.t reified_goal =
   let hyps      = List.map to_tuple hyps in
   { name; ty; hyps; env; sigma };;
 
-let pr_letype_env ?lax ?goal_concl_style env sigma t =
+let pr_letype_env ?lax ?goal_concl_style env sigma ?impargs t =
   Ppconstr.pr_lconstr_expr env sigma
-    (Constrextern.extern_type ?lax ?goal_concl_style env sigma t)
+    (Constrextern.extern_type ?lax ?goal_concl_style env sigma ?impargs t)
 
 let pp_of_type env sigma ty =
   pr_letype_env ~goal_concl_style:true env sigma ty
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
index eebdaccd32..c39146df53 100644
--- a/printing/proof_diffs.mli
+++ b/printing/proof_diffs.mli
@@ -57,7 +57,7 @@ val diff_goal : ?og_s:(Goal.goal sigma) -> Goal.goal -> Evd.evar_map -> Pp.t
 (** Convert a string to a list of token strings using the lexer *)
 val tokenize_string : string -> string list
 
-val pr_letype_env          : ?lax:bool -> ?goal_concl_style:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Pp.t
+val pr_letype_env          : ?lax:bool -> ?goal_concl_style:bool -> Environ.env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> EConstr.types -> Pp.t
 val pr_leconstr_env        : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t
 val pr_lconstr_env         : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> env -> evar_map -> constr -> Pp.t
 
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index cdd93db884..042c1d9013 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 953faf6fdb..3e333db68e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1774,7 +1774,10 @@ 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