diff options
| author | Pierre-Marie Pédrot | 2019-05-31 14:27:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-04 11:16:17 +0200 |
| commit | e7ffa1bfa25300a25c1e81583b77d2d7587bbb5d (patch) | |
| tree | f3b9bc7307d04f2757b3d00504100023bc9f2d9a /stm | |
| parent | 589aaf4f97d5cfcdabfda285739228f5ee52261f (diff) | |
Do not substitute opaque constants when discharging.
Instead we do that on a by-need basis by reusing the section info already
stored in the opaque proof.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index b2bfa552b4..8efb606ddc 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1732,7 +1732,6 @@ end = struct (* {{{ *) | `ERROR_ADMITTED -> cst, false | `OK_ADMITTED -> cst, false | `OK (po,_) -> - let discharge c = List.fold_right Cooking.cook_constr d.(bucket) c in let con = Nametab.locate_constant (Libnames.qualid_of_ident po.Proof_global.id) in @@ -1744,12 +1743,11 @@ end = struct (* {{{ *) the call to [check_task_aux] above. *) let uc = Opaqueproof.force_constraints Library.indirect_accessor (Global.opaque_tables ()) o in let uc = Univ.hcons_universe_context_set uc in + let (pr, ctx) = Option.get (Global.body_of_constant_body Library.indirect_accessor c) 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 Library.indirect_accessor c)) in - let pr = discharge pr in + let () = assert (Univ.AUContext.is_empty ctx) in let pr = Constr.hcons pr in - p.(bucket) <- Some pr; + p.(bucket) <- Some (d.(bucket), Univ.AUContext.size ctx, pr); Univ.ContextSet.union cst uc, false let check_task name l i = |