From 5cbcc8fd761df0779f6202fef935f07cfef8a228 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 23 Jan 2016 15:17:29 -0500
Subject: Implement support for universe binder lists in Instance and Program
 Fixpoint/Definition.

---
 printing/ppvernac.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index d2f59e7b8d..38add9d2c8 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -925,8 +925,9 @@ module Make
             hov 1 (
               (if abst then keyword "Declare" ++ spc () else mt ()) ++
                 keyword "Instance" ++
-                (match snd instid with Name id -> spc () ++ pr_lident (fst instid, id) ++ spc () |
-                    Anonymous -> mt ()) ++
+                (match instid with
+		 | (loc, Name id), l -> spc () ++ pr_plident ((loc, id),l) ++ spc () 
+                 | (_, Anonymous), _ -> mt ()) ++
                 pr_and_type_binders_arg sup ++
                 str":" ++ spc () ++
                 pr_constr cl ++ pr_priority pri ++
-- 
cgit v1.2.3