diff options
| author | Emilio Jesus Gallego Arias | 2017-12-29 20:20:38 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-09-26 16:33:48 +0200 |
| commit | 7628af7af9ff20d2a894673f66c3753e214623f1 (patch) | |
| tree | bb4c10fea3e44e6949a00d591234cecfc3f345ee /tactics | |
| parent | f49928874b51458fb67e89618bb350ae2f3529e4 (diff) | |
[print] Restrict use of "debug" Termops printer.
The functions in `Termops.print_*` are meant to be debug printers,
however, they are sometimes used in non-debug code due to a API
confusion.
We thus wrap such functions into an `Internal` module, improve
documentation, and switch users to the right API.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 5 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 2 |
2 files changed, 4 insertions, 3 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 3456d13bbe..f3581f17dd 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -693,8 +693,9 @@ module Search = struct let msg = match fst ie with | Pretype_errors.PretypeError (env, evd, Pretype_errors.CannotUnify (x,y,_)) -> - str"Cannot unify " ++ print_constr_env env evd x ++ str" and " ++ - print_constr_env env evd y + str"Cannot unify " ++ + Printer.pr_econstr_env env evd x ++ str" and " ++ + Printer.pr_econstr_env env evd y | ReachedLimitEx -> str "Proof-search reached its limit." | NoApplicableEx -> str "Proof-search failed." | e -> CErrors.iprint ie diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 878e2b1f01..596feeec8b 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -655,7 +655,7 @@ module New = struct | _ -> let name_elim = match EConstr.kind sigma elim with - | Const _ | Var _ -> str " " ++ print_constr_env (pf_env gl) sigma elim + | Const _ | Var _ -> str " " ++ Printer.pr_econstr_env (pf_env gl) sigma elim | _ -> mt () in user_err ~hdr:"Tacticals.general_elim_then_using" |