diff options
| author | Pierre-Marie Pédrot | 2019-05-21 19:22:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-24 09:00:10 +0200 |
| commit | d3c931cd8c84d1b7d9d5763e20221d51700f0709 (patch) | |
| tree | 58ca99c4f6007bc66294c41354bb68bf9d71044b /vernac | |
| parent | 2fa3dc389a58ca4a390b99995d82e6c089add163 (diff) | |
Remove the indirect opaque accessor hooks from Opaqueproof.
We simply pass them as arguments, now that they are not called by the
kernel anymore.
The checker definitely needs to access the opaque proofs. In order not to
touch the API at all, I added a hook there, but it could also be provided
as an additional argument, at the cost of changing all the upwards callers.
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 |