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/funind/recdef.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 51d3286715..ffb9a7e69b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -27,7 +27,6 @@ open Tacticals
 open Tacmach
 open Tactics
 open Nametab
-open Declare
 open Tacred
 open Glob_term
 open Pretyping
@@ -54,8 +53,9 @@ let find_reference sl s =
   locate (make_qualid dp (Id.of_string s))
 
 let declare_fun name kind ?univs value =
-  let ce = definition_entry ?univs value (*FIXME *) in
-  GlobRef.ConstRef (declare_constant ~name ~kind (DefinitionEntry ce))
+  let ce = Declare.definition_entry ?univs value (*FIXME *) in
+  GlobRef.ConstRef
+    (Declare.declare_constant ~name ~kind (Declare.DefinitionEntry ce))
 
 let defined lemma =
   Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent ~idopt:None
@@ -1336,7 +1336,7 @@ let whole_start concl_tac nb_args is_mes func input_type relation rec_arg_num :
     g
 
 let get_current_subgoals_types pstate =
-  let p = Declare.get_proof pstate in
+  let p = Declare.Proof.get_proof pstate in
   let Proof.{goals = sgs; sigma; _} = Proof.data p in
   (sigma, List.map (Goal.V82.abstract_type sigma) sgs)
 
@@ -1416,7 +1416,7 @@ let is_opaque_constant c =
 let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
     (gls_type, decompose_and_tac, nb_goal) =
   (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *)
-  let current_proof_name = Lemmas.pf_fold Declare.get_proof_name lemma in
+  let current_proof_name = Lemmas.pf_fold Declare.Proof.get_proof_name lemma in
   let name =
     match goal_name with
     | Some s -> s
@@ -1514,7 +1514,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
                   g))
            lemma
   in
-  if Lemmas.(pf_fold Declare.get_open_goals) lemma = 0 then (
+  if Lemmas.(pf_fold Declare.Proof.get_open_goals) lemma = 0 then (
     defined lemma; None )
   else Some lemma
 
-- 
cgit v1.2.3