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.
---
 plugins/extraction/extract_env.ml  | 11 +++++------
 plugins/extraction/extract_env.mli |  8 ++++----
 plugins/extraction/table.mli       |  8 ++++----
 3 files changed, 13 insertions(+), 14 deletions(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 1e0589fac..4ede11b5c 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -596,19 +596,18 @@ let warns () =
 
 let rec locate_ref = function
   | [] -> [],[]
-  | r::l ->
-      let q = qualid_of_reference r in
-      let mpo = try Some (Nametab.locate_module q.CAst.v) with Not_found -> None
+  | qid::l ->
+      let mpo = try Some (Nametab.locate_module qid) with Not_found -> None
       and ro =
-        try Some (Smartlocate.global_with_alias r)
+        try Some (Smartlocate.global_with_alias qid)
         with Nametab.GlobalizationError _ | UserError _ -> None
       in
       match mpo, ro with
-	| None, None -> Nametab.error_global_not_found q
+        | None, None -> Nametab.error_global_not_found qid
 	| None, Some r -> let refs,mps = locate_ref l in r::refs,mps
 	| Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps
 	| Some mp, Some r ->
-           warning_ambiguous_name (q.CAst.v,mp,r);
+           warning_ambiguous_name (qid,mp,r);
            let refs,mps = locate_ref l in refs,mp::mps
 
 (*s Recursive extraction in the Coq toplevel. The vernacular command is
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 77f1fb5ef..54fde2ca4 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -13,14 +13,14 @@
 open Names
 open Libnames
 
-val simple_extraction : reference -> unit
-val full_extraction : string option -> reference list -> unit
-val separate_extraction : reference list -> unit
+val simple_extraction : qualid -> unit
+val full_extraction : string option -> qualid list -> unit
+val separate_extraction : qualid list -> unit
 val extraction_library : bool -> Id.t -> unit
 
 (* For the test-suite : extraction to a temporary file + ocamlc on it *)
 
-val extract_and_compile : reference list -> unit
+val extract_and_compile : qualid list -> unit
 
 (* For debug / external output via coqtop.byte + Drop : *)
 
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 5bf944434..a8baeaf1b 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -194,17 +194,17 @@ val find_custom_match : ml_branch array -> string
 (*s Extraction commands. *)
 
 val extraction_language : lang -> unit
-val extraction_inline : bool -> reference list -> unit
+val extraction_inline : bool -> qualid list -> unit
 val print_extraction_inline : unit -> Pp.t
 val reset_extraction_inline : unit -> unit
 val extract_constant_inline :
-  bool -> reference -> string list -> string -> unit
+  bool -> qualid -> string list -> string -> unit
 val extract_inductive :
-  reference -> string -> string list -> string option -> unit
+  qualid -> string -> string list -> string option -> unit
 
 
 type int_or_id = ArgInt of int | ArgId of Id.t
-val extraction_implicit : reference -> int_or_id list -> unit
+val extraction_implicit : qualid -> int_or_id list -> unit
 
 (*s Table of blacklisted filenames *)
 
-- 
cgit v1.2.3