diff options
| -rw-r--r-- | kernel/term_typing.ml | 2 | ||||
| -rw-r--r-- | kernel/term_typing.mli | 12 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 2 | ||||
| -rw-r--r-- | toplevel/obligations.ml | 2 |
4 files changed, 11 insertions, 7 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 5c95aacae..dce30413d 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -286,7 +286,7 @@ let translate_local_def env id centry = let translate_mind env kn mie = Indtypes.check_inductive env kn mie -let handle_side_effects env ce = { ce with +let handle_entry_side_effects env ce = { ce with const_entry_body = Future.chain ~greedy:true ~pure:true ce.const_entry_body (fun ((body, ctx), side_eff) -> (handle_side_effects env body side_eff, ctx), Declareops.no_seff); diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 8be1c76e0..a699bce38 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -20,10 +20,14 @@ val translate_local_assum : env -> types -> types val mk_pure_proof : constr -> proof_output -(* returns the same definition_entry but with side effects turned into - * let-ins or beta redexes. it is meant to get a term out of a not yet - * type checked proof *) -val handle_side_effects : env -> definition_entry -> definition_entry +val handle_side_effects : env -> constr -> Declareops.side_effects -> constr +(** Returns the term where side effects have been turned into let-ins or beta + redexes. *) + +val handle_entry_side_effects : env -> definition_entry -> definition_entry +(** Same as {!handle_side_effects} but applied to entries. Only modifies the + {!Entries.const_entry_body} field. It is meant to get a term out of a not + yet type checked proof. *) val translate_constant : env -> constant -> constant_entry -> constant_body diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 09d94a9ce..8e0f3accb 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -149,7 +149,7 @@ let build_by_tactic 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 = Term_typing.handle_side_effects env ce in + let ce = Term_typing.handle_entry_side_effects env ce in let (cb, ctx), se = Future.force ce.const_entry_body in assert(Declareops.side_effects_is_empty se); assert(Univ.ContextSet.is_empty ctx); diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 38580882e..be5711820 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -780,7 +780,7 @@ let solve_by_tac name evi t poly ctx = let (entry,_,ctx') = Pfedit.build_constant_by_tactic id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in let env = Global.env () in - let entry = Term_typing.handle_side_effects env entry in + let entry = Term_typing.handle_entry_side_effects env entry in let body, eff = Future.force entry.Entries.const_entry_body in assert(Declareops.side_effects_is_empty eff); assert(Univ.ContextSet.is_empty (snd body)); |