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 /doc/plugin_tutorial/tuto1/src | |
| 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 'doc/plugin_tutorial/tuto1/src')
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/simple_print.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.ml b/doc/plugin_tutorial/tuto1/src/simple_print.ml index cfc38ff9c9..22a0163fbb 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_print.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_print.ml @@ -11,7 +11,7 @@ let simple_body_access gref = failwith "constructors are not covered in this example" | Globnames.ConstRef cst -> let cb = Environ.lookup_constant cst (Global.env()) in - match Global.body_of_constant_body cb with + match Global.body_of_constant_body Library.indirect_accessor cb with | Some(e, _) -> e | None -> failwith "This term has no value" |