diff options
| author | Maxime Dénès | 2019-10-12 13:28:35 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-10-12 13:28:35 +0200 |
| commit | cc4cddda2eb2a05f685c8404e4864ea0bcdac6eb (patch) | |
| tree | 134dc9c5bb95fd26789556231f73c69896b5255f /stm | |
| parent | e8d0b5a8856a695dc3f6a28e2d305c095ef50c19 (diff) | |
| parent | 69551b566a1339543967a41ff4aaa4580e7394fc (diff) | |
Merge PR #10818: Merge Direct and Indirect nodes in Opaqueproof.
Reviewed-by: gares
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 b60c9c3dad..5c6df26cbb 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1743,9 +1743,9 @@ end = struct (* {{{ *) assert (Univ.ContextSet.is_empty uctx) in let pr = Constr.hcons pr in - let (ci, dummy) = p.(bucket) in + let dummy = p.(bucket) in let () = assert (Option.is_empty dummy) in - p.(bucket) <- ci, Some (pr, priv); + p.(bucket) <- Some (pr, priv); Univ.ContextSet.union cst uc, false let check_task name l i = |