Fix bug #5232: proper globalization of hints paths

3 files changed, 80 insertions, 31 deletions

diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4
index 22a2d7fc2..c561ecf60 100644
--- a/ltac/g_auto.ml4
+++ b/ltac/g_auto.ml4
@@ -171,18 +171,32 @@ TACTIC EXTEND convert_concl_no_check
 | ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x Term.DEFAULTcast ]
 END
 
-let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom
+let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_reference
+let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global
+let glob_hints_path_atom ist = Hints.glob_hints_path_atom
 
 ARGUMENT EXTEND hints_path_atom
   PRINTED BY pr_hints_path_atom
-| [ ne_global_list(g) ] -> [ Hints.PathHints (List.map Nametab.global g) ]
+
+  GLOBALIZED BY glob_hints_path_atom
+
+  RAW_PRINTED BY pr_pre_hints_path_atom
+  GLOB_PRINTED BY pr_hints_path_atom
+| [ ne_global_list(g) ] -> [ Hints.PathHints g ]
 | [ "_" ] -> [ Hints.PathAny ]
 END
 
 let pr_hints_path prc prx pry c = Hints.pp_hints_path c
-
+let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_reference c
+let glob_hints_path ist = Hints.glob_hints_path
+							      
 ARGUMENT EXTEND hints_path
-  PRINTED BY pr_hints_path
+PRINTED BY pr_hints_path
+
+GLOBALIZED BY glob_hints_path
+RAW_PRINTED BY pr_pre_hints_path
+GLOB_PRINTED BY pr_hints_path
+
 | [ "(" hints_path(p) ")"  ] -> [ p ]
 | [ hints_path(p) "*" ] -> [ Hints.PathStar p ]
 | [ "emp" ] -> [ Hints.PathEmpty ]
