From acbf569a3b9f242fd704af9124c58697b8762d0d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 26 Sep 2019 15:36:51 +0200
Subject: Move the declararation of delayed constraints out of
 add_constant_aux.

This allows to remove the double declaration of monomorphic universes of
discharged section constants. This also makes it much clearer that only
the first declaration of a constant is allowed to declare delayed
constraints.

As a nice bonus, this simplifies the Opaqueproof API.
---
 kernel/opaqueproof.ml | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'kernel/opaqueproof.ml')

diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index e256466112..f0ffd2e073 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -142,11 +142,6 @@ let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = funct
         get_mono (Future.force cu)
       else Univ.ContextSet.empty
 
-let get_direct_constraints = function
-| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
-| Direct (_, cu) ->
-  Future.chain cu get_mono
-
 module FMap = Future.UUIDMap
 
 let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } =
-- 
cgit v1.2.3