diff options
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 22 |
1 files changed, 17 insertions, 5 deletions
diff --git a/printing/printer.mli b/printing/printer.mli index a469a8db..5c60b893 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -84,7 +84,8 @@ val pr_sort : evar_map -> sorts -> std_ppcmds (** Universe constraints *) val pr_polymorphic : bool -> std_ppcmds -val pr_universe_ctx : Univ.universe_context -> std_ppcmds +val pr_universe_instance : evar_map -> Univ.universe_context -> std_ppcmds +val pr_universe_ctx : evar_map -> Univ.universe_context -> std_ppcmds (** Printing global references using names as short as possible *) @@ -160,12 +161,23 @@ val emacs_str : string -> string val prterm : constr -> std_ppcmds (** = pr_lconstr *) -(** spiwack: printer function for sets of Environ.assumption. - It is used primarily by the Print Assumption command. *) +(** Declarations for the "Print Assumption" command *) +type context_object = + | Variable of Id.t (** A section variable or a Let definition *) + (** An axiom and the type it inhabits (if an axiom of the empty type) *) + | Axiom of constant * (Label.t * Context.rel_context * types) list + | Opaque of constant (** An opaque constant. *) + | Transparent of constant (** A transparent constant *) + +module ContextObjectSet : Set.S with type elt = context_object +module ContextObjectMap : CMap.ExtS + with type key = context_object and module Set := ContextObjectSet + val pr_assumptionset : - env -> Term.types Assumptions.ContextObjectMap.t ->std_ppcmds + env -> Term.types ContextObjectMap.t -> std_ppcmds -val pr_goal_by_id : string -> std_ppcmds +val pr_goal_by_id : Id.t -> std_ppcmds +val pr_goal_by_uid : string -> std_ppcmds type printer_pr = { pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds; |