diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/opaqueproof.ml | 7 | ||||
| -rw-r--r-- | kernel/opaqueproof.mli | 2 |
2 files changed, 0 insertions, 9 deletions
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index d168f3cb7e..5584b74b36 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -119,13 +119,6 @@ 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) -> - if DirPath.equal dp odp - then Some(Future.chain (snd (Int.Map.find i prfs)) snd) - else !get_univ dp i - module FMap = Future.UUIDMap let a_constr = Future.from_val (mkRel 1) diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 501779a917..b84aeaf35a 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -40,8 +40,6 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab 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 val subst_opaque : substitution -> opaque -> opaque |