From ab14dab1f8a612e3d854df89ae6d21c26ebb2945 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 5 Apr 2020 18:20:36 +0200
Subject: Fixing #3451: coqdoc links for projections of tuples rather than for
 constructor.

Moreover, the link to the constructor was hiding other contents of the
tuple.
---
 interp/constrintern.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4bd0013750..f82783f47d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1432,6 +1432,7 @@ let sort_fields ~complete loc fields completer =
         let (first_field_glob_ref, record) =
           try
             let gr = locate_reference first_field_ref in
+            Dumpglob.add_glob ?loc:first_field_ref.CAst.loc gr;
             (gr, Recordops.find_projection gr)
           with Not_found ->
             raise (InternalizationError(first_field_ref.CAst.loc, NotAProjection first_field_ref))
@@ -1479,6 +1480,7 @@ let sort_fields ~complete loc fields completer =
                     by a let-in in the record declaration
                     (its value is fixed from other fields). *)
                  user_err ?loc  (str "No local fields allowed in a record construction.");
+               Dumpglob.add_glob ?loc:field_ref.CAst.loc field_glob_ref;
                index_fields fields remaining_projs ((field_index, field_value) :: acc)
             | [] ->
                let remaining_fields =
-- 
cgit v1.2.3