diff options
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 4 | ||||
| -rw-r--r-- | plugins/extraction/extract_env.mli | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 7f8e8b36ad..02383799a9 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 = Declare.get_proof pstate in + let prf = Declare.Proof.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 (Declare.get_proof_name pstate) in + let l = Label.of_id (Declare.Proof.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 diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 2e1509c5cc..06cc475200 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 : pstate:Declare.t -> unit +val show_extraction : pstate:Declare.Proof.t -> unit |