diff options
| author | Emilio Jesus Gallego Arias | 2018-12-05 01:06:33 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-27 23:56:18 +0100 |
| commit | 2d8f2cc01d8d35baa39144274a700a9ebc66f794 (patch) | |
| tree | c3638f6994ca53ef5dc9a605500515f5cbfe0667 | |
| parent | 6ac4cfe51abf41c9e3bccb5f760df57258495a86 (diff) | |
[plugins] [extraction] Adapt to removal of imperative proof state.
| -rw-r--r-- | plugins/extraction/extract_env.ml | 13 | ||||
| -rw-r--r-- | plugins/extraction/extract_env.mli | 2 | ||||
| -rw-r--r-- | plugins/extraction/g_extraction.mlg | 4 |
3 files changed, 11 insertions, 8 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 diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 54fde2ca46..7ba7e05019 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -40,4 +40,4 @@ val structure_for_compute : (* Show the extraction of the current ongoing proof *) -val show_extraction : unit -> unit +val show_extraction : pstate:Proof_global.t option -> unit diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg index 1445dffefa..d7bb27f121 100644 --- a/plugins/extraction/g_extraction.mlg +++ b/plugins/extraction/g_extraction.mlg @@ -178,6 +178,6 @@ END (* Show the extraction of the current proof *) VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY -| [ "Show" "Extraction" ] - -> { show_extraction () } +| ![ proof ] [ "Show" "Extraction" ] + -> { fun ~pstate -> let () = show_extraction ~pstate in pstate } END |