From 801aed67a90ec49c15a4469e1905aa2835fabe19 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 15 May 2019 23:50:42 +0200
Subject: Parameterize the constant_body type by opaque subproofs.

---
 plugins/extraction/table.mli | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/extraction/table.mli')

diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index acc1bfee8a..7e53964642 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -72,11 +72,11 @@ val labels_of_ref : GlobRef.t -> ModPath.t * Label.t list
    [mutual_inductive_body] as checksum. In both case, we should ideally
    also check the env *)
 
-val add_typedef : Constant.t -> constant_body -> ml_type -> unit
-val lookup_typedef : Constant.t -> constant_body -> ml_type option
+val add_typedef : Constant.t -> Opaqueproof.opaque constant_body -> ml_type -> unit
+val lookup_typedef : Constant.t -> Opaqueproof.opaque constant_body -> ml_type option
 
-val add_cst_type : Constant.t -> constant_body -> ml_schema -> unit
-val lookup_cst_type : Constant.t -> constant_body -> ml_schema option
+val add_cst_type : Constant.t -> Opaqueproof.opaque constant_body -> ml_schema -> unit
+val lookup_cst_type : Constant.t -> Opaqueproof.opaque constant_body -> ml_schema option
 
 val add_ind : MutInd.t -> mutual_inductive_body -> ml_ind -> unit
 val lookup_ind : MutInd.t -> mutual_inductive_body -> ml_ind option
-- 
cgit v1.2.3