From 61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
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 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

(limited to 'plugins/extraction/extract_env.ml')

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 1e0589fac5..4ede11b5c9 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
-- 
cgit v1.2.3