Backporting 11445 from 8.2 to trunk (negative conditions in

SearchAbout + referring objects by their notation).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11446 85f007b7-540e-0410-9357-904b9bb8a0f7

21 files changed, 197 insertions, 127 deletions

diff --git a/CHANGES b/CHANGES
index 47f131ce9f..6550be7059 100644
--- a/CHANGES
+++ b/CHANGES
@@ -66,6 +66,8 @@ Vernacular commands
   or axioms a theorem or definition relies on.
 - "Add Rec LoadPath" now provides references to libraries using partially
   qualified names (this holds also for coqtop/coqc option -R).
+- SearchAbout supports negated search criteria and reference to logical objects
+  by their notation.
 
 Libraries (DOC TO CHECK)
 
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index a4dc0eacd3..e7c7fde8dd 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -546,7 +546,9 @@ let abort_hook s = output_results_nl (ctf_AbortedMessage !global_request_id s)
 
 let interp_search_about_item = function
   | SearchRef qid -> GlobSearchRef (Nametab.global qid)
-  | SearchString s -> GlobSearchString s
+  | SearchString (s,_) ->
+      warning "Notation case not taken into account";
+      GlobSearchString s
 
 let pcoq_search s l =
   (* LEM: I don't understand why this is done in this way (redoing the
@@ -559,7 +561,7 @@ let pcoq_search s l =
   begin match s with
   | SearchAbout sl -> 
       raw_search_about (filter_by_module_from_list l) add_search
-	(List.map interp_search_about_item sl)
+	(List.map (on_snd interp_search_about_item) sl)
   | SearchPattern c ->
       let _,pat = interp_constrpattern Evd.empty (Global.env()) c in
       raw_pattern_search (filter_by_module_from_list l) add_search pat
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 3421125369..8c470f1bd7 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1944,12 +1944,15 @@ let rec xlate_vernac =
 	| SearchRewrite c ->
 	    CT_search_rewrite(xlate_formula c, translated_restriction)
 	| SearchAbout (a::l) ->
-	    let xlate_search_about_item it =
+	    let xlate_search_about_item (b,it) =
+              if not b then xlate_error "TODO: negative searchabout constraint";
 	      match it with
 		  SearchRef x -> 
 		    CT_coerce_ID_to_ID_OR_STRING(loc_qualid_to_ct_ID x)
-		| SearchString s -> 
-		    CT_coerce_STRING_to_ID_OR_STRING(CT_string s) in
+		| SearchString (s,None) -> 
+		    CT_coerce_STRING_to_ID_OR_STRING(CT_string s)
+		| SearchString (s,_) ->
+                    xlate_error "TODO: notation with explicit scope" in
 	    CT_search_about
 	      (CT_id_or_string_ne_list(xlate_search_about_item a,
 				       List.map xlate_search_about_item l),
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 69f9b2f410..be5980fe43 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -142,94 +142,95 @@
 \newcommand{\typecstr}{\zeroone{{\tt :} {\term}}}
 
 
-\newcommand{\Fwterm}{\textrm{\textsl{Fwterm}}}
-\newcommand{\Index}{\textrm{\textsl{index}}}
-\newcommand{\abbrev}{\textrm{\textsl{abbreviation}}}
-\newcommand{\atomictac}{\textrm{\textsl{atomic\_tactic}}}
-\newcommand{\bindinglist}{\textrm{\textsl{bindings\_list}}}
-\newcommand{\cast}{\textrm{\textsl{cast}}}
-\newcommand{\cofixpointbodies}{\textrm{\textsl{cofix\_bodies}}}
-\newcommand{\cofixpointbody}{\textrm{\textsl{cofix\_body}}}
-\newcommand{\commandtac}{\textrm{\textsl{tactic\_invocation}}}
-\newcommand{\constructor}{\textrm{\textsl{constructor}}}
-\newcommand{\convtactic}{\textrm{\textsl{conv\_tactic}}}
-\newcommand{\declarationkeyword}{\textrm{\textsl{declaration\_keyword}}}
-\newcommand{\declaration}{\textrm{\textsl{declaration}}}
-\newcommand{\definition}{\textrm{\textsl{definition}}}
-\newcommand{\digit}{\textrm{\textsl{digit}}}
-\newcommand{\exteqn}{\textrm{\textsl{ext\_eqn}}}
-\newcommand{\field}{\textrm{\textsl{field}}}
-\newcommand{\firstletter}{\textrm{\textsl{first\_letter}}}
-\newcommand{\fixpg}{\textrm{\textsl{fix\_pgm}}}
-\newcommand{\fixpointbodies}{\textrm{\textsl{fix\_bodies}}}
-\newcommand{\fixpointbody}{\textrm{\textsl{fix\_body}}}
-\newcommand{\fixpoint}{\textrm{\textsl{fixpoint}}}
-\newcommand{\flag}{\textrm{\textsl{flag}}}
-\newcommand{\form}{\textrm{\textsl{form}}}
-\newcommand{\entry}{\textrm{\textsl{entry}}} 
-\newcommand{\proditem}{\textrm{\textsl{production\_item}}} 
-\newcommand{\taclevel}{\textrm{\textsl{tactic\_level}}}
-\newcommand{\tacargtype}{\textrm{\textsl{tactic\_argument\_type}}} 
-\newcommand{\scope}{\textrm{\textsl{scope}}} 
-\newcommand{\optscope}{\textrm{\textsl{opt\_scope}}} 
-\newcommand{\declnotation}{\textrm{\textsl{decl\_notation}}} 
-\newcommand{\symbolentry}{\textrm{\textsl{symbol}}}
-\newcommand{\modifiers}{\textrm{\textsl{modifiers}}}
-\newcommand{\localdef}{\textrm{\textsl{local\_def}}}
-\newcommand{\localdecls}{\textrm{\textsl{local\_decls}}}
-\newcommand{\ident}{\textrm{\textsl{ident}}}
-\newcommand{\accessident}{\textrm{\textsl{access\_ident}}}
-\newcommand{\possiblybracketedident}{\textrm{\textsl{possibly\_bracketed\_ident}}}
-\newcommand{\inductivebody}{\textrm{\textsl{ind\_body}}}
-\newcommand{\inductive}{\textrm{\textsl{inductive}}}
-\newcommand{\naturalnumber}{\textrm{\textsl{natural}}}
-\newcommand{\integer}{\textrm{\textsl{integer}}}
-\newcommand{\multpattern}{\textrm{\textsl{mult\_pattern}}}
-\newcommand{\mutualcoinductive}{\textrm{\textsl{mutual\_coinductive}}}
-\newcommand{\mutualinductive}{\textrm{\textsl{mutual\_inductive}}}
-\newcommand{\nestedpattern}{\textrm{\textsl{nested\_pattern}}}
-\newcommand{\name}{\textrm{\textsl{name}}}
-\newcommand{\num}{\textrm{\textsl{num}}}
-\newcommand{\pattern}{\textrm{\textsl{pattern}}}
-\newcommand{\orpattern}{\textrm{\textsl{or\_pattern}}}
-\newcommand{\intropattern}{\textrm{\textsl{intro\_pattern}}}
-\newcommand{\disjconjintropattern}{\textrm{\textsl{disj\_conj\_intro\_pattern}}}
-\newcommand{\namingintropattern}{\textrm{\textsl{naming\_intro\_pattern}}}
-\newcommand{\pat}{\textrm{\textsl{pat}}}
-\newcommand{\pgs}{\textrm{\textsl{pgms}}}
-\newcommand{\pg}{\textrm{\textsl{pgm}}}
+\newcommand{\Fwterm}{\nterm{Fwterm}}
+\newcommand{\Index}{\nterm{index}}
+\newcommand{\abbrev}{\nterm{abbreviation}}
+\newcommand{\atomictac}{\nterm{atomic\_tactic}}
+\newcommand{\bindinglist}{\nterm{bindings\_list}}
+\newcommand{\cast}{\nterm{cast}}
+\newcommand{\cofixpointbodies}{\nterm{cofix\_bodies}}
+\newcommand{\cofixpointbody}{\nterm{cofix\_body}}
+\newcommand{\commandtac}{\nterm{tactic\_invocation}}
+\newcommand{\constructor}{\nterm{constructor}}
+\newcommand{\convtactic}{\nterm{conv\_tactic}}
+\newcommand{\declarationkeyword}{\nterm{declaration\_keyword}}
+\newcommand{\declaration}{\nterm{declaration}}
+\newcommand{\definition}{\nterm{definition}}
+\newcommand{\digit}{\nterm{digit}}
+\newcommand{\exteqn}{\nterm{ext\_eqn}}
+\newcommand{\field}{\nterm{field}}
+\newcommand{\firstletter}{\nterm{first\_letter}}
+\newcommand{\fixpg}{\nterm{fix\_pgm}}
+\newcommand{\fixpointbodies}{\nterm{fix\_bodies}}
+\newcommand{\fixpointbody}{\nterm{fix\_body}}
+\newcommand{\fixpoint}{\nterm{fixpoint}}
+\newcommand{\flag}{\nterm{flag}}
+\newcommand{\form}{\nterm{form}}
+\newcommand{\entry}{\nterm{entry}} 
+\newcommand{\proditem}{\nterm{production\_item}} 
+\newcommand{\taclevel}{\nterm{tactic\_level}}
+\newcommand{\tacargtype}{\nterm{tactic\_argument\_type}} 
+\newcommand{\scope}{\nterm{scope}} 
+\newcommand{\delimkey}{\nterm{key}} 
+\newcommand{\optscope}{\nterm{opt\_scope}} 
+\newcommand{\declnotation}{\nterm{decl\_notation}} 
+\newcommand{\symbolentry}{\nterm{symbol}}
+\newcommand{\modifiers}{\nterm{modifiers}}
+\newcommand{\localdef}{\nterm{local\_def}}
+\newcommand{\localdecls}{\nterm{local\_decls}}
+\newcommand{\ident}{\nterm{ident}}
+\newcommand{\accessident}{\nterm{access\_ident}}
+\newcommand{\possiblybracketedident}{\nterm{possibly\_bracketed\_ident}}
+\newcommand{\inductivebody}{\nterm{ind\_body}}
+\newcommand{\inductive}{\nterm{inductive}}
+\newcommand{\naturalnumber}{\nterm{natural}}
+\newcommand{\integer}{\nterm{integer}}
+\newcommand{\multpattern}{\nterm{mult\_pattern}}
+\newcommand{\mutualcoinductive}{\nterm{mutual\_coinductive}}
+\newcommand{\mutualinductive}{\nterm{mutual\_inductive}}
+\newcommand{\nestedpattern}{\nterm{nested\_pattern}}
+\newcommand{\name}{\nterm{name}}
+\newcommand{\num}{\nterm{num}}
+\newcommand{\pattern}{\nterm{pattern}}
+\newcommand{\orpattern}{\nterm{or\_pattern}}
+\newcommand{\intropattern}{\nterm{intro\_pattern}}
+\newcommand{\disjconjintropattern}{\nterm{disj\_conj\_intro\_pattern}}
+\newcommand{\namingintropattern}{\nterm{naming\_intro\_pattern}}
+\newcommand{\pat}{\nterm{pat}}
+\newcommand{\pgs}{\nterm{pgms}}
+\newcommand{\pg}{\nterm{pgm}}
 %BEGIN LATEX
-\newcommand{\proof}{\textrm{\textsl{proof}}}
+\newcommand{\proof}{\nterm{proof}}
 %END LATEX
-%HEVEA \renewcommand{\proof}{\textrm{\textsl{proof}}}
-\newcommand{\record}{\textrm{\textsl{record}}}
-\newcommand{\rewrule}{\textrm{\textsl{rewriting\_rule}}}
-\newcommand{\sentence}{\textrm{\textsl{sentence}}}
-\newcommand{\simplepattern}{\textrm{\textsl{simple\_pattern}}}
-\newcommand{\sort}{\textrm{\textsl{sort}}}
-\newcommand{\specif}{\textrm{\textsl{specif}}}
-\newcommand{\statement}{\textrm{\textsl{statement}}}
-\newcommand{\str}{\textrm{\textsl{string}}}
-\newcommand{\subsequentletter}{\textrm{\textsl{subsequent\_letter}}}
-\newcommand{\switch}{\textrm{\textsl{switch}}}
-\newcommand{\messagetoken}{\textrm{\textsl{message\_token}}}
-\newcommand{\tac}{\textrm{\textsl{tactic}}}
-\newcommand{\terms}{\textrm{\textsl{terms}}}
-\newcommand{\term}{\textrm{\textsl{term}}}
-\newcommand{\module}{\textrm{\textsl{module}}}
-\newcommand{\modexpr}{\textrm{\textsl{module\_expression}}}
-\newcommand{\modtype}{\textrm{\textsl{module\_type}}}
-\newcommand{\onemodbinding}{\textrm{\textsl{module\_binding}}}
-\newcommand{\modbindings}{\textrm{\textsl{module\_bindings}}}
-\newcommand{\qualid}{\textrm{\textsl{qualid}}}
-\newcommand{\qualidorstring}{\textrm{\textsl{qualid\_or\_string}}}
-\newcommand{\class}{\textrm{\textsl{class}}}
-\newcommand{\dirpath}{\textrm{\textsl{dirpath}}}
-\newcommand{\typedidents}{\textrm{\textsl{typed\_idents}}}
-\newcommand{\type}{\textrm{\textsl{type}}}
-\newcommand{\vref}{\textrm{\textsl{ref}}}
-\newcommand{\zarithformula}{\textrm{\textsl{zarith\_formula}}}
-\newcommand{\zarith}{\textrm{\textsl{zarith}}}
+%HEVEA \renewcommand{\proof}{\nterm{proof}}
+\newcommand{\record}{\nterm{record}}
+\newcommand{\rewrule}{\nterm{rewriting\_rule}}
+\newcommand{\sentence}{\nterm{sentence}}
+\newcommand{\simplepattern}{\nterm{simple\_pattern}}
+\newcommand{\sort}{\nterm{sort}}
+\newcommand{\specif}{\nterm{specif}}
+\newcommand{\statement}{\nterm{statement}}
+\newcommand{\str}{\nterm{string}}
+\newcommand{\subsequentletter}{\nterm{subsequent\_letter}}
+\newcommand{\switch}{\nterm{switch}}
+\newcommand{\messagetoken}{\nterm{message\_token}}
+\newcommand{\tac}{\nterm{tactic}}
+\newcommand{\terms}{\nterm{terms}}
+\newcommand{\term}{\nterm{term}}
+\newcommand{\module}{\nterm{module}}
+\newcommand{\modexpr}{\nterm{module\_expression}}
+\newcommand{\modtype}{\nterm{module\_type}}
+\newcommand{\onemodbinding}{\nterm{module\_binding}}
+\newcommand{\modbindings}{\nterm{module\_bindings}}
+\newcommand{\qualid}{\nterm{qualid}}
+\newcommand{\qualidorstring}{\nterm{qualid\_or\_string}}
+\newcommand{\class}{\nterm{class}}
+\newcommand{\dirpath}{\nterm{dirpath}}
+\newcommand{\typedidents}{\nterm{typed\_idents}}
+\newcommand{\type}{\nterm{type}}
+\newcommand{\vref}{\nterm{ref}}
+\newcommand{\zarithformula}{\nterm{zarith\_formula}}
+\newcommand{\zarith}{\nterm{zarith}}
 \newcommand{\ltac}{\mbox{${\cal L}_{tac}$}}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index ec07dc079c..7c6bf7297c 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -135,14 +135,34 @@ environment}\\
 \end{ErrMsgs}
 
 \begin{Variants}
-\item {\tt SearchAbout [ \nelist{\textrm{\textsl{qualid-or-string}}}{}
+\item {\tt SearchAbout {\str}.}
+
+If {\str} is a valid identifier, this command displays the name and type
+of all objects (theorems, axioms, etc) of the current context whose
+name contains {\str}. If {\str} is a notation's string denoting some
+reference {\qualid} (referred to by its main symbol as in \verb="+"=
+or by its notation's string as in \verb="_ + _"= or \verb="_ 'U' _"=, see
+Section~\ref{Notation}), the command works like {\tt SearchAbout
+{\qualid}}.
+
+\item {\tt SearchAbout {\str}\%{\delimkey}.}
+
+The string {\str} must be a notation or the main symbol of a notation
+which is then interpreted in the scope bound to the delimiting key
+{\delimkey} (see Section~\ref{scopechange}).
+
+\item {\tt SearchAbout [ \nelist{\zeroone{-}\textrm{\textsl{qualid-or-string}}}{}
 ].}\\
 \noindent where {\textrm{\textsl{qualid-or-string}}} is a {\qualid} or
-a {\str}.
-
-This extension of {\tt SearchAbout} searches for all objects whose
-statement mentions all of {\qualid} of the list and whose name
-contains all {\str} of the list.
+a {\str}, or a {\str} followed by a scope delimiting key 
+{\tt \%{\delimkey}}.
+
+This generalization of {\tt SearchAbout} searches for all objects
+whose statement mentions all of {\qualid} (or {\str} if {\str} is the
+notation for a reference) and whose name contains all {\str} that
+correspond to valid identifiers. If a {\qualid} or a {\str} is
+prefixed by ``-'', the search excludes the objects that mention that
+{\qualid} or that {\str}.
 
 \Example
 
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 22eb0eeaec..967a8180ad 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -713,13 +713,13 @@ ways to change the interpretation of subterms are available.
 \comindex{Delimit Scope}}
 
 It is possible to locally extend the interpretation scope stack using
-the syntax ({\term})\%{\nterm{key}} (or simply {\term}\%{\nterm{key}}
-for atomic terms), where {\nterm{key}} is a special identifier called
+the syntax ({\term})\%{\delimkey} (or simply {\term}\%{\delimkey}
+for atomic terms), where {\delimkey} is a special identifier called
 {\em delimiting key} and bound to a given scope.
 
 In such a situation, the term {\term}, and all its subterms, are
 interpreted in the scope stack extended with the scope bound to
-{\nterm{key}}.
+{\delimkey}.
 
 To bind a delimiting key to a scope, use the command
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index bb845beb17..ca06e1d782 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1317,6 +1317,13 @@ with its $\beta\iota$-normal form.
   this notation refers to an unfoldable constant, then the tactic
   unfolds it.
 
+\item {\tt unfold {\qstring}\%{\delimkey}}
+
+  This is variant of {\tt unfold {\qstring}} where {\qstring} gets its
+  interpretation from the scope bound to the delimiting key
+  {\delimkey} instead of its default interpretation (see
+  Section~\ref{scopechange}).
+
 \item {\tt unfold \qualidorstring$_1$ at \num$_1^1$, \dots, \num$_i^1$,
 \dots,\ \qualidorstring$_n$ at \num$_1^n$ \dots\ \num$_j^n$}
 
diff --git a/interp/genarg.ml b/interp/genarg.ml
index e962880978..d1eda47b78 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -45,7 +45,9 @@ type argument_type =
   | ExtraArgType of string
 
 type 'a and_short_name = 'a * identifier located option
-type 'a or_by_notation = AN of 'a | ByNotation of loc * string
+type 'a or_by_notation =
+  | AN of 'a
+  | ByNotation of loc * string * Notation.delimiters option
 
 type rawconstr_and_expr = rawconstr * constr_expr option
 type open_constr_expr = unit * constr_expr
diff --git a/interp/genarg.mli b/interp/genarg.mli
index bbdc7f7f0a..0ced1e5bea 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -19,7 +19,9 @@ open Evd
 
 type 'a and_short_name = 'a * identifier located option
 
-type 'a or_by_notation = AN of 'a | ByNotation of loc * string
+type 'a or_by_notation =
+  | AN of 'a
+  | ByNotation of loc * string * Notation.delimiters option
 
 (* In globalize tactics, we need to keep the initial [constr_expr] to recompute*)
 (* in the environment by the effective calls to Intro, Inversion, etc *)
diff --git a/interp/notation.ml b/interp/notation.ml
index 46089245c1..0915304c39 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -408,7 +408,7 @@ let exists_notation_in_scope scopt ntn r =
     r' = r
   with Not_found -> false
 
-let isAVar = function AVar _ -> true | _ -> false
+let isAVar_or_AHole = function AVar _ | AHole _ -> true | _ -> false
 
 (**********************************************************************)
 (* Mapping classes to scopes *)
@@ -620,7 +620,7 @@ let browse_notation strict ntn map =
 let global_reference_of_notation test (ntn,(sc,c,_)) =
   match c with
   | ARef ref when test ref -> Some (ntn,sc,ref)
-  | AApp (ARef ref, l) when List.for_all isAVar l & test ref -> 
+  | AApp (ARef ref, l) when List.for_all isAVar_or_AHole l & test ref -> 
       Some (ntn,sc,ref)
   | _ -> None
 
@@ -632,8 +632,12 @@ let error_notation_not_reference loc ntn =
     str "Unable to interpret " ++ quote (str ntn) ++
     str " as a reference.")
 
-let interp_notation_as_global_reference loc test ntn =
-  let ntns = browse_notation true ntn !scope_map in
+let interp_notation_as_global_reference loc test ntn sc =
+  let scopes = match sc with
+  | Some sc ->
+      Gmap.add sc (find_scope (find_delimiters_scope dummy_loc sc)) Gmap.empty
+  | None -> !scope_map in
+  let ntns = browse_notation true ntn scopes in
   let refs = List.map (global_reference_of_notation test) ntns in
   match Option.List.flatten refs with
   | [_,_,ref] -> ref
diff --git a/interp/notation.mli b/interp/notation.mli
index 8bdd8b5863..35d1c0d17b 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -131,7 +131,7 @@ val level_of_notation : notation -> level (* raise [Not_found] if no level *)
 (*s** Miscellaneous *)
 
 val interp_notation_as_global_reference : loc -> (global_reference -> bool) -> 
-      notation -> global_reference
+      notation -> delimiters option -> global_reference
 
 (* Checks for already existing notations *)
 val exists_notation_in_scope : scope_name option -> notation ->
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index ed8422b109..e62fb70768 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -215,7 +215,8 @@ GEXTEND Gram
   ;
   smart_global:
     [ [ c = global -> AN c
-      | s = ne_string -> ByNotation (loc,s) ] ]
+      | s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> 
+	  ByNotation (loc,s,sc) ] ]
   ;
   occs_nums:
     [ [ nl = LIST1 nat_or_var -> no_occurrences_expr_but nl
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index c9fc4e2ffb..76ec0c0901 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -616,9 +616,14 @@ GEXTEND Gram
       | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules ->
 	  VernacSearch (SearchRewrite c, l)
       | IDENT "SearchAbout"; 
-	  sl = [ "["; l = LIST1 [ r = global -> SearchRef r
-                                | s = ne_string -> SearchString s ]; "]" -> l 
-   		 | qid = global -> [SearchRef qid] ];
+	  sl = [ "[";
+	         l = LIST1 [ 
+		   b = positive_search_mark; r = global -> b,SearchRef r
+		 | b = positive_search_mark; s = ne_string; sc = OPT scope
+		   -> b,SearchString (s,sc)
+		 ]; "]" -> l
+   	       | qid = global -> [true,SearchRef qid]
+   	       | s = ne_string; sc = OPT scope -> [true,SearchString (s,sc)] ];
 	  l = in_or_out_modules -> 
 	  VernacSearch (SearchAbout sl, l)
 
@@ -744,6 +749,12 @@ GEXTEND Gram
       | s = STRING -> CommentString s
       | n = natural -> CommentInt n ] ]
   ;
