diff options
Diffstat (limited to 'plugins/extraction/extract_env.ml')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 0fa9be21c9..8f17f7b2dd 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -750,16 +750,19 @@ let extract_and_compile l = Feedback.msg_notice (str "Extracted code successfully compiled") (* Show the extraction of the current ongoing proof *) - -let show_extraction () = +let show_extraction ~pstate = + let pstate = match pstate with + | None -> CErrors.user_err Pp.(str "No ongoing proof") + | Some pstate -> pstate + in init ~inner:true false false; - let prf = Proof_global.give_me_the_proof () in - let sigma, env = Pfedit.get_current_context () in + let prf = Proof_global.give_me_the_proof pstate in + let sigma, env = Pfedit.get_current_context pstate in let trms = Proof.partial_proof prf in let extr_term t = let ast, ty = extract_constr env sigma t in let mp = Lib.current_mp () in - let l = Label.of_id (Proof_global.get_current_proof_name ()) in + let l = Label.of_id (Proof_global.get_current_proof_name pstate) in let fake_ref = ConstRef (Constant.make2 mp l) in let decl = Dterm (fake_ref, ast, ty) in print_one_decl [] mp decl |