Merge PR #7797: Remove reference name type.

2 files changed, 17 insertions, 17 deletions

diff --git a/tactics/hints.ml b/tactics/hints.ml
index d49c8aaa5..85ff02824 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -125,7 +125,7 @@ type 'a hints_path_gen =
   | PathEmpty
   | PathEpsilon
 
-type pre_hints_path = Libnames.reference hints_path_gen
+type pre_hints_path = Libnames.qualid hints_path_gen
 type hints_path = GlobRef.t hints_path_gen
 
 type hint_term =
@@ -157,7 +157,7 @@ type hint_entry = GlobRef.t option *
   raw_hint hint_ast with_uid with_metadata
 
 type reference_or_constr =
-  | HintsReference of reference
+  | HintsReference of qualid
   | HintsConstr of Constrexpr.constr_expr
 
 type hint_mode =
@@ -167,12 +167,12 @@ type hint_mode =
 
 type hints_expr =
   | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
-  | HintsResolveIFF of bool * reference list * int option
+  | HintsResolveIFF of bool * qualid list * int option
   | HintsImmediate of reference_or_constr list
-  | HintsUnfold of reference list
-  | HintsTransparency of reference list * bool
-  | HintsMode of reference * hint_mode list
-  | HintsConstructors of reference list
+  | HintsUnfold of qualid list
+  | HintsTransparency of qualid list * bool
+  | HintsMode of qualid * hint_mode list
+  | HintsConstructors of qualid list
   | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
 
 type import_level = [ `LAX | `WARN | `STRICT ]
@@ -1360,7 +1360,7 @@ let interp_hints poly =
       let constr_hints_of_ind qid =
         let ind = global_inductive_with_alias qid in
 	let mib,_ = Global.lookup_inductive ind in
-        Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_reference qid) "ind";
+        Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_qualid qid) "ind";
           List.init (nconstructors ind) 
 	    (fun i -> let c = (ind,i+1) in
 		      let gr = ConstructRef c in
diff --git a/tactics/hints.mli b/tactics/hints.mli
index e958f986e..ca18f835a 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -73,7 +73,7 @@ type search_entry
 type hint_entry
 
 type reference_or_constr =
-  | HintsReference of Libnames.reference
+  | HintsReference of Libnames.qualid
   | HintsConstr of Constrexpr.constr_expr
 
 type hint_mode =
@@ -83,12 +83,12 @@ type hint_mode =
 
 type hints_expr =
   | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
-  | HintsResolveIFF of bool * Libnames.reference list * int option
+  | HintsResolveIFF of bool * Libnames.qualid list * int option
   | HintsImmediate of reference_or_constr list
-  | HintsUnfold of Libnames.reference list
-  | HintsTransparency of Libnames.reference list * bool
-  | HintsMode of Libnames.reference * hint_mode list
-  | HintsConstructors of Libnames.reference list
+  | HintsUnfold of Libnames.qualid list
+  | HintsTransparency of Libnames.qualid list * bool
+  | HintsMode of Libnames.qualid * hint_mode list
+  | HintsConstructors of Libnames.qualid list
   | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
 
 type 'a hints_path_gen =
@@ -99,7 +99,7 @@ type 'a hints_path_gen =
   | PathEmpty
   | PathEpsilon
 
-type pre_hints_path = Libnames.reference hints_path_gen
+type pre_hints_path = Libnames.qualid hints_path_gen
 type hints_path = GlobRef.t hints_path_gen
     
 val normalize_path : hints_path -> hints_path
@@ -110,9 +110,9 @@ val pp_hints_path_atom : ('a -> Pp.t) -> 'a hints_path_atom_gen -> Pp.t
 val pp_hints_path : hints_path -> Pp.t
 val pp_hint_mode : hint_mode -> Pp.t
 val glob_hints_path_atom :
-  Libnames.reference hints_path_atom_gen -> GlobRef.t hints_path_atom_gen
+  Libnames.qualid hints_path_atom_gen -> GlobRef.t hints_path_atom_gen
 val glob_hints_path :
-  Libnames.reference hints_path_gen -> GlobRef.t hints_path_gen
+  Libnames.qualid hints_path_gen -> GlobRef.t hints_path_gen
 
 module Hint_db :
   sig