aboutsummaryrefslogtreecommitdiff
path: root/engine/evd.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-11-29 23:48:28 +0100
committerPierre-Marie Pédrot2017-02-14 17:30:44 +0100
commit27fbf069ccd846383bcfb35ba1ea5bd1d95090a0 (patch)
tree7f69b79408e4433227d59655d78342108bfed540 /engine/evd.mli
parent390fd4ac0a969103caeb5db3e5138e26f9a533de (diff)
Moving printing code from Evd to Termops.
Diffstat (limited to 'engine/evd.mli')
-rw-r--r--engine/evd.mli16
1 files changed, 0 insertions, 16 deletions
diff --git a/engine/evd.mli b/engine/evd.mli
index eeb9fd8618..fc1d4a5142 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -584,22 +584,6 @@ type open_constr = evar_map * constr (* Special case when before is empty *)
type unsolvability_explanation = SeveralInstancesFound of int
(** Failure explanation. *)
-val pr_existential_key : evar_map -> evar -> Pp.std_ppcmds
-
-val pr_evar_suggested_name : existential_key -> evar_map -> Id.t
-
-(** {5 Debug pretty-printers} *)
-
-val print_constr_hook : (Environ.env -> evar_map -> constr -> Pp.std_ppcmds) Hook.t
-val pr_evar_info : evar_info -> Pp.std_ppcmds
-val pr_evar_constraints : evar_constraint list -> Pp.std_ppcmds
-val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.std_ppcmds
-val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) ->
- evar_map -> Pp.std_ppcmds
-val pr_metaset : Metaset.t -> Pp.std_ppcmds
-val pr_evar_universe_context : evar_universe_context -> Pp.std_ppcmds
-val pr_evd_level : evar_map -> Univ.Level.t -> Pp.std_ppcmds
-
(** {5 Deprecated functions} *)
val create_evar_defs : evar_map -> evar_map