From 61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Wed, 13 Jun 2018 00:22:57 +0200
Subject: Remove reference name type.

reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.

We remove the reference type and replace its uses by qualid.
---
 tactics/hints.ml  | 16 ++++++++--------
 tactics/hints.mli | 18 +++++++++---------
 2 files changed, 17 insertions(+), 17 deletions(-)

(limited to 'tactics')

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
-- 
cgit v1.2.3