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.

---
 kernel/cooking.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/cooking.ml')

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 0951b07d49..087453c31c 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -239,7 +239,7 @@ let cook_constant { from = cb; info } =
   | Undef _ as x -> x
   | Def cs -> Def (Mod_subst.from_val (map (Mod_subst.force_constr cs)))
   | OpaqueDef o ->
-    OpaqueDef (Opaqueproof.discharge_direct_opaque info o)
+    OpaqueDef (Opaqueproof.discharge_opaque info o)
   | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked")
   in
   let const_hyps =
-- 
cgit v1.2.3