From 262ad3c3ce24463094110aa011471213ac0b61c7 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 18 Aug 2016 18:47:55 +0200
Subject: Fix incorrect glob data for module symbols (bug #2336).

The logic was backward: if the path of a symbol was a prefix of the
current path, then the current path (without sections) was used. But what
we want is that, if the current path (without sections) is a prefix of the
path of a symbol, then the former should be used.

This fixes about 1,600 broken links in the documentation of the standard
library.
---
 interp/dumpglob.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 85212b7aba..d70d30d9ec 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -127,9 +127,10 @@ let type_of_global_ref gr =
     | Globnames.ConstructRef _ -> "constr"
 
 let remove_sections dir =
-  if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then
+  let cwd = Lib.cwd_except_section () in
+  if Libnames.is_dirpath_prefix_of cwd dir then
     (* Not yet (fully) discharged *)
-    Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ())
+    cwd
   else
     (* Theorem/Lemma outside its outer section of definition *)
     dir
-- 
cgit v1.2.3


From c85e668255c1a2ef7881a7a106bffebd8f171f28 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 19 Aug 2016 07:05:18 +0200
Subject: Fix anomaly on user-inputted projection name (bug #5029).

---
 interp/constrintern.ml | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7c4688f9fb..30016dedcf 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1078,12 +1078,10 @@ let sort_fields ~complete loc fields completer =
   match fields with
     | [] -> None
     | (first_field_ref, first_field_value):: other_fields ->
-        let env_error_msg = "Environment corruption for records." in
-        let first_field_glob_ref =
-          try global_reference_of_reference first_field_ref
-          with Not_found -> anomaly (Pp.str env_error_msg) in
-        let record =
-          try Recordops.find_projection first_field_glob_ref
+        let (first_field_glob_ref, record) =
+          try
+            let gr = global_reference_of_reference first_field_ref in
+            (gr, Recordops.find_projection gr)
           with Not_found ->
             user_err_loc (loc_of_reference first_field_ref, "intern",
                           pr_reference first_field_ref ++ str": Not a projection")
@@ -1094,7 +1092,8 @@ let sort_fields ~complete loc fields completer =
         let base_constructor =
           let global_record_id = ConstructRef record.Recordops.s_CONST in
           try Qualid (loc, shortest_qualid_of_global Id.Set.empty global_record_id)
-          with Not_found -> anomaly (Pp.str env_error_msg) in
+          with Not_found ->
+            anomaly (str "Environment corruption for records") in
         let (end_index,    (* one past the last field index *)
              first_field_index,  (* index of the first field of the record *)
              proj_list)    (* list of projections *)
-- 
cgit v1.2.3