diff options
| author | SimonBoulier | 2020-03-09 19:33:15 +0100 |
|---|---|---|
| committer | SimonBoulier | 2020-03-12 11:22:50 +0100 |
| commit | 50ad4221263d1a3243541a1108e447ac3c1b3742 (patch) | |
| tree | f0317bc5a2ffd09e8c44eb6f02a403e6ab4d737d /printing/printer.mli | |
| parent | dbd3a4c4213b3d56908a8387de93e27aaec501a4 (diff) | |
Print implicit arguments in types of references
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 8 |
1 files changed, 6 insertions, 2 deletions
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 |