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.

---
 printing/genprint.ml  | 6 ++++++
 printing/genprint.mli | 2 ++
 2 files changed, 8 insertions(+)

(limited to 'printing')

diff --git a/printing/genprint.ml b/printing/genprint.ml
index 543b05024d..b20ea0b620 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -39,6 +39,12 @@ let register_print0 wit raw glb top =
   let printer = { raw; glb; top; } in
   Print.register0 wit printer
 
+let register_vernac_print0 wit raw =
+  let glb _ = CErrors.anomaly (Pp.str "vernac argument needs not globwit printer.") in
+  let top _ = CErrors.anomaly (Pp.str "vernac argument needs not wit printer.") in
+  let printer = { raw; glb; top; } in
+  Print.register0 wit printer
+
 let raw_print wit v = (Print.obj wit).raw v
 let glb_print wit v = (Print.obj wit).glb v
 let top_print wit v = (Print.obj wit).top v
diff --git a/printing/genprint.mli b/printing/genprint.mli
index 130a89c929..76d80f3b50 100644
--- a/printing/genprint.mli
+++ b/printing/genprint.mli
@@ -27,3 +27,5 @@ val generic_top_print : tlevel generic_argument printer
 
 val register_print0 : ('raw, 'glb, 'top) genarg_type ->
   'raw printer -> 'glb printer -> 'top printer -> unit
+val register_vernac_print0 : ('raw, 'glb, 'top) genarg_type ->
+  'raw printer -> unit
-- 
cgit v1.2.3