From 1dc70876b4a5ad027b3b73aa6ba741e89320d17d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 11 Apr 2020 17:14:38 -0400
Subject: [declare] Rename `Declare.t` to `Declare.Proof.t`

This still needs API cleanup but we defer it to the moment we are
ready to make the internals private.
---
 plugins/extraction/extract_env.ml  | 4 ++--
 plugins/extraction/extract_env.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/extraction')

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
-- 
cgit v1.2.3