From 26169d33b45aae8bf2dfafa2b400a9780c73ea13 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 16 May 2019 22:32:48 +0200
Subject: Remove a last use of opacity-piercing function in Safe_typing.

---
 kernel/opaqueproof.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/opaqueproof.mli')

diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 4e8956af06..501779a917 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -39,6 +39,7 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
     indirect opaque accessor configured below. *)
 val force_proof : opaquetab -> opaque -> constr
 val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t
+val get_direct_constraints : opaque -> Univ.ContextSet.t Future.computation
 val get_constraints :
   opaquetab -> opaque -> Univ.ContextSet.t Future.computation option
 
-- 
cgit v1.2.3