diff options
| author | Pierre-Marie Pédrot | 2019-09-26 15:36:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-09-26 15:54:24 +0200 |
| commit | acbf569a3b9f242fd704af9124c58697b8762d0d (patch) | |
| tree | f920fbebb00504f76c85678245de25946dac8d09 /kernel/opaqueproof.ml | |
| parent | 92006b6cc6b49ed6f892a7e5475f32ca852a9769 (diff) | |
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.
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; _ } = |