+  positive_search_mark:
+    [ [ "-" -> false | -> true ] ]
+  ;
+  scope:
+    [ [ "%"; key = IDENT -> key ] ]
+  ;
 END;
 
 GEXTEND Gram
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 0eaac6a635..d2ba5ffbc6 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -79,7 +79,7 @@ let pr_and_short_name pr (c,_) = pr c
 
 let pr_or_by_notation f = function
   | AN v -> f v
-  | ByNotation (_,s) -> str s
+  | ByNotation (_,s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
 
 let pr_located pr (loc,x) = pr x
 
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 3a9de47d80..6cfd277a0e 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -133,9 +133,11 @@ let pr_in_out_modules = function
   | SearchOutside [] -> mt()
   | SearchOutside l -> spc() ++ str"outside" ++ spc() ++ prlist_with_sep sep pr_module l
 
-let pr_search_about = function
+let pr_search_about (b,c) = 
+  (if b then str "-" else mt()) ++
+  match c with
   | SearchRef r -> pr_reference r
-  | SearchString s -> qs s
+  | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
 
 let pr_search a b pr_p = match a with
   | SearchHead qid -> str"Search" ++ spc() ++ pr_reference qid ++ pr_in_out_modules b
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 113e88cd35..31054c7f52 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -68,7 +68,8 @@ let mlexpr_of_loc loc = <:expr< $dloc$ >>
 
 let mlexpr_of_by_notation f = function
   | Genarg.AN x -> <:expr< Genarg.AN $f x$ >>
-  | Genarg.ByNotation (loc,s) -> <:expr< Genarg.ByNotation $dloc$ $str:s$ >>
+  | Genarg.ByNotation (loc,s,sco) -> 
+      <:expr< Genarg.ByNotation $dloc$ $str:s$ $mlexpr_of_option mlexpr_of_string sco$ >>
 
 let mlexpr_of_intro_pattern = function
   | Genarg.IntroWildcard -> <:expr< Genarg.IntroWildcard >>
diff --git a/parsing/search.ml b/parsing/search.ml
index 9670c2b878..49682ee48d 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -214,7 +214,7 @@ let search_about_item (itemref,typ) = function
 let raw_search_about filter_modules display_function l =
   let filter ref' env typ =
     filter_modules ref' env typ &&
-    List.for_all (search_about_item (ref',typ)) l && 
+    List.for_all (fun (b,i) -> b = search_about_item (ref',typ) i) l && 
     not (string_string_contains (name_of_reference ref') "_subproof")
   in
   gen_filtered_search filter display_function
diff --git a/parsing/search.mli b/parsing/search.mli
index b639524698..356c5b4691 100644
--- a/parsing/search.mli
+++ b/parsing/search.mli
@@ -25,7 +25,8 @@ type glob_search_about_item =
 val search_by_head : global_reference -> dir_path list * bool -> unit
 val search_rewrite : constr_pattern -> dir_path list * bool -> unit
 val search_pattern : constr_pattern -> dir_path list * bool -> unit
-val search_about  : glob_search_about_item list -> dir_path list * bool -> unit
+val search_about : 
+  (bool * glob_search_about_item) list -> dir_path list * bool -> unit
 
 (* The filtering function that is by standard search facilities.
    It can be passed as argument to the raw search functions.
@@ -46,4 +47,4 @@ val raw_search_rewrite : (global_reference -> env -> constr -> bool) ->
   (global_reference -> env -> constr -> unit) -> constr_pattern -> unit
 val raw_search_about : (global_reference -> env -> constr -> bool) ->
   (global_reference -> env -> constr -> unit) -> 
-      glob_search_about_item list -> unit
+      (bool * glob_search_about_item) list -> unit
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 9c3ffd292a..c40d402086 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -372,15 +372,15 @@ let intern_or_var ist = function
 
 let loc_of_by_notation f = function
   | AN c -> f c
-  | ByNotation (loc,s) -> loc
+  | ByNotation (loc,s,_) -> loc
 
 let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef"
 
 let intern_inductive_or_by_notation = function
   | AN r -> Nametab.inductive_of_reference r
-  | ByNotation (loc,ntn) ->
+  | ByNotation (loc,ntn,sc) ->
       destIndRef (Notation.interp_notation_as_global_reference loc
-        (function IndRef ind -> true | _ -> false) ntn)
+        (function IndRef ind -> true | _ -> false) ntn sc)
 
 let intern_inductive ist = function
   | AN (Ident (loc,id)) when find_var id ist -> ArgVar (loc,id)
@@ -562,10 +562,10 @@ let interp_global_reference r =
 
 let intern_evaluable_reference_or_by_notation = function
   | AN r -> evaluable_of_global_reference (interp_global_reference r)
-  | ByNotation (loc,ntn) ->
+  | ByNotation (loc,ntn,sc) ->
       evaluable_of_global_reference
       (Notation.interp_notation_as_global_reference loc
-        (function ConstRef _ | VarRef _ -> true | _ -> false) ntn)
+        (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
 
 (* Globalizes a reduction expression *)
 let intern_evaluable ist = function
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8c0e7e05a2..d1c972e2b9 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1107,9 +1107,20 @@ let interp_search_restriction = function
 
 open Search
 
+let is_ident s = try ignore (check_ident s); true with UserError _ -> false
+
 let interp_search_about_item = function
   | SearchRef r -> GlobSearchRef (global_with_alias r)
-  | SearchString s -> GlobSearchString s
+  | SearchString (s,None) when is_ident s -> GlobSearchString s
+  | SearchString (s,sc) ->
+      try 
+	let ref =
+	  Notation.interp_notation_as_global_reference dummy_loc
+	    (fun _ -> true) s sc in
+	GlobSearchRef ref
+      with UserError _ -> 
+	error ("Unable to interp \""^s^"\" either as a reference or
+          	as an identifier component")
 
 let vernac_search s r =
   let r = interp_search_restriction r in
@@ -1124,7 +1135,7 @@ let vernac_search s r =
   | SearchHead ref ->
       Search.search_by_head (global_with_alias ref) r
   | SearchAbout sl ->
-      Search.search_about (List.map interp_search_about_item sl) r
+      Search.search_about (List.map (on_snd interp_search_about_item) sl) r
 
 let vernac_locate = function
   | LocateTerm qid -> msgnl (print_located_qualid qid)
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 86b052d47b..19b913708f 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -70,13 +70,13 @@ type printable =
 
 type search_about_item =
   | SearchRef of reference
-  | SearchString of string
+  | SearchString of string * scope_name option
 
 type searchable =
   | SearchPattern of pattern_expr
   | SearchRewrite of pattern_expr
   | SearchHead of reference
-  | SearchAbout of search_about_item list
+  | SearchAbout of (bool * search_about_item) list
 
 type locatable =
   | LocateTerm of reference