From 280c922fc55b57c430cad721c83650a796a375fd Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 20 Sep 2017 19:45:43 +0200
Subject: Allow local universe renaming in Print.

---
 printing/printmod.mli | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'printing/printmod.mli')

diff --git a/printing/printmod.mli b/printing/printmod.mli
index b0bbb21e05..97ed063fe3 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -11,6 +11,8 @@ open Names
 (** false iff the module is an element of an open module type *)
 val printable_body : DirPath.t -> bool
 
-val pr_mutual_inductive_body : Environ.env -> MutInd.t -> Declarations.mutual_inductive_body -> Pp.t
+val pr_mutual_inductive_body : Environ.env ->
+  MutInd.t -> Declarations.mutual_inductive_body ->
+  Vernacexpr.univ_name_list option -> Pp.t
 val print_module : bool -> ModPath.t -> Pp.t
 val print_modtype : ModPath.t -> Pp.t
-- 
cgit v1.2.3