Searchxxx now search also the hypothesis and support goal selector.

Documentation also updated.

10 files changed, 138 insertions, 67 deletions

diff --git a/CHANGES b/CHANGES
index b1946188b..5c1a27fa6 100644
--- a/CHANGES
+++ b/CHANGES
@@ -52,6 +52,11 @@ Vernacular commands
 - Command "Search" has been renamed into "SearchHead". The command
   name "Search" now behaves like former "SearchAbout". The latter name
   is deprecated.
+- "Search" "SearchHead" "SearchRewrite" and "SearchPattern" now search
+  for hypothesis (of the current goal) first. They now also support the
+  goal selector prefix to specify another goal to search: e.g.
+  "n:Search id". This is also true for SearchAbout although it is
+  deprecated.
 - The coq/user-contrib directory and the XDG directories are no longer
   recursively added to the load path, so files from installed libraries
   now need to be fully qualified for the "Require" command to find them.
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 121b608d0..e4c83a59c 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -146,6 +146,13 @@ This is a synonymous of {\tt Print Options.}
 This command displays the type of {\term}. When called in proof mode, 
 the term is checked in the local context of the current subgoal.
 
+\begin{Variants}
+\item {\tt selector: Check {\term}}.\\
+specifies on which subgoal to perform typing (see
+  Section~\ref{tactic-syntax}).
+\end{Variants}
+
+
 \subsection[\tt Eval {\rm\sl convtactic} in {\term}.]{\tt Eval {\rm\sl convtactic} in {\term}.\comindex{Eval}}
 
 This command performs the specified reduction on {\term}, and displays
@@ -203,10 +210,10 @@ relies.
 \end{Variants}
 
 \subsection[\tt Search {\qualid}.]{\tt Search {\qualid}.\comindex{Search}}
-This command displays the name and type of all objects (theorems,
-axioms, etc) of the current context whose statement contains \qualid.
-This command is useful to remind the user of the name of library
-lemmas.
+This command displays the name and type of all objects (hypothesis of
+the current goal, theorems, axioms, etc) of the current context whose
+statement contains \qualid. This command is useful to remind the user
+of the name of library lemmas.
 
 \begin{ErrMsgs}
 \item \errindex{The reference \qualid\ was not found in the current
@@ -268,6 +275,11 @@ This restricts the search to constructions defined in modules
 This restricts the search to constructions not defined in modules
 {\module$_1$} \ldots{} {\module$_n$}.
 
+\item {\tt selector: Search \nelist{\zeroone{-}{\termpatternorstr}}{}.}
+
+  This specifies the goal on which to search hypothesis (see
+  Section~\ref{tactic-syntax}). By default the 1st goal is searched.
+  This variant can be combined with other variants presented here.
 \end{Variants}
 
 \examples
@@ -290,8 +302,9 @@ search when using {\tt SearchAbout} may also be enclosed by optional
 {\tt [ ]} delimiters.
 
 \subsection[\tt SearchHead {\term}.]{\tt SearchHead {\term}.\comindex{SearchHead}}
-This command displays the name and type of all theorems of the current
-context whose statement's conclusion has the form {\tt ({\term} t1 ..
+This command displays the name and type of all hypothesis of the
+current goal (if any) and theorems of the current context whose
+statement's conclusion has the form {\tt ({\term} t1 ..
   tn)}.  This command is useful to remind the user of the name of
 library lemmas.
 
@@ -321,16 +334,23 @@ This restricts the search to constructions not defined in modules
 No module \module{} has been required (see Section~\ref{Require}).
 \end{ErrMsgs}
 
+\item {\tt selector: SearchHead {\term}.}
+
+  This specifies the goal on which to search hypothesis (see
+  Section~\ref{tactic-syntax}). By default the 1st goal is searched.
+  This variant can be combined with other variants presented here.
+
 \end{Variants}
 
 \Warning Up to Coq version 8.4, {\tt SearchHead} was named {\tt Search}.
 
 \subsection[\tt SearchPattern {\termpattern}.]{\tt SearchPattern {\term}.\comindex{SearchPattern}}
 
