From 26ed8658149d14efa6e4d077c573481281cb610e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Sat, 27 Aug 2016 06:48:46 +0200
Subject: Support qualified identifiers in Show Match (bug #5050).

---
 intf/vernacexpr.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf/vernacexpr.mli')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 156e00368..ed44704df 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -106,7 +106,7 @@ type showable =
   | ShowTree
   | ShowProofNames
   | ShowIntros of bool
-  | ShowMatch of lident
+  | ShowMatch of reference
   | ShowThesis
 
 type comment =
-- 
cgit v1.2.3