4 files changed, 18 insertions, 31 deletions
diff --git a/plugins/extraction/plugin_base.dune b/plugins/extraction/dune
index 037b0d5053..0c01dcd488 100644
--- a/plugins/extraction/plugin_base.dune
+++ b/plugins/extraction/dune
@@ -3,3 +3,5 @@
  (public_name coq.plugins.extraction)
  (synopsis "Coq's extraction plugin")
  (libraries num coq.plugins.ltac))
+
+(coq.pp (modules g_extraction))
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 3a90d24c97..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 = Proof_global.get_proof pstate in
-  let sigma, env = Pfedit.get_current_context 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 (Proof_global.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 edbc1f5ea7..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:Proof_global.t -> unit
+val show_extraction : pstate:Declare.Proof.t -> unit
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index a53c2395f0..f8449bcda1 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -498,16 +498,8 @@ let info_file f =
 (* The objects defined below should survive an arbitrary time,
    so we register them to coq save/undo mechanism. *)
 
-let my_bool_option name initval =
-  let flag = ref initval in
-  let access = fun () -> !flag in
-  let () = declare_bool_option
-    {optdepr = false;
-     optkey = ["Extraction"; name];
-     optread = access;
-     optwrite = (:=) flag }
-  in
-  access
+let my_bool_option name value =
+  declare_bool_option_and_ref ~depr:false ~key:["Extraction"; name] ~value
 
 (*s Extraction AccessOpaque *)
 
@@ -588,25 +580,18 @@ let () = declare_int_option
 
 (* This option controls whether "dummy lambda" are removed when a
    toplevel constant is defined. *)
-let conservative_types_ref = ref false
-let conservative_types () = !conservative_types_ref
-
-let () = declare_bool_option
-  {optdepr = false;
-   optkey = ["Extraction"; "Conservative"; "Types"];
-   optread = (fun () -> !conservative_types_ref);
-   optwrite = (fun b -> conservative_types_ref := b) }
-
+let conservative_types =
+  declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Extraction"; "Conservative"; "Types"]
+    ~value:false
 
 (* Allows to print a comment at the beginning of the output files *)
-let file_comment_ref = ref ""
-let file_comment () = !file_comment_ref
-
-let () = declare_string_option
-  {optdepr = false;
-   optkey = ["Extraction"; "File"; "Comment"];
-   optread = (fun () -> !file_comment_ref);
-   optwrite = (fun s -> file_comment_ref := s) }
+let file_comment =
+  declare_string_option_and_ref
+    ~depr:false
+    ~key:["Extraction"; "File"; "Comment"]
+    ~value:""
 
 (*s Extraction Lang *)