[proof] Move proof_global functionality to Proof_global from Pfedit

This actually gets `Pfedit` out of the dependency picture [can be
almost merged with `Proof` now, as it is what it manipulates] and
would allow to reduce the exported low-level API from `Proof_global`,
as `map_fold_proof` is not used anymore.

6 files changed, 124 insertions, 129 deletions

diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index e85d94cd72..8abd68d28d 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -91,7 +91,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in
   let ectx = Evd.evar_universe_context sigma in
   let (const, safe, ectx) =
-    try Pfedit.build_constant_by_tactic ~name ~opaque:Proof_global.Transparent ~poly ~uctx:ectx ~sign:secsign concl solve_tac
+    try Proof_global.build_constant_by_tactic ~name ~opaque:Proof_global.Transparent ~poly ~uctx:ectx ~sign:secsign concl solve_tac
     with Logic_monad.TacticFailure e as src ->
     (* if the tactic [tac] fails, it reports a [TacticFailure e],
        which is an error irrelevant to the proof system (in fact it
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
index c139594f13..20975cbc57 100644
--- a/tactics/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -10,8 +10,6 @@
 
 open Pp
 open Util
-open Names
-open Environ
 open Evd
 
 let use_unification_heuristics =
@@ -20,48 +18,6 @@ let use_unification_heuristics =
     ~key:["Solve";"Unification";"Constraints"]
     ~value:true
 
-exception NoSuchGoal
-let () = CErrors.register_handler begin function
-  | NoSuchGoal -> Some Pp.(str "No such goal.")
-  | _ -> None
-end
-
-let get_nth_V82_goal p i =
-  let Proof.{ sigma; goals } = Proof.data p in
-  try { it = List.nth goals (i-1) ; sigma }
-  with Failure _ -> raise NoSuchGoal
-
-let get_goal_context_gen pf i =
-  let { it=goal ; sigma=sigma; } = get_nth_V82_goal pf i in
-  (sigma, Refiner.pf_env { it=goal ; sigma=sigma; })
-
-let get_goal_context pf i =
-  let p = Proof_global.get_proof pf in
-  get_goal_context_gen p i
-
-let get_current_goal_context pf =
-  let p = Proof_global.get_proof pf in
-  try get_goal_context_gen p 1
-  with
-  | NoSuchGoal ->
-    (* spiwack: returning empty evar_map, since if there is no goal,
-       under focus, there is no accessible evar either. EJGA: this
-       seems strange, as we have pf *)
-    let env = Global.env () in
-    Evd.from_env env, env
-
-let get_proof_context p =
-  try get_goal_context_gen p 1
-  with
-  | NoSuchGoal ->
-    (* No more focused goals *)
-    let { Proof.sigma } = Proof.data p in
-    sigma, Global.env ()
-
-let get_current_context pf =
-  let p = Proof_global.get_proof pf in
-  get_proof_context p
-
 let solve ?with_end_tac gi info_lvl tac pr =
     let tac = match with_end_tac with
       | None -> tac
@@ -105,39 +61,9 @@ let solve ?with_end_tac gi info_lvl tac pr =
     in
     (p,status)
 
-let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None tac)
-
 (**********************************************************************)
 (* Shortcut to build a term using tactics *)
 
-let next = let n = ref 0 in fun () -> incr n; !n
-
-let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ~uctx ~sign ~poly typ tac =
-  let evd = Evd.from_ctx uctx in
-  let goals = [ (Global.env_of_context sign , typ) ] in
-  let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in
-  let pf, status = by tac pf in
-  let open Proof_global in
-  let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false pf in
-  match entries with
-  | [entry] ->
-    entry, status, uctx
-  | _ ->
-    CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term")
-
-let build_by_tactic ?(side_eff=true) env ~uctx ~poly ~typ tac =
-  let name = Id.of_string ("temporary_proof"^string_of_int (next())) in
-  let sign = val_of_named_context (named_context env) in
-  let ce, status, univs = build_constant_by_tactic ~name ~uctx ~sign ~poly typ tac in
-  let cb, uctx =
-    if side_eff then Declare.inline_private_constants ~uctx env ce
-    else
-      (* GG: side effects won't get reset: no need to treat their universes specially *)
-      let (cb, ctx), _eff = Future.force ce.Declare.proof_entry_body in
-      cb, UState.merge ~sideff:false Evd.univ_rigid uctx ctx
-  in
-  cb, ce.Declare.proof_entry_type, status, univs
-
 let refine_by_tactic ~name ~poly env sigma ty tac =
   (* Save the initial side-effects to restore them afterwards. We set the
      current set of side-effects to be empty so that we can retrieve the
diff --git a/tactics/pfedit.mli b/tactics/pfedit.mli
index c49e997757..8d06a260da 100644
--- a/tactics/pfedit.mli
+++ b/tactics/pfedit.mli
@@ -16,30 +16,6 @@ open Environ
 
 (** {6 ... } *)
 
-exception NoSuchGoal
-
-(** [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_global.t -> int -> Evd.evar_map * env
-
-(** [get_current_goal_context ()] works as [get_goal_context 1] *)
-val get_current_goal_context : Proof_global.t -> Evd.evar_map * env
-
-(** [get_proof_context ()] gets the goal context for the first subgoal
-    of the proof *)
-val get_proof_context : Proof.t -> Evd.evar_map * 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_global.t -> Evd.evar_map * env
-
-(** {6 ... } *)
-
 (** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th
     subgoal of the current focused proof. [solve SelectAll
     tac] applies [tac] to all subgoals. *)
@@ -48,38 +24,9 @@ val solve : ?with_end_tac:unit Proofview.tactic ->
       Goal_select.t -> int option -> unit Proofview.tactic ->
       Proof.t -> Proof.t * bool
 
-(** [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_global.t -> Proof_global.t * bool
-
 (** Option telling if unification heuristics should be used. *)
 val use_unification_heuristics : unit -> bool
 
-(** [build_by_tactic typ tac] returns a term of type [typ] by calling
-    [tac]. The return boolean, if [false] indicates the use of an unsafe
-    tactic. *)
-
-val build_constant_by_tactic
-  :  name:Id.t
-  -> ?opaque:Proof_global.opacity_flag
-  -> uctx:UState.t
-  -> sign:named_context_val
-  -> poly:bool
-  -> EConstr.types
-  -> unit Proofview.tactic
-  -> Evd.side_effects Declare.proof_entry * bool * UState.t
-
-val build_by_tactic
-  :  ?side_eff:bool
-  -> env
-  -> uctx:UState.t
-  -> poly:bool
-  -> typ:EConstr.types
-  -> unit Proofview.tactic
-  -> constr * types option * bool * UState.t
-
 val refine_by_tactic
   :  name:Id.t
   -> poly:bool
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index 98de0c848b..78691d8c74 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -282,3 +282,74 @@ let update_global_env =
       let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
       let p, (status,info), _ = Proof.run_tactic (Global.env ()) tac p in
       p)
+
+let next = let n = ref 0 in fun () -> incr n; !n
+
+let by tac = map_fold_proof (Pfedit.solve (Goal_select.SelectNth 1) None tac)
+
+let build_constant_by_tactic ~name ?(opaque=Transparent) ~uctx ~sign ~poly typ tac =
+  let evd = Evd.from_ctx uctx in
+  let goals = [ (Global.env_of_context sign , typ) ] in
+  let pf = start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in
+  let pf, status = by tac pf in
+  let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false pf in
+  match entries with
+  | [entry] ->
+    entry, status, uctx
+  | _ ->
+    CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term")
+
+let build_by_tactic ?(side_eff=true) env ~uctx ~poly ~typ tac =
+  let name = Id.of_string ("temporary_proof"^string_of_int (next())) in
+  let sign = Environ.(val_of_named_context (named_context env)) in
+  let ce, status, univs = build_constant_by_tactic ~name ~uctx ~sign ~poly typ tac in
+  let cb, uctx =
+    if side_eff then Declare.inline_private_constants ~uctx env ce
+    else
+      (* GG: side effects won't get reset: no need to treat their universes specially *)
+      let (cb, ctx), _eff = Future.force ce.Declare.proof_entry_body in
+      cb, UState.merge ~sideff:false Evd.univ_rigid uctx ctx
+  in
+  cb, ce.Declare.proof_entry_type, status, univs
+
+exception NoSuchGoal
+let () = CErrors.register_handler begin function
+  | NoSuchGoal -> Some Pp.(str "No such goal.")
+  | _ -> None
+end
+
+let get_nth_V82_goal p i =
+  let Proof.{ sigma; goals } = Proof.data p in
+  try { Evd.it = List.nth goals (i-1) ; sigma }
+  with Failure _ -> raise NoSuchGoal
+
+let get_goal_context_gen pf i =
+  let { Evd.it=goal ; sigma=sigma; } = get_nth_V82_goal pf i in
+  (sigma, Refiner.pf_env { Evd.it=goal ; sigma=sigma; })
+
+let get_goal_context pf i =
+  let p = get_proof pf in
+  get_goal_context_gen p i
+
+let get_current_goal_context pf =
+  let p = get_proof pf in
+  try get_goal_context_gen p 1
+  with
+  | NoSuchGoal ->
+    (* spiwack: returning empty evar_map, since if there is no goal,
+       under focus, there is no accessible evar either. EJGA: this
+       seems strange, as we have pf *)
+    let env = Global.env () in
+    Evd.from_env env, env
+
+let get_proof_context p =
+  try get_goal_context_gen p 1
+  with
+  | NoSuchGoal ->
+    (* No more focused goals *)
+    let { Proof.sigma } = Proof.data p in
+    sigma, Global.env ()
+
+let get_current_context pf =
+  let p = get_proof pf in
+  get_proof_context p
diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli
index 874708ded8..c41a9c656e 100644
--- a/tactics/proof_global.mli
+++ b/tactics/proof_global.mli
@@ -96,3 +96,54 @@ val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
  * (w.r.t. type dependencies and let-ins covered by it) *)
 val set_used_variables : t ->
   Names.Id.t list -> Constr.named_context * t
+
+(** [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
+
+(** [build_by_tactic typ tac] returns a term of type [typ] by calling
+    [tac]. The return boolean, if [false] indicates the use of an unsafe
+    tactic. *)
+val build_constant_by_tactic
+  :  name:Names.Id.t
+  -> ?opaque:opacity_flag
+  -> uctx:UState.t
+  -> sign:Environ.named_context_val
+  -> poly:bool
+  -> EConstr.types
+  -> unit Proofview.tactic
+  -> Evd.side_effects Declare.proof_entry * bool * UState.t
+
+val build_by_tactic
+  :  ?side_eff:bool
+  -> Environ.env
+  -> uctx:UState.t
+  -> poly:bool
+  -> typ:EConstr.types
+  -> unit Proofview.tactic
+  -> Constr.constr * Constr.types option * bool * UState.t
+
+(** {6 ... } *)
+
+exception NoSuchGoal
+
+(** [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 : t -> int -> Evd.evar_map * Environ.env
+
+(** [get_current_goal_context ()] works as [get_goal_context 1] *)
+val get_current_goal_context : t -> Evd.evar_map * Environ.env
+
+(** [get_proof_context ()] gets the goal context for the first subgoal
+    of the proof *)
+val get_proof_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 : t -> Evd.evar_map * Environ.env
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 0c4e496650..f9f2a78c35 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -1,7 +1,7 @@
 DeclareScheme
+Pfedit
 Declare
 Proof_global
-Pfedit
 Dnet
 Dn
 Btermdn