diff options
| author | Gaëtan Gilbert | 2019-10-01 10:12:33 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-01 10:12:33 +0200 |
| commit | 77fd11a9f012a2878e13451e9d8a9f500c6392eb (patch) | |
| tree | b8440203d6eb46a6af050e493661a0a29bf19233 /kernel/opaqueproof.ml | |
| parent | 41f3d8f0b0b6efbb7133cd4e44c70a1d9105c3e9 (diff) | |
| parent | 7e70815c2f326518c71f25fd9b222281a757572b (diff) | |
Merge PR #10797: Implement discharging in kernel
Reviewed-by: SkySkimmer
Reviewed-by: maximedenes
Diffstat (limited to 'kernel/opaqueproof.ml')
| -rw-r--r-- | kernel/opaqueproof.ml | 5 |
1 files changed, 0 insertions, 5 deletions
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; _ } = |