[coqchk] Improve previous heuristic.

Instead of considering all constants without body in the environment,
consider only the ones appearing in the body of the opacified constant.

(cherry picked from commit 5b2e6c3)

checker/mod_checking.ml

@@ -15,15 +15,20 @@ let indirect_accessor = ref {
 
 let set_indirect_accessor f = indirect_accessor := f
 
-let register_opacified_constant env opac kn =
+let register_opacified_constant env opac kn cb =
+  let rec gather_consts s c =
+    match Constr.kind c with
+    | Constr.Const (c, _) -> Cset.add c s
+    | _ -> Constr.fold gather_consts s c
+  in
   let wo_body =
-    fold_constants
-      (fun kn cb s ->
-        if Declareops.constant_has_body cb then s else
+    Cset.fold
+      (fun kn s ->
+        if Declareops.constant_has_body (lookup_constant kn env) then s else
           match Cmap.find_opt kn opac with
           | None -> Cset.add kn s
           | Some s' -> Cset.union s' s)
-      env
+      (gather_consts Cset.empty cb)
       Cset.empty
   in
   Cmap.add kn wo_body opac
@@ -68,7 +73,7 @@ let check_constant_declaration env opac kn cb opacify =
     | None -> ()
   in
   match body with
-  | Some _ when opacify -> register_opacified_constant env opac kn
+  | Some body when opacify -> register_opacified_constant env opac kn body
   | Some _ | None -> opac
 
 let check_constant_declaration env opac kn cb opacify =