From 9908ce57e15a316ff692ce31f493651734998ded Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 2 Apr 2020 01:08:24 -0400
Subject: [proof] Move proof_global functionality to Proof_global from Pfedit

This actually gets `Pfedit` out of the dependency picture [can be
almost merged with `Proof` now, as it is what it manipulates] and
would allow to reduce the exported low-level API from `Proof_global`,
as `map_fold_proof` is not used anymore.
---
 plugins/extraction/extract_env.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 3a90d24c97..40dbf8bea4 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -729,7 +729,7 @@ let extract_and_compile l =
 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 sigma, env = Proof_global.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
-- 
cgit v1.2.3