From be133d7bc92b67a6581a99f7aa679fb3a60ce57b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 7 Nov 2017 16:26:21 +0100
Subject: Extending further PR#6047 (system to register printers for Ltac
 values).

We generalize the possible use of levels to raw and glob printers.

This is potentially useful for printing ltac expressions which are the
glob level.
---
 API/API.mli | 18 +++++++++++-------
 1 file changed, 11 insertions(+), 7 deletions(-)

(limited to 'API')

diff --git a/API/API.mli b/API/API.mli
index 1f1b05eadb..2aa5da67da 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -5217,16 +5217,20 @@ end
 
 module Genprint :
 sig
-  type printer_with_level =
+  type 'a 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 }
+      printer : 'a }
   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
-  type 'a top_printer = 'a -> printer_result
+| PrinterBasic of (unit -> Pp.t)
+| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level
+  type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t
+  type top_printer_result =
+    | TopPrinterBasic of (unit -> Pp.t)
+    | TopPrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
+    | TopPrinterNeedsContextAndLevel of printer_fun_with_level with_level
+  type 'a printer = 'a -> printer_result
+  type 'a top_printer = 'a -> top_printer_result
   val register_print0 : ('raw, 'glb, 'top) Genarg.genarg_type ->
                         'raw printer -> 'glb printer -> 'top top_printer -> unit
   val register_vernac_print0 : ('raw, 'glb, 'top) Genarg.genarg_type ->
-- 
cgit v1.2.3