diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-05-17 18:19:09 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-17 18:19:09 +0200 |
| commit | 6d770156669dd9868ae7623b8f4302866e2cc8c7 (patch) | |
| tree | c287c2ce79ab183413472f7d65f470bb4eaa64ab /printing/printer.mli | |
| parent | cf90eb14c78d0afd0eb52b8b36152b4e861ccfde (diff) | |
| parent | 697cd5a8e7927873ed6700c7e906ae3675bd98b1 (diff) | |
Merge PR#457: Adding an even more compact goal hyps mode.
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 c28295054..24107394e 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -116,6 +116,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 @@ -137,7 +140,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 |