@@ -203,7 +217,7 @@ END
 
 VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF
 | [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [
-  let entry = Hints.HintsCutEntry p in
+  let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in
     Hints.add_hints (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
       (match dbnames with None -> ["core"] | Some l -> l) entry ]
 END
diff --git a/tactics/hints.ml b/tactics/hints.ml
index d91ea8079..9a96b7389 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -100,18 +100,25 @@ type 'a hint_ast =
   | Unfold_nth of evaluable_global_reference       (* Hint Unfold *)
   | Extern     of Genarg.glob_generic_argument (* Hint Extern *)
 
-type hints_path_atom = 
-  | PathHints of global_reference list
+
+type 'a hints_path_atom_gen =
+  | PathHints of 'a list
+  (* For forward hints, their names is the list of projections *)
   | PathAny
 
-type hints_path =
-  | PathAtom of hints_path_atom
-  | PathStar of hints_path
-  | PathSeq of hints_path * hints_path
-  | PathOr of hints_path * hints_path
+type hints_path_atom = global_reference hints_path_atom_gen
+
+type 'a hints_path_gen =
+  | PathAtom of 'a hints_path_atom_gen
+  | PathStar of 'a hints_path_gen
+  | PathSeq of 'a hints_path_gen * 'a hints_path_gen
+  | PathOr of 'a hints_path_gen * 'a hints_path_gen
   | PathEmpty
   | PathEpsilon
 
+type pre_hints_path = Libnames.reference hints_path_gen
+type hints_path = global_reference hints_path_gen
+
 type hint_term =
   | IsGlobRef of global_reference
   | IsConstr of constr * Univ.universe_context_set
@@ -393,21 +400,40 @@ let rec normalize_path h =
 
 let path_derivate hp hint = normalize_path (path_derivate hp hint)
 
-let pp_hints_path_atom a =
+let pp_hints_path_atom prg a =
   match a with
   | PathAny -> str"_"
-  | PathHints grs -> pr_sequence pr_global grs
-					   
-let rec pp_hints_path = function
-  | PathAtom pa -> pp_hints_path_atom pa
-  | PathStar (PathAtom PathAny) -> str"_*"
-  | PathStar p -> str "(" ++ pp_hints_path p ++ str")*"
-  | PathSeq (p, p') -> pp_hints_path p ++ spc () ++ pp_hints_path p'
-  | PathOr (p, p') -> 
-     str "(" ++ pp_hints_path p ++ spc () ++ str"|" ++ cut () ++ spc () ++
-       pp_hints_path p' ++ str ")"
+  | PathHints grs -> pr_sequence prg grs
+
+let pp_hints_path_gen prg =
+  let rec aux = function
+    | PathAtom pa -> pp_hints_path_atom prg pa
+    | PathStar (PathAtom PathAny) -> str"_*"
+    | PathStar p -> str "(" ++ aux p ++ str")*"
+    | PathSeq (p, p') -> aux p ++ spc () ++ aux p'
+    | PathOr (p, p') -> 
+     str "(" ++ aux p ++ spc () ++ str"|" ++ cut () ++ spc () ++
+     aux p' ++ str ")"
   | PathEmpty -> str"emp"
   | PathEpsilon -> str"eps"
+  in aux
+     
+let pp_hints_path = pp_hints_path_gen pr_global
+
+let glob_hints_path_atom p =
+  match p with
+  | PathHints g -> PathHints (List.map Nametab.global g)
+  | PathAny -> PathAny
+
+let glob_hints_path =
+  let rec aux = function
+    | PathAtom pa -> PathAtom (glob_hints_path_atom pa)
+    | PathStar p -> PathStar (aux p)
+    | PathSeq (p, p') -> PathSeq (aux p, aux p')
+    | PathOr (p, p') -> PathOr (aux p, aux p')
+    | PathEmpty -> PathEmpty
+    | PathEpsilon -> PathEpsilon
+  in aux
 
 let subst_path_atom subst p =
   match p with
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 42a2896ed..1be3e0c52 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -42,11 +42,12 @@ type 'a hint_ast =
 type hint
 type raw_hint = constr * types * Univ.universe_context_set
 
-type hints_path_atom = 
-  | PathHints of global_reference list
+type 'a hints_path_atom_gen =
+  | PathHints of 'a list
   (* For forward hints, their names is the list of projections *)
   | PathAny
 
+type hints_path_atom = global_reference hints_path_atom_gen
 type hint_db_name = string
 
 type 'a with_metadata = private {
@@ -67,20 +68,28 @@ type search_entry
 
 type hint_entry
 
-type hints_path =
-  | PathAtom of hints_path_atom
-  | PathStar of hints_path
-  | PathSeq of hints_path * hints_path
-  | PathOr of hints_path * hints_path
+type 'a hints_path_gen =
+  | PathAtom of 'a hints_path_atom_gen
+  | PathStar of 'a hints_path_gen
+  | PathSeq of 'a hints_path_gen * 'a hints_path_gen
+  | PathOr of 'a hints_path_gen * 'a hints_path_gen
   | PathEmpty
   | PathEpsilon
 
+type pre_hints_path = Libnames.reference hints_path_gen
+type hints_path = global_reference hints_path_gen
+    
 val normalize_path : hints_path -> hints_path
 val path_matches : hints_path -> hints_path_atom list -> bool
 val path_derivate : hints_path -> hints_path_atom -> hints_path
-val pp_hints_path_atom : hints_path_atom -> Pp.std_ppcmds
+val pp_hints_path_gen : ('a -> Pp.std_ppcmds) -> 'a hints_path_gen -> Pp.std_ppcmds
+val pp_hints_path_atom : ('a -> Pp.std_ppcmds) -> 'a hints_path_atom_gen -> Pp.std_ppcmds
 val pp_hints_path : hints_path -> Pp.std_ppcmds
 val pp_hint_mode : hint_mode -> Pp.std_ppcmds
+val glob_hints_path_atom :
+  Libnames.reference hints_path_atom_gen -> Globnames.global_reference hints_path_atom_gen
+val glob_hints_path :
+  Libnames.reference hints_path_gen -> Globnames.global_reference hints_path_gen
 
 module Hint_db :
   sig