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

4 files changed, 15 insertions, 7 deletions

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 ->