From e3a0a4d58b74d2113485ceabe4235567fda962c8 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 10 Oct 2014 17:12:30 +0200
Subject: selective join/export of the safe_environment

This generalizes the BuildVi flag and lets one choose which
opaque proofs are done and which not.
---
 kernel/declareops.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'kernel/declareops.mli')

diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 4978566765..ad3e8be4f4 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -75,8 +75,6 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
 
 val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body
 
-val join_constant_body : Opaqueproof.opaquetab -> constant_body -> unit
-
 (** {6 Hash-consing} *)
 
 (** Here, strictly speaking, we don't perform true hash-consing
-- 
cgit v1.2.3