diff options
| author | Enrico Tassi | 2019-05-24 14:11:17 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-05-24 14:11:17 +0200 |
| commit | 831639deec0ce88fca4ede4756815cf434088ac3 (patch) | |
| tree | e61b8bbaee62d36519eb6845c1a6d89e31ed1bf6 /vernac | |
| parent | 1c2cfc1fc66416dbd72dc5f1c72b608727195b27 (diff) | |
| parent | 069a5e5fa201bb60810dd1b8dc8e1492770a5963 (diff) | |
Merge PR #10201: Remove access to indirect opaques in the kernel
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Reviewed-by: gares
Reviewed-by: maximedenes
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/assumptions.ml | 4 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 445f10ecc1..9353ef3902 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -168,7 +168,7 @@ let rec traverse current ctx accu t = match Constr.kind t with let body () = id |> Global.lookup_named |> NamedDecl.get_value in traverse_object accu body (VarRef id) | Const (kn, _) -> - let body () = Option.map fst (Global.body_of_constant_body (lookup_constant kn)) in + let body () = Option.map fst (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in traverse_object accu body (ConstRef kn) | Ind ((mind, _) as ind, _) -> traverse_inductive accu mind (IndRef ind) @@ -181,7 +181,7 @@ let rec traverse current ctx accu t = match Constr.kind t with | Lambda(_,_,oty), Const (kn, _) when Vars.noccurn 1 oty && not (Declareops.constant_has_body (lookup_constant kn)) -> - let body () = Option.map fst (Global.body_of_constant_body (lookup_constant kn)) in + let body () = Option.map fst (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in traverse_object ~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn) | _ -> diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 317cf487cc..740b9031cc 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -57,7 +57,7 @@ let retrieve_first_recthm uctx = function let uctx = UState.context uctx in let inst = Univ.UContext.instance uctx in let map (c, ctx) = Vars.subst_instance_constr inst c in - (Option.map map (Global.body_of_constant_body cb), is_opaque cb) + (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), is_opaque cb) | _ -> assert false let adjust_guardness_conditions const = function |