diff options
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 35 |
1 files changed, 23 insertions, 12 deletions
diff --git a/printing/printer.mli b/printing/printer.mli index a469a8dbed..70993bb727 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -10,7 +10,6 @@ open Pp open Names open Globnames open Term -open Context open Environ open Pattern open Evd @@ -84,7 +83,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 *) @@ -108,13 +108,13 @@ val pr_pconstructor : env -> pconstructor -> std_ppcmds val pr_context_unlimited : env -> evar_map -> std_ppcmds val pr_ne_context_of : std_ppcmds -> env -> evar_map -> std_ppcmds -val pr_var_decl : env -> evar_map -> named_declaration -> std_ppcmds -val pr_var_list_decl : env -> evar_map -> named_list_declaration -> std_ppcmds -val pr_rel_decl : env -> evar_map -> rel_declaration -> std_ppcmds +val pr_var_decl : env -> evar_map -> Context.Named.Declaration.t -> std_ppcmds +val pr_var_list_decl : env -> evar_map -> Context.NamedList.Declaration.t -> std_ppcmds +val pr_rel_decl : env -> evar_map -> Context.Rel.Declaration.t -> std_ppcmds -val pr_named_context : env -> evar_map -> named_context -> std_ppcmds +val pr_named_context : env -> evar_map -> Context.Named.t -> std_ppcmds val pr_named_context_of : env -> evar_map -> std_ppcmds -val pr_rel_context : env -> evar_map -> rel_context -> std_ppcmds +val pr_rel_context : env -> evar_map -> Context.Rel.t -> std_ppcmds val pr_rel_context_of : env -> evar_map -> std_ppcmds val pr_context_of : env -> evar_map -> std_ppcmds @@ -160,12 +160,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.t * 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; |