From 69551b566a1339543967a41ff4aaa4580e7394fc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 26 Sep 2019 17:02:26 +0200
Subject: Merge Direct and Indirect nodes in Opaqueproof.

---
 stm/stm.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'stm')

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 =
-- 
cgit v1.2.3