From 925778ff0128dfbfe00aafa8a4aa9f3a2eb2301d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 15 May 2019 17:00:57 +0200
Subject: Make the type of constant bodies parametric on opaque proofs.

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

(limited to 'kernel/cooking.mli')

diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index b0f143c47d..d218dd36da 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -18,7 +18,7 @@ type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
 type inline = bool
 
 type result = {
-  cook_body : constr Mod_subst.substituted constant_def;
+  cook_body : (constr Mod_subst.substituted, Opaqueproof.opaque) constant_def;
   cook_type : types;
   cook_universes : universes;
   cook_private_univs : Univ.ContextSet.t option;
-- 
cgit v1.2.3