From a417d138c0a8abc028486c20d59e4f2e82f456ef Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Fri, 12 Dec 2014 15:19:10 +0100
Subject: Searchxxx now search also the hypothesis and support goal selector.

Documentation also updated.
---
 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 6cd56e6a63..f2a6309e38 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -402,7 +402,7 @@ type vernac_expr =
   | VernacGlobalCheck of constr_expr
   | VernacDeclareReduction of string * raw_red_expr
   | VernacPrint of printable
-  | VernacSearch of searchable * search_restriction
+  | VernacSearch of searchable * int option * search_restriction
   | VernacLocate of locatable
   | VernacRegister of lident * register_kind
   | VernacComments of comment list
-- 
cgit v1.2.3