diff options
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 22 |
1 files changed, 5 insertions, 17 deletions
diff --git a/printing/printer.mli b/printing/printer.mli index 41843680b..7a8b963d2 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Globnames open Constr open Environ open Pattern @@ -37,7 +36,7 @@ val pr_constr : constr -> Pp.t [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t -val pr_constr_n_env : env -> evar_map -> Notation_term.tolerability -> constr -> Pp.t +val pr_constr_n_env : env -> evar_map -> Notation_gram.tolerability -> constr -> Pp.t (** Same, but resilient to [Nametab] errors. Prints fully-qualified names when [shortest_qualid_of_global] has failed. Prints "??" @@ -58,7 +57,7 @@ val pr_leconstr_env : env -> evar_map -> EConstr.t -> Pp.t val pr_leconstr : EConstr.t -> Pp.t [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] -val pr_econstr_n_env : env -> evar_map -> Notation_term.tolerability -> EConstr.t -> Pp.t +val pr_econstr_n_env : env -> evar_map -> Notation_gram.tolerability -> EConstr.t -> Pp.t val pr_etype_env : env -> evar_map -> EConstr.types -> Pp.t val pr_letype_env : env -> evar_map -> EConstr.types -> Pp.t @@ -88,7 +87,7 @@ val pr_type_env : env -> evar_map -> types -> Pp.t val pr_type : types -> Pp.t [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] -val pr_closed_glob_n_env : env -> evar_map -> Notation_term.tolerability -> closed_glob_constr -> Pp.t +val pr_closed_glob_n_env : env -> evar_map -> Notation_gram.tolerability -> closed_glob_constr -> Pp.t val pr_closed_glob_env : env -> evar_map -> closed_glob_constr -> Pp.t val pr_closed_glob : closed_glob_constr -> Pp.t [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] @@ -130,8 +129,8 @@ val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t (** Printing global references using names as short as possible *) -val pr_global_env : Id.Set.t -> global_reference -> Pp.t -val pr_global : global_reference -> Pp.t +val pr_global_env : Id.Set.t -> GlobRef.t -> Pp.t +val pr_global : GlobRef.t -> Pp.t val pr_constant : env -> Constant.t -> Pp.t val pr_existential_key : evar_map -> Evar.t -> Pp.t @@ -223,14 +222,3 @@ val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t -type printer_pr = { - pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused:goal list -> goals:goal list -> Pp.t; - - pr_subgoal : int -> evar_map -> goal list -> Pp.t; - pr_goal : goal sigma -> Pp.t; -} - -val set_printer_pr : printer_pr -> unit - -val default_printer_pr : printer_pr - |