diff options
| author | Hugo Herbelin | 2020-04-05 18:20:36 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-04-21 19:29:57 +0200 |
| commit | ab14dab1f8a612e3d854df89ae6d21c26ebb2945 (patch) | |
| tree | 24942a0d27ea149f3830c0bef23a78d8c67decf4 /interp | |
| parent | 6908a9da72bc534d53493816d9b552c85d447f49 (diff) | |
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.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 2 |
1 files changed, 2 insertions, 0 deletions
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 = |