From f44ec99f9ae9b8aa8d77c39795dd4de2a5724218 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Sat, 11 Apr 2020 14:03:54 +0200
Subject: [coqchk] Fix #5030

When encountering
```Coq
Module M : T.
...
Lemma c :...
...
Qed.
...
End M.
```
every field `c` without body in `T` but with a body in `M` is
registered as opacified in a table along with all constants
`opacified(c)` without body in the environment at this point (i.e.,
all axioms potentially used by c).

Then, when printing axioms, if `c` appears in the final environment it
is replaced by `opacified(c)` in the resulting list of axioms.
---
 checker/check.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'checker/check.ml')

diff --git a/checker/check.ml b/checker/check.ml
index 6d307b3c5e..1ff1425dea 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -119,11 +119,12 @@ let check_one_lib admit senv (dir,m) =
     if LibrarySet.mem dir admit then
       (Flags.if_verbose Feedback.msg_notice
          (str "Admitting library: " ++ pr_dirpath dir);
-       Safe_checking.unsafe_import senv md m.library_extra_univs dig)
+       Safe_checking.unsafe_import (fst senv) md m.library_extra_univs dig),
+      (snd senv)
     else
       (Flags.if_verbose Feedback.msg_notice
          (str "Checking library: " ++ pr_dirpath dir);
-       Safe_checking.import senv md m.library_extra_univs dig)
+       Safe_checking.import (fst senv) (snd senv) md m.library_extra_univs dig)
   in
     register_loaded_library m; senv
 
@@ -435,6 +436,6 @@ let recheck_library senv ~norec ~admit ~check =
   Flags.if_verbose Feedback.msg_notice (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++
     prlist
     (fun (dir,_) -> pr_dirpath dir ++ fnl()) needed));
-  let senv = List.fold_left (check_one_lib nochk) senv needed in
+  let senv = List.fold_left (check_one_lib nochk) (senv, Cmap.empty) needed in
   Flags.if_verbose Feedback.msg_notice (str"Modules were successfully checked");
   senv
-- 
cgit v1.2.3