diff options
| author | Hugo Herbelin | 2019-11-18 16:04:45 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-12-06 17:31:39 +0100 |
| commit | 490704f4b2db98f4ef15f5e380b63e49e13a418b (patch) | |
| tree | 625e60c878e2768dbce36129e1df80ceace17495 /tactics | |
| parent | 28c4f57e0614523879201d1c59816cde188e5b22 (diff) | |
Moving the diversity of constr printers to a label style.
This allows to give access to all printing options (e.g. a scope or
being-in-context) to every printer w/o increasing the numbers of
functions.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 33c9c11350..c44082cd88 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -934,7 +934,7 @@ let is_local_unfold env flags = let reduce redexp cl = let trace env sigma = let open Printer in - let pr = (pr_econstr_env, pr_leconstr_env, pr_evaluable_reference, pr_constr_pattern_env) in + let pr = ((fun e -> pr_econstr_env e), (fun e -> pr_leconstr_env e), pr_evaluable_reference, pr_constr_pattern_env) in Pp.(hov 2 (Ppred.pr_red_expr_env env sigma pr str redexp)) in Proofview.Trace.name_tactic trace begin |