diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-05-03 11:37:08 +0200 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-05-03 18:50:04 +0200 |
| commit | 952e9aea47d3fad2d0f488d968ff0e90fa403ebc (patch) | |
| tree | 28abee0a59949e89a15e748a014a331af04fdf75 /printing/printer.mli | |
| parent | 3c795ba6b5728e8a0a699ab15c773c52c48f33e4 (diff) | |
Adding an even more compact mode for goal display.
We want to print variables in vertical boxes as much as possible.
The criterion to distinguish "variable" from "hypothesis" is not
obvious. We chose this one but may change it in the future:
X:T is a variable if T is not of type Prop AND T is "simple" which
means T is either id or (t T1 .. Tn) Ti's are sort-typed (typicall
Ti:Type, but not Ti:nat).
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 |