diff options
Diffstat (limited to 'plugins/extraction/extract_env.ml')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 40dbf8bea4..7f8e8b36ad 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -728,13 +728,13 @@ let extract_and_compile l = (* Show the extraction of the current ongoing proof *) let show_extraction ~pstate = init ~inner:true false false; - let prf = Proof_global.get_proof pstate in - let sigma, env = Proof_global.get_current_context pstate in + let prf = Declare.get_proof pstate in + let sigma, env = Declare.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_proof_name pstate) in + let l = Label.of_id (Declare.get_proof_name pstate) in let fake_ref = GlobRef.ConstRef (Constant.make2 mp l) in let decl = Dterm (fake_ref, ast, ty) in print_one_decl [] mp decl |