diff options
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/printing/printer.mli b/printing/printer.mli index 504392e35..9c9f6e766 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -111,6 +111,9 @@ val pr_pconstructor : env -> pconstructor -> std_ppcmds (** Contexts *) +(** Display compact contexts of goals (simple hyps on the same line) *) +val set_compact_context : bool -> unit +val get_compact_context : unit -> bool val pr_context_unlimited : env -> evar_map -> std_ppcmds val pr_ne_context_of : std_ppcmds -> env -> evar_map -> std_ppcmds @@ -132,7 +135,7 @@ val pr_cpred : Cpred.t -> std_ppcmds val pr_idpred : Id.Pred.t -> std_ppcmds val pr_transparent_state : transparent_state -> std_ppcmds -(** Proofs *) +(** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *) val pr_goal : goal sigma -> std_ppcmds val pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds |