Merge PR #12862: [coqchk] Look inside inner modules as well

Reviewed-by: ppedrot
Reviewed-by: proux01

4 files changed, 41 insertions, 7 deletions

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 999f44bf1d..a881b7804f 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -100,26 +100,27 @@ let mk_mtb mp sign delta =
     mod_delta = delta;
     mod_retroknowledge = ModTypeRK; }
 
-let collect_constants_without_body sign mp =
+let rec collect_constants_without_body sign mp accu =
   let collect_sf s lab = function
   | SFBconst cb ->
      let c = Constant.make2 mp lab in
      if Declareops.constant_has_body cb then s else Cset.add c s
-  | SFBmind _ | SFBmodule _ | SFBmodtype _ -> s in
+  | SFBmodule msb -> collect_constants_without_body msb.mod_type (MPdot(mp,lab)) s
+  | SFBmind _ | SFBmodtype _ -> s in
   match sign with
   | MoreFunctor _ -> Cset.empty  (* currently ignored *)
   | NoFunctor struc ->
-     List.fold_left (fun s (lab,mb) -> collect_sf s lab mb) Cset.empty struc
+     List.fold_left (fun s (lab,mb) -> collect_sf s lab mb) accu struc
 
-let rec check_module env opac mp mb =
+let rec check_module env opac mp mb opacify =
   Flags.if_verbose Feedback.msg_notice (str "  checking module: " ++ str (ModPath.to_string mp));
   let env = Modops.add_retroknowledge mb.mod_retroknowledge env in
   let sign, opac =
-    check_signature env opac mb.mod_type mb.mod_mp mb.mod_delta Cset.empty
+    check_signature env opac mb.mod_type mb.mod_mp mb.mod_delta opacify
   in
   let optsign, opac = match mb.mod_expr with
     |Struct sign_struct ->
-      let opacify = collect_constants_without_body sign mb.mod_mp in
+      let opacify = collect_constants_without_body sign mb.mod_mp opacify in
       let sign, opac = check_signature env opac sign_struct mb.mod_mp mb.mod_delta opacify in
       Some (sign, mb.mod_delta), opac
     |Algebraic me -> Some (check_mexpression env opac me mb.mod_mp mb.mod_delta), opac
@@ -152,7 +153,7 @@ and check_structure_field env opac mp lab res opacify = function
       let kn = Mod_subst.mind_of_delta_kn res kn in
       CheckInductive.check_inductive env kn mib, opac
   | SFBmodule msb ->
-      let opac = check_module env opac (MPdot(mp,lab)) msb in
+      let opac = check_module env opac (MPdot(mp,lab)) msb opacify in
       Modops.add_module msb env, opac
   | SFBmodtype mty ->
       check_module_type env mty;
@@ -194,3 +195,5 @@ and check_signature env opac sign mp_mse res opacify = match sign with
         check_structure_field env opac mp_mse lab res opacify mb) (env, opac) struc
       in
       NoFunctor struc, opac
+
+let check_module env opac mp mb = check_module env opac mp mb Cset.empty
diff --git a/doc/changelog/08-tools/12862-more-mod-checking.rst b/doc/changelog/08-tools/12862-more-mod-checking.rst
new file mode 100644
index 0000000000..bb1bf9e789
--- /dev/null
+++ b/doc/changelog/08-tools/12862-more-mod-checking.rst
@@ -0,0 +1,4 @@
+- **Fixed:**
+  ``coqchk`` no longer reports names from inner modules of opaque modules as
+  axioms (`#12862 <https://github.com/coq/coq/pull/12862>`_, fixes `#12845
+  <https://github.com/coq/coq/issues/12845>`_, by Jason Gross).
diff --git a/test-suite/output-coqchk/bug_12845.out b/test-suite/output-coqchk/bug_12845.out
new file mode 100644
index 0000000000..bef45bf2f6
--- /dev/null
+++ b/test-suite/output-coqchk/bug_12845.out
@@ -0,0 +1,14 @@
+
+CONTEXT SUMMARY
+===============
+
+* Theory: Set is predicative
+  
+* Axioms: <none>
+  
+* Constants/Inductives relying on type-in-type: <none>
+  
+* Constants/Inductives relying on unsafe (co)fixpoints: <none>
+  
+* Inductives whose positivity is assumed: <none>
+  
diff --git a/test-suite/output-coqchk/bug_12845.v b/test-suite/output-coqchk/bug_12845.v
new file mode 100644
index 0000000000..d16146855b
--- /dev/null
+++ b/test-suite/output-coqchk/bug_12845.v
@@ -0,0 +1,13 @@
+Module Type A.
+  Module B.
+    Axiom t : Set.
+  End B.
+End A.
+
+Module a : A.
+  Module B.
+    Definition t : Set := unit.
+  End B.
+End a.
+
+Check a.B.t.