From 0ddf7d9c35eb2dd5f368e7a5735970ef1fd41fc6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 19 Nov 2017 19:08:35 +0100 Subject: [printing] Deprecate all printing functions accessing the global proof. We'd like to handle proofs functionally we thus recommend not to use printing functions without an explicit context. We also adapt most of the code, making more explicit where the printing environment is coming from. An open task is to refactor some code so we gradually make the `Pfedit.get_current_context ()` disappear. --- vernac/lemmas.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'vernac/lemmas.ml') diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 7b8a38d5f..a025bfff8 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -253,7 +253,9 @@ let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2) | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t) | App (t, args) -> mkApp (body_i t, args) - | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body ++ str ".") in + | _ -> + let sigma, env = Pfedit.get_current_context () in + anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr_env env sigma body ++ str ".") in let body_i = body_i body in match locality with | Discharge -> @@ -530,7 +532,5 @@ let save_proof ?proof = function Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj))) (* Miscellaneous *) +let get_current_context () = Pfedit.get_current_context () -let get_current_context () = - Pfedit.get_current_context () - -- cgit v1.2.3