From 27468ae02bbbf018743d53a9db49efa34b6d6a3e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 16 May 2019 00:02:54 +0200
Subject: Ensure statically that declarations built by Term_typing are direct.

This removes a lot of cruft breaking the opaque proof abstraction in
Safe_typing and similar.
---
 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 57059300b8..423a416ca4 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -100,6 +100,10 @@ let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function
         let fp = snd (Int.Map.find i prfs) in
         join except fp
 
+let force_direct = function
+| Direct (_, cu) -> Future.force cu
+| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
+
 let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (_,cu) ->
       fst(Future.force cu)
-- 
cgit v1.2.3