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/cbytegen.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/cbytegen.mli')

diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index 6a9550342c..bdaf5fe422 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -20,7 +20,7 @@ val compile : fail_on_error:bool ->
 (** init, fun, fv *)
 
 val compile_constant_body : fail_on_error:bool ->
-  env -> universes -> Constr.t Mod_subst.substituted constant_def ->
+  env -> universes -> (Constr.t Mod_subst.substituted, 'opaque) constant_def ->
   body_code option
 
 (** Shortcut of the previous function used during module strengthening *)
-- 
cgit v1.2.3