diff options
| author | Pierre-Marie Pédrot | 2019-05-17 14:18:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-20 14:11:44 +0200 |
| commit | e69e4f7fd9aaba0e3fd6c38624e3fdb0bd96026c (patch) | |
| tree | caf9be18ce8da31926142946455fa7982f9d84fd /kernel/opaqueproof.ml | |
| parent | 27468ae02bbbf018743d53a9db49efa34b6d6a3e (diff) | |
Do not perform the section variable check on global recipes.
By construction, we know that Cooking is returning the right set of
used variables. This set has been checked already once at the time
when the definition was performed inside the section.
Diffstat (limited to 'kernel/opaqueproof.ml')
| -rw-r--r-- | kernel/opaqueproof.ml | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 423a416ca4..18c1bcc0f8 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -77,11 +77,6 @@ let subst_opaque sub = function | Indirect (s,dp,i) -> Indirect (sub::s,dp,i) | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque.") -let iter_direct_opaque f = function - | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") - | Direct (d,cu) -> - Direct (d,Future.chain cu (fun (c, u) -> f c; c, u)) - let discharge_direct_opaque ~cook_constr ci = function | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") | Direct (d,cu) -> @@ -100,10 +95,6 @@ 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) |