From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- proofs/pfedit.ml | 22 +++++++++++++--------- 1 file changed, 13 insertions(+), 9 deletions(-) (limited to 'proofs/pfedit.ml') diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index d1b6afe2..02dbd1fd 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -42,7 +42,7 @@ let cook_this_proof p = let cook_proof () = cook_this_proof (fst - (Proof_global.close_proof ~keep_body_ucst_sepatate:false (fun x -> x))) + (Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x))) let get_pftreestate () = Proof_global.give_me_the_proof () @@ -108,7 +108,7 @@ let solve ?with_end_tac gi info_lvl tac pr = let () = match info_lvl with | None -> () - | Some i -> Pp.ppnl (hov 0 (Proofview.Trace.pr_info ~lvl:i info)) + | Some i -> Pp.msg_info (hov 0 (Proofview.Trace.pr_info ~lvl:i info)) in (p,status) with @@ -133,7 +133,7 @@ open Decl_kinds let next = let n = ref 0 in fun () -> incr n; !n let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac = - let evd = Evd.from_env ~ctx Environ.empty_env in + let evd = Evd.from_ctx ctx in start_proof id goal_kind evd sign typ (fun _ -> ()); try let status = by tac in @@ -145,16 +145,20 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo delete_current_proof (); iraise reraise -let build_by_tactic env ctx ?(poly=false) typ tac = +let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac = let id = Id.of_string ("temporary_proof"^string_of_int (next())) in 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_entry_side_effects env ce 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 - assert(Declareops.side_effects_is_empty se); - assert(Univ.ContextSet.is_empty ctx); - cb, status, univs + let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in + assert(Safe_typing.empty_private_constants = se); + cb, status, Evd.evar_universe_context univs' let refine_by_tactic env sigma ty tac = (** Save the initial side-effects to restore them afterwards. We set the @@ -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 (**********************************************************************) -- cgit v1.2.3