From b1d749e59444f86e40f897c41739168bb1b1b9b3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 25 Feb 2018 22:43:42 +0100
Subject: [located] Push inner locations in `reference` to a CAst.t node.

The `reference` type contains some ad-hoc locations in its
constructors, but there is no reason not to handle them with the
standard attribute container provided by `CAst.t`.

An orthogonal topic to this commit is whether the `reference` type
should contain a location or not at all.

It seems that many places would become a bit clearer by splitting
`reference` into non-located `reference` and `lreference`, however
some other places become messier so we maintain the current status-quo
for now.
---
 plugins/funind/indfun_common.ml | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

(limited to 'plugins/funind/indfun_common.ml')

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index d6fd2f2a0f..a0b9217c75 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -32,7 +32,7 @@ let id_of_name = function
   | _ -> raise Not_found
 
 let locate  ref =
-    let (loc,qid) = qualid_of_reference ref in
+    let {CAst.v=qid} = qualid_of_reference ref in
     Nametab.locate qid
 
 let locate_ind ref =
@@ -100,13 +100,8 @@ let list_union_eq eq_fun l1 l2 =
 let list_add_set_eq eq_fun x l =
   if List.exists (eq_fun x) l then l else x::l
 
-
-
-
 let const_of_id id =
-  let _,princ_ref =
-    qualid_of_reference (Libnames.Ident (Loc.tag id))
-  in
+  let princ_ref = qualid_of_ident id in
   try Constrintern.locate_reference princ_ref
   with Not_found ->
     CErrors.user_err ~hdr:"IndFun.const_of_id"
-- 
cgit v1.2.3