From 952e9aea47d3fad2d0f488d968ff0e90fa403ebc Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Wed, 3 May 2017 11:37:08 +0200 Subject: 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). --- printing/printer.mli | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'printing/printer.mli') 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 -- cgit v1.2.3