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

7 files changed, 98 insertions, 93 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 1397746dd9..c8208cd444 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -363,7 +363,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id
   (* XXX: We need to normalize the type, otherwise Admitted / Qed will fails!
      This is due to a bug in proof_global :( *)
   let termtype = Evarutil.nf_evar sigma termtype in
-  let lemma = Declare.start_proof ~name:id ~poly ~info ~impargs sigma termtype in
+  let lemma = Declare.Proof.start ~name:id ~poly ~info ~impargs sigma termtype in
   (* spiwack: I don't know what to do with the status here. *)
   let lemma =
     match term with
@@ -375,15 +375,15 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id
           Tactics.New.reduce_after_refine;
         ]
       in
-      let lemma, _ = Declare.by init_refine lemma in
+      let lemma, _ = Declare.Proof.by init_refine lemma in
       lemma
     | None ->
-      let lemma, _ = Declare.by (Tactics.auto_intros_tac ids) lemma in
+      let lemma, _ = Declare.Proof.by (Tactics.auto_intros_tac ids) lemma in
       lemma
   in
   match tac with
   | Some tac ->
-    let lemma, _ = Declare.by tac lemma in
+    let lemma, _ = Declare.Proof.by tac lemma in
     lemma
   | None ->
     lemma
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 925a2d8389..99db8df803 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -271,7 +271,7 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
   let init_terms = Some fixdefs in
   let evd = Evd.from_ctx ctx in
   let lemma =
-    Declare.start_proof_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl
+    Declare.Proof.start_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl
       evd (Some(cofix,indexes,init_terms)) thms None in
   (* Declare notations *)
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 29f2713192..e72f5a0397 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -2079,6 +2079,12 @@ let save_lemma_proved_delayed ~proof ~info ~idopt =
 
 module Proof = struct
   type nonrec t = t
+  let start = start_proof
+  let start_dependent = start_dependent_proof
+  let start_with_initialization = start_proof_with_initialization
+  let save = save_lemma_proved
+  let save_admitted = save_lemma_admitted
+  let by = by
   let get = get_proof
   let get_name = get_proof_name
   let fold ~f = fold_proof f
@@ -2091,4 +2097,7 @@ module Proof = struct
   let update_global_env = update_global_env
   let get_open_goals = get_open_goals
   let info { info } = info
+  let get_goal_context = get_goal_context
+  let get_current_goal_context = get_current_goal_context
+  let get_current_context = get_current_context
 end
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 25a4d80f49..10d5501285 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -133,8 +133,57 @@ module Proof : sig
 
   type t
 
-  (** XXX: These are internal and will go away from publis API once
-     lemmas is merged here *)
+  (** [start ~name ~poly ~info sigma goals] starts a proof of
+      name [name] with goals [goals] (a list of pairs of environment and
+      conclusion); [poly] determines if the proof is universe
+      polymorphic. The proof is started in the evar map [sigma] (which
+      can typically contain universe constraints). *)
+  val start
+    :  name:Names.Id.t
+    -> poly:bool
+    -> ?impargs:Impargs.manual_implicits
+    -> info:Info.t
+    -> Evd.evar_map
+    -> EConstr.t
+    -> t
+
+  (** Like [start] except that there may be dependencies between initial goals. *)
+  val start_dependent
+    :  name:Names.Id.t
+    -> poly:bool
+    -> info:Info.t
+    -> Proofview.telescope
+    -> t
+
+  (** Pretty much internal, used by the Lemma / Fixpoint vernaculars *)
+  val start_with_initialization
+    :  ?hook:Hook.t
+    -> poly:bool
+    -> scope:Locality.locality
+    -> kind:Decls.logical_kind
+    -> udecl:UState.universe_decl
+    -> Evd.evar_map
+    -> (bool * lemma_possible_guards * Constr.t option list option) option
+    -> Recthm.t list
+    -> int list option
+    -> t
+
+  (** Qed a proof  *)
+  val save
+    : proof:t
+    -> opaque:Vernacexpr.opacity_flag
+    -> idopt:Names.lident option
+    -> unit
+
+  (** Admit a proof *)
+  val save_admitted : proof:t -> unit
+
+  (** [by tac] applies tactic [tac] to the 1st subgoal of the current
+      focused proof.
+      Returns [false] if an unsafe tactic has been used. *)
+  val by : unit Proofview.tactic -> t -> t * bool
+
+  (** Operations on ongoing proofs *)
   val get : t -> Proof.t
   val get_name : t -> Names.Id.t
 
@@ -148,8 +197,7 @@ module Proof : sig
 
   (** Sets the section variables assumed by the proof, returns its closure
    * (w.r.t. type dependencies and let-ins covered by it) *)
-  val set_used_variables : t ->
-    Names.Id.t list -> Constr.named_context * t
+  val set_used_variables : t -> Names.Id.t list -> Constr.named_context * t
 
   val compact : t -> t
 
@@ -160,46 +208,27 @@ module Proof : sig
 
   val get_open_goals : t -> int
 
-  (* Internal, don't use *)
-  val info : t -> Info.t
-end
+  (** Helpers to obtain proof state when in an interactive proof *)
 
-(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of
-   name [name] with goals [goals] (a list of pairs of environment and
-   conclusion); [poly] determines if the proof is universe
-   polymorphic. The proof is started in the evar map [sigma] (which
-   can typically contain universe constraints), and with universe
-   bindings [udecl]. *)
-val start_proof
-  :  name:Names.Id.t
-  -> poly:bool
-  -> ?impargs:Impargs.manual_implicits
-  -> info:Info.t
-  -> Evd.evar_map
-  -> EConstr.t
-  -> Proof.t
+  (** [get_goal_context n] returns the context of the [n]th subgoal of
+      the current focused proof or raises a [UserError] if there is no
+      focused proof or if there is no more subgoals *)
 
-(** Like [start_proof] except that there may be dependencies between
-    initial goals. *)
-val start_dependent_proof
-  :  name:Names.Id.t
-  -> poly:bool
-  -> info:Info.t
-  -> Proofview.telescope
-  -> Proof.t
+  val get_goal_context : t -> int -> Evd.evar_map * Environ.env
 
-(** Pretty much internal, used by the Lemma / Fixpoint vernaculars *)
-val start_proof_with_initialization
-  :  ?hook:Hook.t
-  -> poly:bool
-  -> scope:Locality.locality
-  -> kind:Decls.logical_kind
-  -> udecl:UState.universe_decl
-  -> Evd.evar_map
-  -> (bool * lemma_possible_guards * Constr.t option list option) option
-  -> Recthm.t list
-  -> int list option
-  -> Proof.t
+  (** [get_current_goal_context ()] works as [get_goal_context 1] *)
+  val get_current_goal_context : t -> Evd.evar_map * Environ.env
+
+  (** [get_current_context ()] returns the context of the
+      current focused goal. If there is no focused goal but there
+      is a proof in progress, it returns the corresponding evar_map.
+      If there is no pending proof then it returns the current global
+      environment and empty evar_map. *)
+  val get_current_context : t -> Evd.evar_map * Environ.env
+
+  (* Internal, don't use *)
+  val info : t -> Info.t
+end
 
 (** Proof entries represent a proof that has been finished, but still
    not registered with the kernel.
@@ -300,11 +329,6 @@ val return_proof : Proof.t -> closed_proof_output
 val return_partial_proof : Proof.t -> closed_proof_output
 val close_future_proof : feedback_id:Stateid.t -> Proof.t -> closed_proof_output Future.computation -> proof_object
 
-(** [by tac] applies tactic [tac] to the 1st subgoal of the current
-    focused proof.
-    Returns [false] if an unsafe tactic has been used. *)
-val by : unit Proofview.tactic -> Proof.t -> Proof.t * bool
-
 (** Semantics of this function is a bit dubious, use with care *)
 val build_by_tactic
   :  ?side_eff:bool
@@ -315,24 +339,6 @@ val build_by_tactic
   -> unit Proofview.tactic
   -> Constr.constr * Constr.types option * Entries.universes_entry * bool * UState.t
 
-(** {6 Helpers to obtain proof state when in an interactive proof } *)
-
-(** [get_goal_context n] returns the context of the [n]th subgoal of
-   the current focused proof or raises a [UserError] if there is no
-   focused proof or if there is no more subgoals *)
-
-val get_goal_context : Proof.t -> int -> Evd.evar_map * Environ.env
-
-(** [get_current_goal_context ()] works as [get_goal_context 1] *)
-val get_current_goal_context : Proof.t -> Evd.evar_map * Environ.env
-
-(** [get_current_context ()] returns the context of the
-  current focused goal. If there is no focused goal but there
-  is a proof in progress, it returns the corresponding evar_map.
-  If there is no pending proof then it returns the current global
-  environment and empty evar_map. *)
-val get_current_context : Proof.t -> Evd.evar_map * Environ.env
-
 (** Information for a constant *)
 module CInfo : sig
 
@@ -524,16 +530,6 @@ val dependencies : Obligation.t array -> int -> Int.Set.t
 
 end
 
-val save_lemma_proved
-  : proof:Proof.t
-  -> opaque:Vernacexpr.opacity_flag
-  -> idopt:Names.lident option
-  -> unit
-
-val save_lemma_admitted :
-     proof:Proof.t
-  -> unit
-
 (** Special cases for delayed proofs, in this case we must provide the
    proof information so the proof won't be forced. *)
 val save_lemma_admitted_delayed :
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 86cad967b9..57aa79d749 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -146,8 +146,8 @@ let rec solve_obligation prg num tac =
   in
   let info = Declare.Info.make ~proof_ending ~scope ~kind () in
   let poly = Internal.get_poly prg in
-  let lemma = Declare.start_proof ~name:obl.obl_name ~poly ~impargs:[] ~info evd (EConstr.of_constr obl.obl_type) in
-  let lemma = fst @@ Declare.by !default_tactic lemma in
+  let lemma = Declare.Proof.start ~name:obl.obl_name ~poly ~impargs:[] ~info evd (EConstr.of_constr obl.obl_type) in
+  let lemma = fst @@ Declare.Proof.by !default_tactic lemma in
   let lemma = Option.cata (fun tac -> Declare.Proof.set_endline_tactic tac lemma) lemma tac in
   lemma
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6295587844..89294fee8c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -34,12 +34,12 @@ let (f_interp_redexp, interp_redexp_hook) = Hook.make ()
 let get_current_or_global_context ~pstate =
   match pstate with
   | None -> let env = Global.env () in Evd.(from_env env, env)
-  | Some p -> Declare.get_current_context p
+  | Some p -> Declare.Proof.get_current_context p
 
 let get_goal_or_global_context ~pstate glnum =
   match pstate with
   | None -> let env = Global.env () in Evd.(from_env env, env)
-  | Some p -> Declare.get_goal_context p glnum
+  | Some p -> Declare.Proof.get_goal_context p glnum
 
 let cl_of_qualid = function
   | FunClass -> Coercionops.CL_FUN
@@ -95,7 +95,7 @@ let show_proof ~pstate =
   try
     let pstate = Option.get pstate in
     let p = Declare.Proof.get pstate in
-    let sigma, _ = Declare.get_current_context pstate in
+    let sigma, _ = Declare.Proof.get_current_context pstate in
     let pprf = Proof.partial_proof p in
     (* In the absence of an environment explicitly attached to the
        proof and on top of which side effects of the proof would be pushed, ,
@@ -521,7 +521,7 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
     else (* We fix the variables to ensure they won't be lowered to Set *)
       Evd.fix_undefined_variables evd
   in
-  Declare.start_proof_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl
+  Declare.Proof.start_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl
 
 let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in function
 | Coercion ->
@@ -595,15 +595,15 @@ let vernac_start_proof ~atts kind l =
 
 let vernac_end_proof ~lemma = let open Vernacexpr in function
   | Admitted ->
-    Declare.save_lemma_admitted ~proof:lemma
+    Declare.Proof.save_admitted ~proof:lemma
   | Proved (opaque,idopt) ->
-    Declare.save_lemma_proved ~proof:lemma ~opaque ~idopt
+    Declare.Proof.save ~proof:lemma ~opaque ~idopt
 
 let vernac_exact_proof ~lemma c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the beginning of a proof. *)
-  let lemma, status = Declare.by (Tactics.exact_proof c) lemma in
-  let () = Declare.save_lemma_proved ~proof:lemma ~opaque:Opaque ~idopt:None in
+  let lemma, status = Declare.Proof.by (Tactics.exact_proof c) lemma in
+  let () = Declare.Proof.save ~proof:lemma ~opaque:Opaque ~idopt:None in
   if not status then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_assumption ~atts discharge kind l nl =
@@ -1602,8 +1602,8 @@ let get_current_context_of_args ~pstate =
     let env = Global.env () in Evd.(from_env env, env)
   | Some lemma ->
     function
-    | Some n -> Declare.get_goal_context lemma n
-    | None -> Declare.get_current_context lemma
+    | Some n -> Declare.Proof.get_goal_context lemma n
+    | None -> Declare.Proof.get_current_context lemma
 
 let query_command_selector ?loc = function
   | None -> None
@@ -1703,7 +1703,7 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt =
     let natureofid = match decl with
                      | LocalAssum _ -> "Hypothesis"
                      | LocalDef (_,bdy,_) ->"Constant (let in)" in
-    let sigma, env = Declare.get_current_context pstate in
+    let sigma, env = Declare.Proof.get_current_context pstate in
     v 0 (Id.print id ++ str":" ++ pr_econstr_env env sigma (NamedDecl.get_type decl) ++ fnl() ++ fnl()
          ++ str natureofid ++ str " of the goal context.")
   with (* fallback to globals *)
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 536f413bf4..2a5762b712 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -169,7 +169,7 @@ module Declare = struct
   let discard_all () = s_lemmas := None
   let update_global_env () = dd (Declare.Proof.update_global_env)
 
-  let get_current_context () = cc Declare.get_current_context
+  let get_current_context () = cc Declare.Proof.get_current_context
 
   let get_all_proof_names () =
     try cc_stack LemmaStack.get_all_proof_names