diff options
Diffstat (limited to 'parsing/printer.mli')
| -rw-r--r-- | parsing/printer.mli | 112 |
1 files changed, 76 insertions, 36 deletions
diff --git a/parsing/printer.mli b/parsing/printer.mli index c44be124..66471d41 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: printer.mli,v 1.26.2.2 2005/01/21 16:42:37 herbelin Exp $ i*) +(*i $Id: printer.mli 7855 2006-01-12 08:21:57Z herbelin $ i*) (*i*) open Pp @@ -19,42 +19,82 @@ open Rawterm open Pattern open Nametab open Termops +open Evd +open Proof_type +open Rawterm (*i*) (* These are the entry points for printing terms, context, tac, ... *) -(*i -val gentacpr : Tacexpr.raw_tactic_expr -> std_ppcmds -i*) - -val prterm_env : env -> constr -> std_ppcmds -val prterm_env_at_top : env -> constr -> std_ppcmds -val prterm : constr -> std_ppcmds -val prtype_env : env -> types -> std_ppcmds -val prtype : types -> std_ppcmds -val prjudge_env : - env -> Environ.unsafe_judgment -> std_ppcmds * std_ppcmds -val prjudge : Environ.unsafe_judgment -> std_ppcmds * std_ppcmds - -val pr_rawterm : Rawterm.rawconstr -> std_ppcmds -val pr_cases_pattern : Rawterm.cases_pattern -> std_ppcmds - -val pr_constant : env -> constant -> std_ppcmds -val pr_existential : env -> existential -> std_ppcmds -val pr_constructor : env -> constructor -> std_ppcmds -val pr_inductive : env -> inductive -> std_ppcmds -val pr_global : global_reference -> std_ppcmds -val pr_ref_label : constr_label -> std_ppcmds -val pr_pattern : constr_pattern -> std_ppcmds -val pr_pattern_env : env -> names_context -> constr_pattern -> std_ppcmds - -val pr_ne_context_of : std_ppcmds -> env -> std_ppcmds - -val pr_var_decl : env -> named_declaration -> std_ppcmds -val pr_rel_decl : env -> rel_declaration -> std_ppcmds - -val pr_named_context_of : env -> std_ppcmds -val pr_rel_context : env -> rel_context -> std_ppcmds -val pr_context_of : env -> std_ppcmds - -val emacs_str : string -> string +(* Terms *) + +val pr_lconstr_env : env -> constr -> std_ppcmds +val pr_lconstr_env_at_top : env -> constr -> std_ppcmds +val pr_lconstr : constr -> std_ppcmds + +val pr_constr_env : env -> constr -> std_ppcmds +val pr_constr : constr -> std_ppcmds + +val pr_ltype_env : env -> types -> std_ppcmds +val pr_ltype : types -> std_ppcmds + +val pr_type_env : env -> types -> std_ppcmds +val pr_type : types -> std_ppcmds + +val pr_ljudge_env : env -> unsafe_judgment -> std_ppcmds * std_ppcmds +val pr_ljudge : unsafe_judgment -> std_ppcmds * std_ppcmds + +val pr_lrawconstr_env : env -> rawconstr -> std_ppcmds +val pr_lrawconstr : rawconstr -> std_ppcmds + +val pr_rawconstr_env : env -> rawconstr -> std_ppcmds +val pr_rawconstr : rawconstr -> std_ppcmds + +val pr_constr_pattern_env : env -> constr_pattern -> std_ppcmds +val pr_constr_pattern : constr_pattern -> std_ppcmds + +val pr_cases_pattern : cases_pattern -> std_ppcmds + +(* Printing global references using names as short as possible *) + +val pr_global_env : Idset.t -> global_reference -> std_ppcmds +val pr_global : global_reference -> std_ppcmds + +val pr_constant : env -> constant -> std_ppcmds +val pr_existential : env -> existential -> std_ppcmds +val pr_constructor : env -> constructor -> std_ppcmds +val pr_inductive : env -> inductive -> std_ppcmds +val pr_evaluable_reference : evaluable_global_reference -> std_ppcmds + +(* Contexts *) + +val pr_ne_context_of : std_ppcmds -> env -> std_ppcmds + +val pr_var_decl : env -> named_declaration -> std_ppcmds +val pr_rel_decl : env -> rel_declaration -> std_ppcmds + +val pr_named_context : env -> named_context -> std_ppcmds +val pr_named_context_of : env -> std_ppcmds +val pr_rel_context : env -> rel_context -> std_ppcmds +val pr_rel_context_of : env -> std_ppcmds +val pr_context_of : env -> std_ppcmds + +(* Proofs *) + +val pr_goal : goal -> std_ppcmds +val pr_subgoals : evar_map -> goal list -> std_ppcmds +val pr_subgoal : int -> goal list -> std_ppcmds + +val pr_open_subgoals : unit -> std_ppcmds +val pr_nth_open_subgoal : int -> std_ppcmds +val pr_evars_int : int -> (evar * evar_info) list -> std_ppcmds + +val pr_prim_rule : prim_rule -> std_ppcmds + +(* Emacs/proof general support *) + +val emacs_str : string -> string + +(* Backwards compatibility *) + +val prterm : constr -> std_ppcmds (* = pr_lconstr *) |