diff options
Diffstat (limited to 'plugins/extraction/extract_env.ml')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 8f17f7b2dd..c5439ffaf6 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -751,10 +751,6 @@ let extract_and_compile l = (* Show the extraction of the current ongoing proof *) 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 pstate in let sigma, env = Pfedit.get_current_context pstate in |