From fb57fefa5f46ba8ad7be98cff81354389d87d402 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 30 Oct 2017 12:18:11 +0100
Subject: Exporting a few more printing functions.

---
 plugins/ltac/pptactic.mli | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'plugins/ltac/pptactic.mli')

diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index d9da954fe6..058b205697 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -69,11 +69,16 @@ val pr_may_eval :
 val pr_and_short_name : ('a -> Pp.t) -> 'a and_short_name -> Pp.t
 val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t
 
+val pr_evaluable_reference_env : env -> evaluable_global_reference -> Pp.t
+
+val pr_quantified_hypothesis : quantified_hypothesis -> Pp.t
+
 val pr_in_clause :
   ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t
 
-val pr_clauses :  bool option ->
+val pr_clauses : (* default: *) bool option ->
   ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t
+  (* Some true = default is concl; Some false = default is all; None = no default *)
 
 val pr_raw_generic : env -> rlevel generic_argument -> Pp.t
 
-- 
cgit v1.2.3


From 767816eece27e6bb8cba0bbf122507bd2a3b77a1 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 1 Nov 2017 22:54:24 +0100
Subject: Using a specific function to register vernac printers.

---
 plugins/ltac/pptactic.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'plugins/ltac/pptactic.mli')

diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 058b205697..b47f07a453 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -46,6 +46,10 @@ val declare_extra_genarg_pprule :
   'b glob_extra_genarg_printer ->
   'c extra_genarg_printer -> unit
 
+val declare_extra_vernac_genarg_pprule :
+  ('a, 'b, 'c) genarg_type ->
+  'a raw_extra_genarg_printer -> unit
+
 type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list
 
 type pp_tactic = {
-- 
cgit v1.2.3


From 565a9a1b5368c586e529fc9774e4cb4b81c6441b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 31 Oct 2017 17:18:50 +0100
Subject: 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".
---
 plugins/ltac/pptactic.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'plugins/ltac/pptactic.mli')

diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index b47f07a453..5ecfaf590c 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
-- 
cgit v1.2.3