-This command displays the name and type of all theorems of the current
-context whose statement's conclusion or last hypothesis and conclusion
-matches the expression {\term} where holes in the latter are denoted
-by ``{\texttt \_}''. It is a variant of {\tt Search
+This command displays the name and type of all hypothesis of the
+current goal (if any) and theorems of the current context whose statement's
+conclusion or last hypothesis and conclusion matches the expression
+{\term} where holes in the latter are denoted by ``{\texttt \_}''. It
+is a variant of {\tt Search
   {\termpattern}} that does not look for subterms but searches for
 statements whose conclusion has exactly the expected form, or whose
 statement finishes by the given series of hypothesis/conclusion.
@@ -363,13 +383,20 @@ This restricts the search to constructions defined in modules
 This restricts the search to constructions not defined in modules
 {\module$_1$} \ldots{} {\module$_n$}.
 
+\item {\tt selector: SearchPattern {\term}.}
+
+  This specifies the goal on which to search hypothesis (see
+  Section~\ref{tactic-syntax}). By default the 1st goal is searched.
+  This variant can be combined with other variants presented here.
+
 \end{Variants}
 
 \subsection[\tt SearchRewrite {\term}.]{\tt SearchRewrite {\term}.\comindex{SearchRewrite}}
 
-This command displays the name and type of all theorems of the current
-context whose statement's conclusion is an equality of which one side matches
-the expression {\term}. Holes in {\term} are denoted by ``{\texttt \_}''.
+This command displays the name and type of all hypothesis of the
+current goal (if any) and theorems of the current context whose
+statement's conclusion is an equality of which one side matches the
+expression {\term}. Holes in {\term} are denoted by ``{\texttt \_}''.
 
 \begin{coq_example}
 Require Import Arith.
@@ -388,6 +415,12 @@ This restricts the search to constructions defined in modules
 This restricts the search to constructions not defined in modules
 {\module$_1$} \ldots{} {\module$_n$}.
 
+\item {\tt selector: SearchRewrite {\term}.}
+
+  This specifies the goal on which to search hypothesis (see
+  Section~\ref{tactic-syntax}). By default the 1st goal is searched.
+  This variant can be combined with other variants presented here.
+
 \end{Variants}
 
 \subsubsection{Nota Bene:}
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 6cd56e6a6..f2a6309e3 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
diff --git a/lib/util.ml b/lib/util.ml
index 531e4fe7d..cfb4ebabc 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -105,6 +105,11 @@ let app_opt f x =
   | Some f -> f x
   | None -> x
 
+let un_opt x default =
+  match x with
+  | None -> default
+  | Some y -> y
+
 (* Stream *)
 
 let stream_nth n st =
diff --git a/lib/util.mli b/lib/util.mli
index 86720fe47..bcb1b6265 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -89,6 +89,10 @@ val iterate : ('a -> 'a) -> int -> 'a -> 'a
 val repeat : int -> ('a -> unit) -> 'a -> unit
 val app_opt : ('a -> 'a) option -> 'a -> 'a
 
+(** [un_opt opt default] returns the content of [opt] if possible and
+    default otherwise. *)
+val un_opt : 'a option -> 'a -> 'a
+
 (** {6 Delayed computations. } *)
 
 type 'a delayed = unit -> 'a
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 07ce048ea..3ae7bd92c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -32,7 +32,7 @@ let _ = List.iter Lexer.add_keyword vernac_kw
 (* Rem: do not join the different GEXTEND into one, it breaks native *)
 (* compilation on PowerPC and Sun architectures *)
 
-let check_command = Gram.entry_create "vernac:check_command"
+let query_command = Gram.entry_create "vernac:query_command"
 
 let tactic_mode = Gram.entry_create "vernac:tactic_command"
 let noedit_mode = Gram.entry_create "vernac:noedit_command"
@@ -145,7 +145,7 @@ GEXTEND Gram
   ;
 
   subgoal_command: 
-    [ [ c = check_command; "." ->
+    [ [ c = query_command; "." ->
                   begin function
                     | Some (SelectNth g) -> c (Some g)
                     | None -> c None
@@ -733,7 +733,7 @@ GEXTEND Gram
 END
 
 GEXTEND Gram
-  GLOBAL: command check_command class_rawexpr;
+  GLOBAL: command query_command class_rawexpr;
 
   command:
     [ [ IDENT "Ltac";
@@ -796,22 +796,6 @@ GEXTEND Gram
       | IDENT "Inspect"; n = natural -> VernacPrint (PrintInspect n)
       | IDENT "About"; qid = smart_global -> VernacPrint (PrintAbout qid)
 
-      (* Searching the environment *)
-      | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules ->
-	  VernacSearch (SearchHead c, l)
-      | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules ->
-	  VernacSearch (SearchPattern c, l)
-      | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules ->
-	  VernacSearch (SearchRewrite c, l)
-      | IDENT "Search"; s = searchabout_query; l = searchabout_queries ->
-	  let (sl,m) = l in VernacSearch (SearchAbout (s::sl), m)
-      (* compatibility: SearchAbout *)
-      | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries ->
-	  let (sl,m) = l in VernacSearch (SearchAbout (s::sl), m)
-      (* compatibility: SearchAbout with "[ ... ]" *)
-      | IDENT "SearchAbout"; "["; sl = LIST1 searchabout_query; "]";
-	  l = in_or_out_modules -> VernacSearch (SearchAbout sl, l)
-
       | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = ne_string ->
 	  VernacAddMLPath (false, dir)
       | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = ne_string ->
@@ -847,13 +831,29 @@ GEXTEND Gram
       | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value ->
 	  VernacRemoveOption ([table], v) ]] 
   ;
-  check_command: (* TODO: rapprocher Eval et Check *)
+  query_command: (* TODO: rapprocher Eval et Check *)
     [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr ->
           fun g -> VernacCheckMayEval (Some r, g, c)
       | IDENT "Compute"; c = lconstr ->
 	  fun g -> VernacCheckMayEval (Some (Genredexpr.CbvVm None), g, c)
       | IDENT "Check"; c = lconstr ->
-	  fun g -> VernacCheckMayEval (None, g, c) ] ]
+	 fun g -> VernacCheckMayEval (None, g, c)
+      (* Searching the environment *)
+      | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules ->
+	  fun g -> VernacSearch (SearchHead c,g, l)
+      | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules ->
+	  fun g -> VernacSearch (SearchPattern c,g, l)
+      | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules ->
+	  fun g -> VernacSearch (SearchRewrite c,g, l)
+      | IDENT "Search"; s = searchabout_query; l = searchabout_queries ->
+	  let (sl,m) = l in fun g -> VernacSearch (SearchAbout (s::sl),g, m)
+      (* compatibility: SearchAbout *)
+      | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries ->
+	  fun g -> let (sl,m) = l in VernacSearch (SearchAbout (s::sl),g, m)
+      (* compatibility: SearchAbout with "[ ... ]" *)
+      | IDENT "SearchAbout"; "["; sl = LIST1 searchabout_query; "]";
+	  l = in_or_out_modules -> fun g -> VernacSearch (SearchAbout sl,g, l)
+      ] ]
   ;
   printable:
     [ [ IDENT "Term"; qid = smart_global -> PrintName qid
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 92d94bdc3..2755b98c6 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -127,11 +127,15 @@ module Make
         | SearchSubPattern p -> pr_constr_pattern_expr p
         | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
 
-  let pr_search a b pr_p = match a with
-    | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b
-    | SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b
-    | SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b
-    | SearchAbout sl -> keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b
+  let pr_search a gopt b pr_p =
+    pr_opt (fun g -> int g ++ str ":"++ spc()) gopt
+    ++
+      match a with
+      | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b
+      | SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b
+      | SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b
+      | SearchAbout sl ->
+	 keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b
 
   let pr_locality local = if local then keyword "Local" else keyword "Global"
 
@@ -1167,8 +1171,8 @@ module Make
           )
         | VernacPrint p ->
           return (pr_printable p)
-        | VernacSearch (sea,sea_r) ->
-          return (pr_search sea sea_r pr_constr_pattern_expr)
+        | VernacSearch (sea,g,sea_r) ->
+          return (pr_search sea g sea_r pr_constr_pattern_expr)
         | VernacLocate loc ->
           let pr_locate =function
             | LocateAny qid -> pr_smart_global qid
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 9632e1c79..8336b488a 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -49,6 +49,18 @@ let iter_constructors indsp u fn env nconstr =
     fn (ConstructRef (indsp, i)) env typ
   done
 
+let iter_named_context_name_type f = List.iter (fun (nme,_,typ) -> f nme typ) 
+
+(* General search over hypothesis of a goal *)
+let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) =
+  try
+    let env = Global.env () in
+    let iter_hyp idh typ = fn (VarRef idh) env typ in
+    let evmap,e = Pfedit.get_goal_context glnum in
+    let pfctxt = named_context e in
+    iter_named_context_name_type iter_hyp pfctxt
+  with _ -> ()
+
 (* General search over declarations *)
 let iter_declarations (fn : global_reference -> env -> constr -> unit) =
   let env = Global.env () in
@@ -81,7 +93,9 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) =
   try Declaremods.iter_all_segments iter_obj
   with Not_found -> ()
 
-let generic_search = iter_declarations
+let generic_search glnum fn =
+  iter_hypothesis glnum fn;
+  iter_declarations fn
 
 (** Standard display *)
 
@@ -118,8 +132,8 @@ let full_name_of_reference ref =
 
 (** Whether a reference is blacklisted *)
 let blacklist_filter ref env typ =
-  let name = full_name_of_reference ref in
   let l = SearchBlacklist.elements () in
+  let name = full_name_of_reference ref in
   let is_not_bl str = not (String.string_contains ~where:name ~what:str) in
   List.for_all is_not_bl l
 
@@ -142,7 +156,7 @@ let search_about_filter query gr env typ = match query with
 
 (** SearchPattern *)
 
-let search_pattern pat mods =
+let search_pattern g pat mods =
   let ans = ref [] in
   let filter ref env typ =
     let f_module = module_filter mods ref env typ in
@@ -153,7 +167,7 @@ let search_pattern pat mods =
   let iter ref env typ =
     if filter ref env typ then plain_display ans ref env typ
   in
-  let () = generic_search iter in
+  let () = generic_search g iter in
   format_display !ans
 
 (** SearchRewrite *)
@@ -166,7 +180,7 @@ let rewrite_pat1 pat =
 let rewrite_pat2 pat =
   PApp (PRef eq, [| PMeta None; PMeta None; pat |])
 
-let search_rewrite pat mods =
+let search_rewrite g pat mods =
   let pat1 = rewrite_pat1 pat in
   let pat2 = rewrite_pat2 pat in
   let ans = ref [] in
@@ -182,12 +196,12 @@ let search_rewrite pat mods =
   let iter ref env typ =
     if filter ref env typ then plain_display ans ref env typ
   in
-  let () = generic_search iter in
+  let () = generic_search g iter in
   format_display !ans
 
 (** Search *)
 
-let search_by_head pat mods =
+let search_by_head g pat mods =
   let ans = ref [] in
   let filter ref env typ =
     let f_module = module_filter mods ref env typ in
@@ -198,12 +212,12 @@ let search_by_head pat mods =
   let iter ref env typ =
     if filter ref env typ then plain_display ans ref env typ
   in
-  let () = generic_search iter in
+  let () = generic_search g iter in
   format_display !ans
 
 (** SearchAbout *)
 
-let search_about items mods =
+let search_about g items mods =
   let ans = ref [] in
   let filter ref env typ =
     let eqb b1 b2 = if b1 then b2 else not b2 in
@@ -215,7 +229,7 @@ let search_about items mods =
   let iter ref env typ =
     if filter ref env typ then plain_display ans ref env typ
   in
-  let () = generic_search iter in
+  let () = generic_search g iter in
   format_display !ans
 
 type search_constraint =
@@ -319,5 +333,5 @@ let interface_search flags =
   let iter ref env typ =
     if filter_function ref env typ then print_function ref env typ
   in
-  let () = generic_search iter in
+  let () = generic_search 1 iter in (* TODO: chose a goal number? *)
   !ans
diff --git a/toplevel/search.mli b/toplevel/search.mli
index a69a8db79..f5d1d13ed 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.mli
@@ -33,13 +33,17 @@ val module_filter : DirPath.t list * bool -> filter_function
 val search_about_filter : glob_search_about_item -> filter_function
 (** Check whether a reference matches a SearchAbout query. *)
 
-(** {6 Specialized search functions} *)
+(** {6 Specialized search functions}
 
-val search_by_head : constr_pattern -> DirPath.t list * bool -> std_ppcmds
-val search_rewrite : constr_pattern -> DirPath.t list * bool -> std_ppcmds
-val search_pattern : constr_pattern -> DirPath.t list * bool -> std_ppcmds
-val search_about   : (bool * glob_search_about_item) list ->
-  DirPath.t list * bool -> std_ppcmds
+[search_xxx gl pattern modinout] searches the hypothesis of the [gl]th
+goal and the global environment for things matching [pattern] and
+satisfying module exclude/include clauses of [modinout]. *)
+
+val search_by_head : int -> constr_pattern -> DirPath.t list * bool -> std_ppcmds
+val search_rewrite : int -> constr_pattern -> DirPath.t list * bool -> std_ppcmds
+val search_pattern : int -> constr_pattern -> DirPath.t list * bool -> std_ppcmds
+val search_about   : int -> (bool * glob_search_about_item) list
+  -> DirPath.t list * bool -> std_ppcmds
 
 type search_constraint =
   (** Whether the name satisfies a regexp (uses Ocaml Str syntax) *)
@@ -64,5 +68,6 @@ val interface_search : (search_constraint * bool) list ->
 
 (** {6 Generic search function} *)
 
-val generic_search : display_function -> unit
-(** This function iterates over all known declarations *)
+val generic_search : int -> display_function -> unit
+(** This function iterates over all hypothesis of the goal numbered
+    [glnum] (if present) and all known declarations. *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 93c12c335..8fb2d320c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1610,19 +1610,20 @@ let interp_search_about_item = function
 	error ("Unable to interp \""^s^"\" either as a reference or \
           	as an identifier component")
 
-let vernac_search s r =
+let vernac_search s gopt r =
+  let g = un_opt gopt 1 in
   let r = interp_search_restriction r in
   let env = Global.env () in
   let get_pattern c = snd (Constrintern.intern_constr_pattern env c) in
   match s with
   | SearchPattern c ->
-      msg_notice (Search.search_pattern (get_pattern c) r)
+      msg_notice (Search.search_pattern g (get_pattern c) r)
   | SearchRewrite c ->
-      msg_notice (Search.search_rewrite (get_pattern c) r)
+      msg_notice (Search.search_rewrite g (get_pattern c) r)
   | SearchHead c ->
-      msg_notice (Search.search_by_head (get_pattern c) r)
+      msg_notice (Search.search_by_head g (get_pattern c) r)
   | SearchAbout sl ->
-      msg_notice (Search.search_about (List.map (on_snd interp_search_about_item) sl) r)
+     msg_notice (Search.search_about g (List.map (on_snd interp_search_about_item) sl) r)
 
 let vernac_locate = function
   | LocateAny (AN qid) -> msg_notice (print_located_qualid qid)
@@ -1886,7 +1887,7 @@ let interp ?proof locality poly c =
   | VernacDeclareReduction (s,r) -> vernac_declare_reduction locality s r
   | VernacGlobalCheck c -> vernac_global_check c
   | VernacPrint p -> vernac_print p
-  | VernacSearch (s,r) -> vernac_search s r
+  | VernacSearch (s,g,r) -> vernac_search s g r
   | VernacLocate l -> vernac_locate l
   | VernacRegister (id, r) -> vernac_register id r
   | VernacComments l -> if_verbose msg_info (str "Comments ok\n")