[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`.

3 files changed, 24 insertions, 25 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 2c85ae079f..79f311e282 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -855,13 +855,14 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
      constructing the lemma Ensures by: obvious i*)
   let info = Declare.Info.make () in
   let lemma =
-    Declare.start_proof ~name:(mk_equation_id f_id) ~poly:false ~info
+    Declare.Proof.start ~name:(mk_equation_id f_id) ~poly:false ~info
       ~impargs:[] evd lemma_type
   in
-  let lemma, _ = Declare.by (Proofview.V82.tactic prove_replacement) lemma in
+  let lemma, _ =
+    Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma
+  in
   let () =
-    Declare.save_lemma_proved ~proof:lemma ~opaque:Vernacexpr.Transparent
-      ~idopt:None
+    Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
   in
   evd
 
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index a914cef6e4..50ce783579 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1520,15 +1520,15 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
           let typ, _ = lemmas_types_infos.(i) in
           let info = Declare.Info.make () in
           let lemma =
-            Declare.start_proof ~name:lem_id ~poly:false ~info ~impargs:[] !evd
+            Declare.Proof.start ~name:lem_id ~poly:false ~info ~impargs:[] !evd
               typ
           in
           let lemma =
-            fst @@ Declare.by (Proofview.V82.tactic (proving_tac i)) lemma
+            fst @@ Declare.Proof.by (Proofview.V82.tactic (proving_tac i)) lemma
           in
           let () =
-            Declare.save_lemma_proved ~proof:lemma
-              ~opaque:Vernacexpr.Transparent ~idopt:None
+            Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
+              ~idopt:None
           in
           let finfo =
             match find_Function_infos (fst f_as_constant) with
@@ -1586,12 +1586,12 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
           let lem_id = mk_complete_id f_id in
           let info = Declare.Info.make () in
           let lemma =
-            Declare.start_proof ~name:lem_id ~poly:false sigma ~info ~impargs:[]
+            Declare.Proof.start ~name:lem_id ~poly:false sigma ~info ~impargs:[]
               (fst lemmas_types_infos.(i))
           in
           let lemma =
             fst
-              (Declare.by
+              (Declare.Proof.by
                  (Proofview.V82.tactic
                     (observe_tac
                        ("prove completeness (" ^ Id.to_string f_id ^ ")")
@@ -1599,8 +1599,8 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
                  lemma)
           in
           let () =
-            Declare.save_lemma_proved ~proof:lemma
-              ~opaque:Vernacexpr.Transparent ~idopt:None
+            Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
+              ~idopt:None
           in
           let finfo =
             match find_Function_infos (fst f_as_constant) with
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 9f36eada45..5a188ca82b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -58,8 +58,7 @@ let declare_fun name kind ?univs value =
     (Declare.declare_constant ~name ~kind (Declare.DefinitionEntry ce))
 
 let defined lemma =
-  Declare.save_lemma_proved ~proof:lemma ~opaque:Vernacexpr.Transparent
-    ~idopt:None
+  Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
 
 let def_of_const t =
   match Constr.kind t with
@@ -1490,19 +1489,19 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
                      [Hints.Hint_db.empty TransparentState.empty false] ]))
     in
     let lemma = build_proof env (Evd.from_env env) start_tac end_tac in
-    Declare.save_lemma_proved ~proof:lemma ~opaque:opacity ~idopt:None
+    Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None
   in
   let info = Declare.Info.make ~hook:(Declare.Hook.make hook) () in
   let lemma =
-    Declare.start_proof ~name:na ~poly:false (* FIXME *) ~info ~impargs:[] sigma
+    Declare.Proof.start ~name:na ~poly:false (* FIXME *) ~info ~impargs:[] sigma
       gls_type
   in
   let lemma =
     if Indfun_common.is_strict_tcc () then
-      fst @@ Declare.by (Proofview.V82.tactic tclIDTAC) lemma
+      fst @@ Declare.Proof.by (Proofview.V82.tactic tclIDTAC) lemma
     else
       fst
-      @@ Declare.by
+      @@ Declare.Proof.by
            (Proofview.V82.tactic (fun g ->
                 tclTHEN decompose_and_tac
                   (tclORELSE
@@ -1533,18 +1532,18 @@ let com_terminate interactive_proof tcc_lemma_name tcc_lemma_ref is_mes
   let start_proof env ctx tac_start tac_end =
     let info = Declare.Info.make ~hook () in
     let lemma =
-      Declare.start_proof ~name:thm_name ~poly:false (*FIXME*) ~info ctx
+      Declare.Proof.start ~name:thm_name ~poly:false (*FIXME*) ~info ctx
         ~impargs:[]
         (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref))
     in
     let lemma =
       fst
-      @@ Declare.by
+      @@ Declare.Proof.by
            (New.observe_tac (fun _ _ -> str "starting_tac") tac_start)
            lemma
     in
     fst
-    @@ Declare.by
+    @@ Declare.Proof.by
          (Proofview.V82.tactic
             (observe_tac
                (fun _ _ -> str "whole_start")
@@ -1607,12 +1606,12 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
   let equation_lemma_type = subst1 f_constr equation_lemma_type in
   let info = Declare.Info.make () in
   let lemma =
-    Declare.start_proof ~name:eq_name ~poly:false evd ~info ~impargs:[]
+    Declare.Proof.start ~name:eq_name ~poly:false evd ~info ~impargs:[]
       (EConstr.of_constr equation_lemma_type)
   in
   let lemma =
     fst
-    @@ Declare.by
+    @@ Declare.Proof.by
          (Proofview.V82.tactic
             (start_equation f_ref terminate_ref (fun x ->
                  prove_eq
@@ -1646,8 +1645,7 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
   in
   let _ =
     Flags.silently
-      (fun () ->
-        Declare.save_lemma_proved ~proof:lemma ~opaque:opacity ~idopt:None)
+      (fun () -> Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None)
       ()
   in
   ()