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 /stm | |
| 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 'stm')
| -rw-r--r-- | stm/stm.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 30cf8a0622..660dc27211 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1839,11 +1839,11 @@ end = struct (* {{{ *) | _ -> assert false in (* No need to delay the computation, the future has been forced by the call to [check_task_aux] above. *) - let uc = Opaqueproof.force_constraints (Global.opaque_tables ()) o in + let uc = Opaqueproof.force_constraints Library.indirect_accessor (Global.opaque_tables ()) o in let uc = Univ.hcons_universe_context_set uc in (* We only manipulate monomorphic terms here. *) let map (c, ctx) = assert (Univ.AUContext.is_empty ctx); c in - let pr = map (Option.get (Global.body_of_constant_body c)) in + let pr = map (Option.get (Global.body_of_constant_body Library.indirect_accessor c)) in let pr = discharge pr in let pr = Constr.hcons pr in u.(bucket) <- Some uc; |