aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/extract_env.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index efd5b5575f..7d04fee7c1 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.pstate -> unit
+val show_extraction : pstate:Proof_global.t -> unit