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

(limited to 'kernel/cClosure.mli')

diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index b1b69dded8..1a790eaed6 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -215,7 +215,7 @@ val eta_expand_ind_stack : env -> inductive -> fconstr -> stack ->
 (** Conversion auxiliary functions to do step by step normalisation *)
 
 (** [unfold_reference] unfolds references in a [fconstr] *)
-val unfold_reference : clos_infos -> clos_tab -> table_key -> fconstr constant_def
+val unfold_reference : clos_infos -> clos_tab -> table_key -> (fconstr, Util.Empty.t) constant_def
 
 (***********************************************************************
   i This is for lazy debug *)
-- 
cgit v1.2.3