From 4fec6bdf0ad0f49c98a82538c5caf4511ba5e95c Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Mon, 15 Dec 2014 17:43:14 +0100
Subject: About now accepts hypothesis names and goal selector.

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

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index f2a6309e38..bc167d94a3 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -74,7 +74,7 @@ type printable =
   | PrintScopes
   | PrintScope of string
   | PrintVisibility of string option
-  | PrintAbout of reference or_by_notation
+  | PrintAbout of reference or_by_notation*int option
   | PrintImplicit of reference or_by_notation
   | PrintAssumptions of bool * bool * reference or_by_notation
   | PrintStrategy of reference or_by_notation option
-- 
cgit v1.2.3