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/extraction.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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

diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli
index d27c79cb62..bf98f8cd70 100644
--- a/plugins/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
@@ -16,9 +16,9 @@ open Environ
 open Evd
 open Miniml
 
-val extract_constant : env -> Constant.t -> constant_body -> ml_decl
+val extract_constant : env -> Constant.t -> Opaqueproof.opaque constant_body -> ml_decl
 
-val extract_constant_spec : env -> Constant.t -> constant_body -> ml_spec
+val extract_constant_spec : env -> Constant.t -> 'a constant_body -> ml_spec
 
 (** For extracting "module ... with ..." declaration *)
 
-- 
cgit v1.2.3