diff options
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index a0627dbe63..39c6c4ea54 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -729,13 +729,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 = Declare.Proof.get_proof pstate in + let prf = Declare.Proof.get 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 (Declare.Proof.get_proof_name pstate) in + let l = Label.of_id (Declare.Proof.get_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 |