diff options
Diffstat (limited to 'checker/mod_checking.ml')
| -rw-r--r-- | checker/mod_checking.ml | 17 |
1 files changed, 11 insertions, 6 deletions
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 = |