Print implicit arguments in types of references

4 files changed, 11 insertions, 7 deletions

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