diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-31 17:18:50 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-02 11:36:41 +0100 |
| commit | 565a9a1b5368c586e529fc9774e4cb4b81c6441b (patch) | |
| tree | 054160a2e7eb5842f8b5e6b7c20fa016b8ae1817 /plugins/ltac/pptactic.mli | |
| parent | b0e9d691d6c48fb09b20bb9d98626143eb8b92df (diff) | |
Setting a system to register printers for Ltac values.
The model provides three kinds of printers depending on whether the
printer needs a context, and, if yes if it supports levels. In the
latter case, it takes defaults levels for printing when in a
surrounded context (lconstr style) and for printing when not in a
surrounded context (constr style).
This model preserves the 8.7 focussing semantics of "idtac"
(i.e. focussing only when an env is needed) but it also shows that the
semantics of "idtac", which focusses the goal depending on the type of
its arguments, is a bit ad hoc to understand.
See discussion at PR#6047
"https://github.com/coq/coq/pull/6047#discussion_r148278454".
Diffstat (limited to 'plugins/ltac/pptactic.mli')
| -rw-r--r-- | plugins/ltac/pptactic.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index b47f07a45..5ecfaf590 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -125,3 +125,6 @@ val pr_value : tolerability -> Val.t -> Pp.t val ltop : tolerability + +val make_constr_printer : (env -> Evd.evar_map -> Notation_term.tolerability -> 'a -> Pp.t) -> + 'a Genprint.top_printer |