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.

---
 API/API.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index e207930771..608bd43cd8 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4977,6 +4977,8 @@ sig
   val generic_top_print : Genarg.tlevel Genarg.generic_argument printer
   val register_print0 : ('raw, 'glb, 'top) Genarg.genarg_type ->
                         'raw printer -> 'glb printer -> 'top printer -> unit
+  val register_vernac_print0 : ('raw, 'glb, 'top) Genarg.genarg_type ->
+                        'raw printer -> unit
 end
 
 module Pputils :
-- 
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".
---
 API/API.mli | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index 608bd43cd8..589745b616 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4973,12 +4973,23 @@ end
 
 module Genprint :
 sig
+  type printer_with_level =
+    { default_already_surrounded : Notation_term.tolerability;
+      default_ensure_surrounded : Notation_term.tolerability;
+      printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t }
+  type printer_result =
+    | PrinterBasic of (unit -> Pp.t)
+    | PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
+    | PrinterNeedsContextAndLevel of printer_with_level
   type 'a printer = 'a -> Pp.t
-  val generic_top_print : Genarg.tlevel Genarg.generic_argument printer
+  type 'a top_printer = 'a -> printer_result
   val register_print0 : ('raw, 'glb, 'top) Genarg.genarg_type ->
-                        'raw printer -> 'glb printer -> 'top printer -> unit
+                        'raw printer -> 'glb printer -> 'top top_printer -> unit
   val register_vernac_print0 : ('raw, 'glb, 'top) Genarg.genarg_type ->
                         'raw printer -> unit
+  val register_val_print0 : 'top Geninterp.Val.typ -> 'top top_printer -> unit
+  val generic_top_print : Genarg.tlevel Genarg.generic_argument top_printer
+  val generic_val_print : Geninterp.Val.t top_printer
 end
 
 module Pputils :
@@ -4999,6 +5010,8 @@ sig
   val pr_name : Names.Name.t -> Pp.t
   [@@ocaml.deprecated "alias of API.Names.Name.print"]
 
+  val lsimpleconstr : Notation_term.tolerability
+  val ltop : Notation_term.tolerability
   val pr_id : Names.Id.t -> Pp.t
   val pr_or_var : ('a -> Pp.t) -> 'a Misctypes.or_var -> Pp.t
   val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t
@@ -5031,6 +5044,7 @@ sig
   val pr_constr_pattern : Pattern.constr_pattern -> Pp.t
   val pr_glob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.t
   val pr_lglob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.t
+  val pr_econstr_n_env : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> EConstr.constr -> Pp.t
   val pr_econstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t
   val pr_constr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t
   val pr_lconstr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t
@@ -5043,6 +5057,7 @@ sig
   val pr_lconstr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t
 
   val pr_constr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t
+  val pr_closed_glob_n_env : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Ltac_pretype.closed_glob_constr -> Pp.t
   val pr_closed_glob_env : Environ.env -> Evd.evar_map -> Ltac_pretype.closed_glob_constr -> Pp.t
   val pr_rel_context_of : Environ.env -> Evd.evar_map -> Pp.t
   val pr_named_context_of : Environ.env -> Evd.evar_map -> Pp.t
-- 
cgit v1.2.3