From 84d8a4bd7d797b6e13e4107ad24a6dcf4f098dbb Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 Apr 2016 16:15:31 +0200
Subject: Fixing printing of Register retroknowledge.

---
 printing/ppvernacsig.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'printing')

diff --git a/printing/ppvernacsig.mli b/printing/ppvernacsig.mli
index 5d1c89332c..5e5e4bcf49 100644
--- a/printing/ppvernacsig.mli
+++ b/printing/ppvernacsig.mli
@@ -8,6 +8,9 @@
 
 module type Pp = sig
 
+  (** Prints a fixpoint body *)
+  val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.std_ppcmds
+
   (** Prints a vernac expression *)
   val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.std_ppcmds
 
-- 
cgit v1.2.3