smartlocate: look for the head symbol for real

This bug was hacked around in ssreflect, but with the new idea
that parsing and interpretation are done in distinct phases the
work around could not be implemented anymore.

2 files changed, 23 insertions, 9 deletions

diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index c5a28ab2d..7ad5561e3 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -20,6 +20,18 @@ open Misctypes
 open Syntax_def
 open Notation_term
 
+let global_of_extended_global_head = function
+  | TrueGlobal ref -> ref
+  | SynDef kn ->
+      let _, syn_def = search_syntactic_definition kn in
+      let rec head_of = function
+        | NRef ref -> ref
+        | NApp (rc, _) -> head_of rc
+        | NCast (rc, _) -> head_of rc
+        | NLetIn (_, _, rc) -> head_of rc
+        | _ -> raise Not_found in
+      head_of syn_def
+
 let global_of_extended_global = function
   | TrueGlobal ref -> ref
   | SynDef kn ->
@@ -28,9 +40,11 @@ let global_of_extended_global = function
   | [],NApp (NRef ref,[]) -> ref
   | _ -> raise Not_found
 
-let locate_global_with_alias (loc,qid) =
+let locate_global_with_alias ?(head=false) (loc,qid) =
   let ref = Nametab.locate_extended qid in
-  try global_of_extended_global ref
+  try
+    if head then global_of_extended_global_head ref
+    else global_of_extended_global ref
   with Not_found ->
     user_err_loc (loc,"",pr_qualid qid ++
       str " is bound to a notation that does not denote a reference.")
@@ -44,14 +58,14 @@ let global_inductive_with_alias r =
         pr_reference r ++ spc () ++ str "is not an inductive type.")
   with Not_found -> Nametab.error_global_not_found_loc loc qid
 
-let global_with_alias r =
+let global_with_alias ?head r =
   let (loc,qid as lqid) = qualid_of_reference r in
-  try locate_global_with_alias lqid
+  try locate_global_with_alias ?head lqid
   with Not_found -> Nametab.error_global_not_found_loc loc qid
 
-let smart_global = function
+let smart_global ?head = function
   | AN r ->
-      global_with_alias r
+      global_with_alias ?head r
   | ByNotation (loc,ntn,sc) ->
       Notation.interp_notation_as_global_reference loc (fun _ -> true) ntn sc
 
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 86aa69681..9006e3687 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -17,7 +17,7 @@ open Misctypes
    if not bound in the global env; raise a [UserError] if bound to a
    syntactic def that does not denote a reference *)
 
-val locate_global_with_alias : qualid located -> global_reference
+val locate_global_with_alias : ?head:bool -> qualid located -> global_reference
 
 (** Extract a global_reference from a reference that can be an "alias" *)
 val global_of_extended_global : extended_global_reference -> global_reference
@@ -26,13 +26,13 @@ val global_of_extended_global : extended_global_reference -> global_reference
     May raise [Nametab.GlobalizationError _] for an unknown reference,
     or a [UserError] if bound to a syntactic def that does not denote
     a reference. *)
-val global_with_alias : reference -> global_reference
+val global_with_alias : ?head:bool -> reference -> global_reference
 
 (** The same for inductive types *)
 val global_inductive_with_alias : reference -> inductive
 
 (** Locate a reference taking into account notations and "aliases" *)
-val smart_global : reference or_by_notation -> global_reference
+val smart_global : ?head:bool -> reference or_by_notation -> global_reference
 
 (** The same for inductive types *)
 val smart_global_inductive : reference or_by_notation -> inductive