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.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel/opaqueproof.ml')

diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 18c1bcc0f8..d168f3cb7e 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -115,6 +115,10 @@ let force_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function
         | None -> Univ.ContextSet.empty
         | Some u -> Future.force u
 
+let get_direct_constraints = function
+| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
+| Direct (_, cu) -> Future.chain cu snd
+
 let get_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (_,cu) -> Some(Future.chain cu snd)
   | Indirect (_,dp,i) ->
-- 
cgit v1.2.3