From 030bb57d4b7e70d45379cab61903b75bf7a41b19 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 25 May 2020 16:43:01 +0200
Subject: [declare] Reify Proof.t API into the Proof module.

This is in preparation for the next commit which will clean-up the
current API flow in `Declare`.
---
 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 39c6c4ea54..af43c0517e 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -730,7 +730,7 @@ let extract_and_compile l =
 let show_extraction ~pstate =
   init ~inner:true false false;
   let prf = Declare.Proof.get pstate in
-  let sigma, env = Declare.get_current_context pstate in
+  let sigma, env = Declare.Proof.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