diff options
| author | Pierre-Marie Pédrot | 2018-10-04 10:57:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-04 10:57:25 +0200 |
| commit | 4b2c12fddf2dfad949eea44326da87b11f614772 (patch) | |
| tree | 75507f89f1dea560dabdfe1b4589dd4f5bdca2ba | |
| parent | 53929e9bacf251f60c85d4ff24d46fec2c42ab4b (diff) | |
| parent | 6e61b19d5509d06d31e5e2e1cb73dbf7d48f8d66 (diff) | |
Merge PR #8639: [api] Be more explicit about deprecation of debug printers.
| -rw-r--r-- | engine/termops.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/engine/termops.mli b/engine/termops.mli index aa0f837938..0e5d564d3f 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -341,10 +341,10 @@ val print_constr : constr -> Pp.t end val print_constr : constr -> Pp.t -[@@deprecated "use Internal.print_constr_env"] +[@@deprecated "This is an internal, debug printer. WARNING, it is *extremely* likely that you want to use [Printer.pr_econstr_env] instead"] val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t -[@@deprecated "use Internal.print_constr_env"] +[@@deprecated "This is an internal, debug printer. WARNING, it is *extremely* likely that you want to use [Printer.pr_econstr_env] instead"] val print_rel_context : env -> Pp.t -[@@deprecated "use Internal.print_rel_context"] +[@@deprecated "This is an internal, debug printer. WARNING, this function is not suitable for plugin code, if you still want to use it then call [Internal.print_rel_context] instead"] |