diff options
| author | Emilio Jesus Gallego Arias | 2018-10-02 23:07:43 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-03 15:00:32 +0200 |
| commit | 6e61b19d5509d06d31e5e2e1cb73dbf7d48f8d66 (patch) | |
| tree | 95d77cbb5b312dc2f1633865fd4c1ec86594f3b9 | |
| parent | 10477a2b31e9cddc697b03f75adcc5e42acb0e85 (diff) | |
[api] Be more explicit about deprecation of debug printers.
As suggested by @mattam82
| -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"] |