From 5b2e6c3567329ebe8d9a680ef914a84aeae312a1 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Wed, 15 Apr 2020 12:40:21 +0200
Subject: [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.
---
 checker/mod_checking.ml | 17 +++++++++++------
 1 file changed, 11 insertions(+), 6 deletions(-)

(limited to 'checker/mod_checking.ml')

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index c2b486c371..999f44bf1d 100644
--- a/checker/mod_checking.ml
+++ b/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 =
-- 
cgit v1.2.3