aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/pfedit.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-10-28 16:46:42 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2015-10-28 17:31:53 +0100
commit908dcd613b12645f3b62bf44c2696b80a0b16940 (patch)
treee1f6d5b1479f39ff634a47b2fa637e8aab4a0d13 /proofs/pfedit.ml
parent0a1b046d37761fe47435d5041bb5031e3f7d6613 (diff)
Avoid type checking private_constants (side_eff) again during Qed (#4357).
Side effects are now an opaque data type, called private_constant, you can only obtain from safe_typing. When add_constant is called on a definition_entry that contains private constants, they are either - inlined in the main proof term but not re-checked - declared globally without re-checking them As a safety measure, the opaque data type contains a pointer to the revstruct (an internal field of safe_env that changes every time a new constant is added), and such pointer is compared with the current value store in safe_env when the private_constant is inlined. Only when the comparison is successful the private_constant is not re-checked. Otherwise else it is. In short, we accept into the kernel private constant only when they arrive in the very same order and on top of the very same env they arrived when we fist checked them. Note: private_constants produced by workers never pass the safety measure (the revstruct pointer is an Ephemeron). Sending back the entire revstruct is possible but: 1. we lack a way to quickly compare two revstructs, 2. it can be large.
Diffstat (limited to 'proofs/pfedit.ml')
-rw-r--r--proofs/pfedit.ml10
1 files changed, 7 insertions, 3 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 00ef8ecaf..02dbd1fdc 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -150,10 +150,14 @@ let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac =
let sign = val_of_named_context (named_context env) in
let gk = Global, poly, Proof Theorem in
let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in
- let ce = if side_eff then Term_typing.handle_entry_side_effects env ce else { ce with const_entry_body = Future.chain ~pure:true ce.const_entry_body (fun (pt, _) -> pt, Declareops.no_seff) } in
+ let ce =
+ if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce
+ else { ce with
+ const_entry_body = Future.chain ~pure:true ce.const_entry_body
+ (fun (pt, _) -> pt, Safe_typing.empty_private_constants) } in
let (cb, ctx), se = Future.force ce.const_entry_body in
let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in
- assert(Declareops.side_effects_is_empty se);
+ assert(Safe_typing.empty_private_constants = se);
cb, status, Evd.evar_universe_context univs'
let refine_by_tactic env sigma ty tac =
@@ -188,7 +192,7 @@ let refine_by_tactic env sigma ty tac =
other goals that were already present during its invocation, so that
those goals rely on effects that are not present anymore. Hopefully,
this hack will work in most cases. *)
- let ans = Term_typing.handle_side_effects env ans neff in
+ let ans = Safe_typing.inline_private_constants_in_constr env ans neff in
ans, sigma
(**********************************************************************)