diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/opaqueproof.ml | 16 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 6 |
2 files changed, 11 insertions, 11 deletions
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 5e20c1b514..400f9feeea 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -78,12 +78,12 @@ let subst_opaque sub = function let iter_direct_opaque f = function | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") | Direct (d,cu) -> - Direct (d,Future.chain ~pure:true cu (fun (c, u) -> f c; c, u)) + 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) -> - Direct (ci::d,Future.chain ~pure:true cu (fun (c, u) -> cook_constr c, u)) + Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u)) let join_opaque { opaque_val = prfs; opaque_dir = odp } = function | Direct (_,cu) -> ignore(Future.join cu) @@ -105,7 +105,7 @@ let force_proof { opaque_val = prfs; opaque_dir = odp } = function | Indirect (l,dp,i) -> let pt = if DirPath.equal dp odp - then Future.chain ~pure:true (snd (Int.Map.find i prfs)) fst + then Future.chain (snd (Int.Map.find i prfs)) fst else !get_opaque dp i in let c = Future.force pt in force_constr (List.fold_right subst_substituted l (from_val c)) @@ -120,20 +120,20 @@ let force_constraints { opaque_val = prfs; opaque_dir = odp } = function | Some u -> Future.force u let get_constraints { opaque_val = prfs; opaque_dir = odp } = function - | Direct (_,cu) -> Some(Future.chain ~pure:true cu snd) + | Direct (_,cu) -> Some(Future.chain cu snd) | Indirect (_,dp,i) -> if DirPath.equal dp odp - then Some(Future.chain ~pure:true (snd (Int.Map.find i prfs)) snd) + then Some(Future.chain (snd (Int.Map.find i prfs)) snd) else !get_univ dp i let get_proof { opaque_val = prfs; opaque_dir = odp } = function - | Direct (_,cu) -> Future.chain ~pure:true cu fst + | Direct (_,cu) -> Future.chain cu fst | Indirect (l,dp,i) -> let pt = if DirPath.equal dp odp - then Future.chain ~pure:true (snd (Int.Map.find i prfs)) fst + then Future.chain (snd (Int.Map.find i prfs)) fst else !get_opaque dp i in - Future.chain ~pure:true pt (fun c -> + Future.chain pt (fun c -> force_constr (List.fold_right subst_substituted l (from_val c))) module FMap = Future.UUIDMap diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 22e109b01c..f93b24b3ee 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -266,7 +266,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let tyj = infer_type env typ in let proofterm = - Future.chain ~pure:true body (fun ((body,uctx),side_eff) -> + Future.chain body (fun ((body,uctx),side_eff) -> let j, uctx = match trust with | Pure -> let env = push_context_set uctx env in @@ -535,7 +535,7 @@ let export_side_effects mb env ce = let { const_entry_body = body } = c in let _, eff = Future.force body in let ce = DefinitionEntry { c with - const_entry_body = Future.chain ~pure:true body + const_entry_body = Future.chain body (fun (b_ctx, _) -> b_ctx, ()) } in let not_exists (c,_,_,_) = try ignore(Environ.lookup_constant c env); false @@ -628,7 +628,7 @@ let translate_local_def mb env id centry = let translate_mind env kn mie = Indtypes.check_inductive env kn mie let inline_entry_side_effects env ce = { ce with - const_entry_body = Future.chain ~pure:true + const_entry_body = Future.chain ce.const_entry_body (fun ((body, ctx), side_eff) -> let body, ctx',_ = inline_side_effects env body ctx side_eff in (body, ctx'), ()); |