diff options
| author | Pierre-Marie Pédrot | 2019-09-26 17:02:26 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-04 18:00:26 +0200 |
| commit | 69551b566a1339543967a41ff4aaa4580e7394fc (patch) | |
| tree | 4b60e8a6bb3c25c029e43fd40fd56e5839db6e68 /stm | |
| parent | d5f2e13e51c3404d326f04513a50d264790a7a4c (diff) | |
Merge Direct and Indirect nodes in Opaqueproof.
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 1042061021..054c7244fd 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 = |