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.

---
 pretyping/cbv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/cbv.ml')

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index c9f18d89be..5ea9b79336 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -145,7 +145,7 @@ let mkSTACK = function
 
 type cbv_infos = {
   env : Environ.env;
-  tab : cbv_value Declarations.constant_def KeyTable.t;
+  tab : (cbv_value, Empty.t) Declarations.constant_def KeyTable.t;
   reds : RedFlags.reds;
   sigma : Evd.evar_map
 }
-- 
cgit v1.2.3