diff options
| author | Emilio Jesus Gallego Arias | 2019-12-07 13:45:43 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-12-07 13:45:43 +0100 |
| commit | 756d2f4db5eae51c8c01a40550b8c4553bd30f53 (patch) | |
| tree | c6564c232e5067c2acb48e8c7a4d7ee3ab6ff01a /plugins/ltac | |
| parent | 28c4f57e0614523879201d1c59816cde188e5b22 (diff) | |
| parent | f87ce66b88b74f090c316c8a3c33828a970b2108 (diff) | |
Merge PR #11141: Moving the diversity of constr printers to a label style
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 6df068883c..0e8c225a8f 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1273,7 +1273,7 @@ let pr_intro_pattern_env p = Genprint.TopPrinterNeedsContext (fun env sigma -> Miscprint.pr_intro_pattern print_constr p) let pr_red_expr_env r = Genprint.TopPrinterNeedsContext (fun env sigma -> - pr_red_expr env sigma (pr_econstr_env, pr_leconstr_env, + pr_red_expr env sigma ((fun e -> pr_econstr_env e), (fun e -> pr_leconstr_env e), pr_evaluable_reference_env env, pr_constr_pattern_env) r) let pr_bindings_env bl = Genprint.TopPrinterNeedsContext (fun env sigma -> |