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

7 files changed, 27 insertions, 11 deletions

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