[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.

1 files changed, 3 insertions, 3 deletions

diff --git a/checker/safe_checking.ml b/checker/safe_checking.ml
index b5beab532e..55bfa36ce5 100644
--- a/checker/safe_checking.ml
+++ b/checker/safe_checking.ml
@@ -11,14 +11,14 @@
 open Declarations
 open Environ
 
-let import senv clib univs digest =
+let import senv opac clib univs digest =
   let mb = Safe_typing.module_of_library clib in
   let env = Safe_typing.env_of_safe_env senv in
   let env = push_context_set ~strict:true (Safe_typing.univs_of_library clib) env in
   let env = push_context_set ~strict:true univs env in
   let env = Modops.add_retroknowledge mb.mod_retroknowledge env in
-  Mod_checking.check_module env mb.mod_mp mb;
-  let (_,senv) = Safe_typing.import clib univs digest senv in senv
+  let opac = Mod_checking.check_module env opac mb.mod_mp mb in
+  let (_,senv) = Safe_typing.import clib univs digest senv in senv, opac
 
 let unsafe_import senv clib univs digest =
   let (_,senv) = Safe_typing.import clib univs digest senv in senv