Merge PR#763: [proof] Deprecate redundant wrappers.

19 files changed, 188 insertions, 168 deletions

diff --git a/API/API.mli b/API/API.mli
index 0cfa3e328..68fbda7c7 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -3465,6 +3465,8 @@ sig
   (** @raise NoCurrentProof when outside proof mode. *)
 
   val discard_all : unit -> unit
+  val discard_current : unit -> unit
+  val get_current_proof_name : unit -> Names.Id.t
 end
 
 module Nametab :
@@ -3940,11 +3942,18 @@ sig
   val solve : ?with_end_tac:unit Proofview.tactic ->
       Vernacexpr.goal_selector -> int option -> unit Proofview.tactic ->
       Proof.proof -> Proof.proof * bool
-  val delete_current_proof : unit -> unit
   val cook_proof :
     unit -> (Names.Id.t * (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * Decl_kinds.goal_kind))
-  val get_current_proof_name : unit -> Names.Id.t
+
   val get_current_context : unit -> Evd.evar_map * Environ.env
+
+  (* Deprecated *)
+  val delete_current_proof : unit -> unit
+  [@@ocaml.deprecated "use Proof_global.discard_current"]
+
+  val get_current_proof_name : unit -> Names.Id.t
+  [@@ocaml.deprecated "use Proof_global.get_current_proof_name"]
+
 end
 
 module Tactics :
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 70245a8b1..8ffd15f9f 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -371,12 +371,12 @@ let generate_functional_principle (evd: Evd.evar_map ref)
     begin
       begin
 	try
-	  let id = Pfedit.get_current_proof_name () in
+	  let id = Proof_global.get_current_proof_name () in
 	  let s = Id.to_string id in
 	  let n = String.length "___________princ_________" in
 	  if String.length s >= n
 	  then if String.equal (String.sub s 0 n) "___________princ_________"
-	  then Pfedit.delete_current_proof ()
+	  then Proof_global.discard_current ()
 	  else ()
 	  else ()
 	with e when CErrors.noncritical e -> ()
@@ -524,12 +524,12 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con
        begin
 	 begin
 	   try
-	     let id = Pfedit.get_current_proof_name () in
+	     let id = Proof_global.get_current_proof_name () in
 	     let s = Id.to_string id in
 	     let n = String.length "___________princ_________" in
 	     if String.length s >= n
 	     then if String.equal (String.sub s 0 n) "___________princ_________"
-		  then Pfedit.delete_current_proof ()
+		  then Proof_global.discard_current ()
 		  else ()
 	     else ()
 	   with e when CErrors.noncritical e -> ()
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 7558ac7ac..6fe6888f3 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -161,7 +161,7 @@ let save with_clean id const (locality,_,kind) hook =
         let kn = declare_constant id ~local (DefinitionEntry const, k) in
 	(locality, ConstRef kn)
   in
-  if with_clean then  Pfedit.delete_current_proof ();
+  if with_clean then Proof_global.discard_current ();
   CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r);
   definition_message id
 
@@ -173,7 +173,7 @@ let cook_proof _ =
 
 let get_proof_clean do_reduce =
   let result = cook_proof do_reduce in
-  Pfedit.delete_current_proof ();
+  Proof_global.discard_current ();
   result
 
 let with_full_print f a =
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 20abde82f..3cd20a950 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1295,7 +1295,7 @@ let is_opaque_constant c =
 
 let open_new_goal 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 = get_current_proof_name () in
+  let current_proof_name = Proof_global.get_current_proof_name () in
   let name = match goal_name with
     | Some s -> s
     | None   ->
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 945b10bcf..0cd3ee2f9 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -22,7 +22,6 @@ open Nameops
 open Libnames
 open Globnames
 open Nametab
-open Pfedit
 open Refiner
 open Tacmach.New
 open Tactic_debug
@@ -629,7 +628,7 @@ let interp_gen kind ist pattern_mode flags env sigma c =
 let constr_flags () = {
   use_typeclasses = true;
   solve_unification_constraints = true;
-  use_hook = solve_by_implicit_tactic ();
+  use_hook = Pfedit.solve_by_implicit_tactic ();
   fail_evar = true;
   expand_evars = true }
 
@@ -644,14 +643,14 @@ let interp_type = interp_constr_gen IsType
 let open_constr_use_classes_flags () = {
   use_typeclasses = true;
   solve_unification_constraints = true;
-  use_hook = solve_by_implicit_tactic ();
+  use_hook = Pfedit.solve_by_implicit_tactic ();
   fail_evar = false;
   expand_evars = true }
 
 let open_constr_no_classes_flags () = {
   use_typeclasses = false;
   solve_unification_constraints = true;
-  use_hook = solve_by_implicit_tactic ();
+  use_hook = Pfedit.solve_by_implicit_tactic ();
   fail_evar = false;
   expand_evars = true }
 
diff --git a/printing/printer.ml b/printing/printer.ml
index 3c31dd96b..d6f0778f7 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -17,7 +17,6 @@ open Nametab
 open Evd
 open Proof_type
 open Refiner
-open Pfedit
 open Constrextern
 open Ppconstr
 open Declarations
@@ -812,7 +811,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
   end
 
 let pr_nth_open_subgoal n =
-  let pf = get_pftreestate () in
+  let pf = Proof_global.give_me_the_proof () in
   let { it=gls ; sigma=sigma } = Proof.V82.subgoals pf in
   pr_subgoal n sigma gls
 
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 3fb66d1b8..b28234a50 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -24,19 +24,6 @@ let _ = Goptions.declare_bool_option {
 
 let use_unification_heuristics () = !use_unification_heuristics_ref
 
-let refining = Proof_global.there_are_pending_proofs
-let check_no_pending_proofs = Proof_global.check_no_pending_proof
-
-let get_current_proof_name = Proof_global.get_current_proof_name
-let get_all_proof_names = Proof_global.get_all_proof_names
-
-type lemma_possible_guards = Proof_global.lemma_possible_guards
-type universe_binders = Proof_global.universe_binders
-
-let delete_proof = Proof_global.discard
-let delete_current_proof = Proof_global.discard_current
-let delete_all_proofs = Proof_global.discard_all
-
 let start_proof (id : Id.t) ?pl str sigma hyps c ?init_tac terminator =
   let goals = [ (Global.env_of_context hyps , c) ] in
   Proof_global.start_proof sigma id ?pl str goals terminator;
@@ -55,32 +42,20 @@ let cook_this_proof p =
 let cook_proof () =
   cook_this_proof (fst
     (Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x)))
-let get_pftreestate () =
-  Proof_global.give_me_the_proof ()
-
-let set_end_tac tac =
-  Proof_global.set_endline_tactic tac
-
-let set_used_variables l =
-  Proof_global.set_used_variables l
-let get_used_variables () =
-  Proof_global.get_used_variables ()
-
-let get_universe_binders () =
-  Proof_global.get_universe_binders ()
 
 exception NoSuchGoal
 let _ = CErrors.register_handler begin function
   | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.")
   | _ -> raise CErrors.Unhandled
 end
+
 let get_nth_V82_goal i =
   let p = Proof_global.give_me_the_proof () in
   let { it=goals ; sigma = sigma; } = Proof.V82.subgoals p in
   try
           { it=(List.nth goals (i-1)) ; sigma=sigma; }
   with Failure _ -> raise NoSuchGoal
-    
+
 let get_goal_context_gen i =
   let { it=goal ; sigma=sigma; } =  get_nth_V82_goal i in
   (sigma, Refiner.pf_env { it=goal ; sigma=sigma; })
@@ -106,7 +81,7 @@ let get_current_context () =
     (Evd.from_env env, env)
      | NoSuchGoal ->
         (* No more focused goals ? *)
-        let p = get_pftreestate () in
+        let p = Proof_global.give_me_the_proof () in
         let evd = Proof.in_proof p (fun x -> x) in
         (evd, Global.env ())
 
@@ -165,11 +140,11 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
   try
     let status = by tac in
     let _,(const,univs,_) = cook_proof () in
-    delete_current_proof ();
+    Proof_global.discard_current ();
     const, status, fst univs
   with reraise ->
     let reraise = CErrors.push reraise in
-    delete_current_proof ();
+    Proof_global.discard_current ();
     iraise reraise
 
 let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
@@ -257,4 +232,32 @@ let solve_by_implicit_tactic () = match !implicit_tactic with
 | None -> None
 | Some tac -> Some (apply_implicit_tactic tac)
 
+(** Deprecated functions  *)
+let refining = Proof_global.there_are_pending_proofs
+let check_no_pending_proofs = Proof_global.check_no_pending_proof
+
+let get_current_proof_name = Proof_global.get_current_proof_name
+let get_all_proof_names = Proof_global.get_all_proof_names
+
+type lemma_possible_guards = Proof_global.lemma_possible_guards
+type universe_binders = Proof_global.universe_binders
+
+let delete_proof = Proof_global.discard
+let delete_current_proof = Proof_global.discard_current
+let delete_all_proofs = Proof_global.discard_all
+
+let get_pftreestate () =
+  Proof_global.give_me_the_proof ()
+
+let set_end_tac tac =
+  Proof_global.set_endline_tactic tac
+
+let set_used_variables l =
+  Proof_global.set_used_variables l
+
+let get_used_variables () =
+  Proof_global.get_used_variables ()
+
+let get_universe_binders () =
+  Proof_global.get_universe_binders ()
 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 1bf65b8ae..f009593e9 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -14,39 +14,6 @@ open Term
 open Environ
 open Decl_kinds
 
-(** Several proofs can be opened simultaneously but at most one is
-   focused at some time. The following functions work by side-effect
-   on current set of open proofs. In this module, ``proofs'' means an
-   open proof (something started by vernacular command [Goal], [Lemma]
-   or [Theorem]), and ``goal'' means a subgoal of the current focused
-   proof *)
-
-(** {6 ... } *)
-(** [refining ()] tells if there is some proof in progress, even if a not
-   focused one *)
-
-val refining : unit -> bool
-
-(** [check_no_pending_proofs ()] fails if there is still some proof in
-   progress *)
-
-val check_no_pending_proofs : unit -> unit
-
-(** {6 ... } *)
-(** [delete_proof name] deletes proof of name [name] or fails if no proof
-    has this name *)
-
-val delete_proof : Id.t located -> unit
-
-(** [delete_current_proof ()] deletes current focused proof or fails if
-    no proof is focused *)
-
-val delete_current_proof : unit -> unit
-
-(** [delete_all_proofs ()] deletes all open proofs if any *)
-
-val delete_all_proofs : unit -> unit
-
 (** {6 ... } *)
 (** [start_proof s str env t hook tac] starts a proof of name [s] and
     conclusion [t]; [hook] is optionally a function to be applied at
@@ -55,12 +22,8 @@ val delete_all_proofs : unit -> unit
     systematically apply at initialization time (e.g. to start the
     proof of mutually dependent theorems) *)
 
-type lemma_possible_guards = Proof_global.lemma_possible_guards
-
-type universe_binders = Id.t Loc.located list
-
 val start_proof :
-  Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr ->
+  Id.t -> ?pl:Proof_global.universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr ->
   ?init_tac:unit Proofview.tactic ->
   Proof_global.proof_terminator -> unit
 
@@ -80,11 +43,6 @@ val cook_proof : unit ->
     (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind))
 
 (** {6 ... } *)
-(** [get_pftreestate ()] returns the current focused pending proof.
-   @raise NoCurrentProof if there is no pending proof. *)
-
-val get_pftreestate : unit -> Proof.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 *)
@@ -109,34 +67,6 @@ val current_proof_statement :
   unit -> Id.t * goal_kind * EConstr.types
 
 (** {6 ... } *)
-(** [get_current_proof_name ()] return the name of the current focused
-    proof or failed if no proof is focused *)
-
-val get_current_proof_name : unit -> Id.t
-
-(** [get_all_proof_names ()] returns the list of all pending proof names.
-    The first name is the current proof, the other names may come in
-    any order. *)
-
-val get_all_proof_names : unit -> Id.t list
-
-(** {6 ... } *)
-(** [set_end_tac tac] applies tactic [tac] to all subgoal generate
-    by [solve] *)
-
-val set_end_tac : Genarg.glob_generic_argument -> unit
-
-(** {6 ... } *)
-(** [set_used_variables l] declares that section variables [l] will be
-    used in the proof *)
-val set_used_variables :
-  Id.t list -> Context.Named.t * Names.Id.t Loc.located list
-val get_used_variables : unit -> Context.Named.t option
-
-(** {6 Universe binders } *)
-val get_universe_binders : unit -> universe_binders option
-
-(** {6 ... } *)
 (** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th
     subgoal of the current focused proof or raises a [UserError] if no
     proof is focused or if there is no [n]th subgoal. [solve SelectAll
@@ -191,3 +121,88 @@ val clear_implicit_tactic : unit -> unit
 
 (* Raise Exit if cannot solve *)
 val solve_by_implicit_tactic : unit -> Pretyping.inference_hook option
+
+(** {5 Deprecated functions in favor of [Proof_global]} *)
+
+(** {6 ... } *)
+(** Several proofs can be opened simultaneously but at most one is
+   focused at some time. The following functions work by side-effect
+   on current set of open proofs. In this module, ``proofs'' means an
+   open proof (something started by vernacular command [Goal], [Lemma]
+   or [Theorem]), and ``goal'' means a subgoal of the current focused
+   proof *)
+
+(** [refining ()] tells if there is some proof in progress, even if a not
+   focused one *)
+
+val refining : unit -> bool
+[@@ocaml.deprecated "use Proof_global.there_are_pending_proofs"]
+
+(** [check_no_pending_proofs ()] fails if there is still some proof in
+   progress *)
+
+val check_no_pending_proofs : unit -> unit
+[@@ocaml.deprecated "use Proof_global.check_no_pending_proofs"]
+
+(** {6 ... } *)
+(** [delete_proof name] deletes proof of name [name] or fails if no proof
+    has this name *)
+
+val delete_proof : Id.t located -> unit
+[@@ocaml.deprecated "use Proof_global.discard"]
+
+(** [delete_current_proof ()] deletes current focused proof or fails if
+    no proof is focused *)
+
+val delete_current_proof : unit -> unit
+[@@ocaml.deprecated "use Proof_global.discard_current"]
+
+(** [delete_all_proofs ()] deletes all open proofs if any *)
+val delete_all_proofs : unit -> unit
+[@@ocaml.deprecated "use Proof_global.discard_all"]
+
+(** [get_pftreestate ()] returns the current focused pending proof.
+   @raise NoCurrentProof if there is no pending proof. *)
+
+val get_pftreestate : unit -> Proof.proof
+[@@ocaml.deprecated "use Proof_global.give_me_the_proof"]
+
+(** {6 ... } *)
+(** [set_end_tac tac] applies tactic [tac] to all subgoal generate
+    by [solve] *)
+
+val set_end_tac : Genarg.glob_generic_argument -> unit
+[@@ocaml.deprecated "use Proof_global.set_endline_tactic"]
+
+(** {6 ... } *)
+(** [set_used_variables l] declares that section variables [l] will be
+    used in the proof *)
+val set_used_variables :
+  Id.t list -> Context.Named.t * Names.Id.t Loc.located list
+[@@ocaml.deprecated "use Proof_global.set_used_variables"]
+
+val get_used_variables : unit -> Context.Named.t option
+[@@ocaml.deprecated "use Proof_global.get_used_variables"]
+
+(** {6 Universe binders } *)
+val get_universe_binders : unit -> Proof_global.universe_binders option
+[@@ocaml.deprecated "use Proof_global.get_universe_binders"]
+
+(** {6 ... } *)
+(** [get_current_proof_name ()] return the name of the current focused
+    proof or failed if no proof is focused *)
+val get_current_proof_name : unit -> Id.t
+[@@ocaml.deprecated "use Proof_global.get_current_proof_name"]
+
+(** [get_all_proof_names ()] returns the list of all pending proof names.
+    The first name is the current proof, the other names may come in
+    any order. *)
+val get_all_proof_names : unit -> Id.t list
+[@@ocaml.deprecated "use Proof_global.get_all_proof_names"]
+
+type lemma_possible_guards = Proof_global.lemma_possible_guards
+[@@ocaml.deprecated "use Proof_global.lemma_possible_guards"]
+
+type universe_binders = Proof_global.universe_binders
+[@@ocaml.deprecated "use Proof_global.universe_binders"]
+
diff --git a/stm/stm.ml b/stm/stm.ml
index a79bf5426..1580b451d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -931,7 +931,7 @@ let show_script ?proof () =
   try
     let prf =
       try match proof with
-      | None -> Some (Pfedit.get_current_proof_name ())
+      | None -> Some (Proof_global.get_current_proof_name ())
       | Some (p,_) -> Some (p.Proof_global.id)
       with Proof_global.NoCurrentProof -> None
     in
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 773abb9f0..681db5d08 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -29,7 +29,6 @@ open Decl_kinds
 open Pattern
 open Patternops
 open Clenv
-open Pfedit
 open Tacred
 open Printer
 open Vernacexpr
@@ -1462,7 +1461,7 @@ let pr_hint_term sigma cl =
 
 (* print all hints that apply to the concl of the current goal *)
 let pr_applicable_hint () =
-  let pts = get_pftreestate () in
+  let pts = Proof_global.give_me_the_proof () in
   let glss = Proof.V82.subgoals pts in
   match glss.Evd.it with
   | [] -> CErrors.user_err Pp.(str "No focused goal.")
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cde891290..d0c6fdca5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -25,7 +25,6 @@ open Inductiveops
 open Reductionops
 open Globnames
 open Evd
-open Pfedit
 open Tacred
 open Genredexpr
 open Tacmach.New
@@ -543,7 +542,7 @@ end
 let fix ido n = match ido with
   | None ->
     Proofview.Goal.enter begin fun gl ->
-      let name = Pfedit.get_current_proof_name () in
+      let name = Proof_global.get_current_proof_name () in
       let id = new_fresh_id [] name gl in
       mutual_fix id n [] 0
     end
@@ -594,7 +593,7 @@ end
 let cofix ido = match ido with
   | None ->
     Proofview.Goal.enter begin fun gl ->
-      let name = Pfedit.get_current_proof_name () in
+      let name = Proof_global.get_current_proof_name () in
       let id = new_fresh_id [] name gl in
       mutual_cofix id [] 0
     end
@@ -1140,7 +1139,7 @@ let rec intros_move = function
 let tactic_infer_flags with_evar = {
   Pretyping.use_typeclasses = true;
   Pretyping.solve_unification_constraints = true;
-  Pretyping.use_hook = solve_by_implicit_tactic ();
+  Pretyping.use_hook = Pfedit.solve_by_implicit_tactic ();
   Pretyping.fail_evar = not with_evar;
   Pretyping.expand_evars = true }
 
@@ -5032,11 +5031,11 @@ let name_op_to_name name_op object_kind suffix =
   let default_gk = (Global, false, object_kind) in
   match name_op with
     | Some s ->
-      (try let _, gk, _ = current_proof_statement () in s, gk
+      (try let _, gk, _ = Pfedit.current_proof_statement () in s, gk
        with NoCurrentProof -> s, default_gk)
     | None   ->
       let name, gk =
-	try let name, gk, _ = current_proof_statement () in name, gk
+	try let name, gk, _ = Pfedit.current_proof_statement () in name, gk
 	with NoCurrentProof -> anon_id, default_gk in
       add_suffix name suffix, gk
 
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 908786565..0b0ef6717 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -187,7 +187,7 @@ end
     from cycling. *)
 let make_prompt () =
   try
-    (Names.Id.to_string (Pfedit.get_current_proof_name ())) ^ " < "
+    (Names.Id.to_string (Proof_global.get_current_proof_name ())) ^ " < "
   with Proof_global.NoCurrentProof ->
     "Coq < "
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index a61ade784..d4146ace1 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -285,7 +285,7 @@ let ensure_exists f =
 (* Compile a vernac file *)
 let compile verbosely f =
   let check_pending_proofs () =
-    let pfs = Pfedit.get_all_proof_names () in
+    let pfs = Proof_global.get_all_proof_names () in
     if not (List.is_empty pfs) then vernac_error (str "There are pending proofs")
   in
   match !Flags.compilation_mode with
diff --git a/vernac/command.ml b/vernac/command.ml
index b1425d703..998e7803e 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -187,7 +187,7 @@ let declare_definition ident (local, p, k) ce pl imps hook =
     let () = definition_message ident in
     let gr = VarRef ident in
     let () = maybe_declare_manual_implicits false gr imps in
-    let () = if Pfedit.refining () then
+    let () = if Proof_global.there_are_pending_proofs () then
 	       warn_definition_not_visible ident
     in
     gr
@@ -233,7 +233,7 @@ match local with
   let _ = declare_variable ident decl in
   let () = assumption_message ident in
   let () =
-    if not !Flags.quiet && Pfedit.refining () then
+    if not !Flags.quiet && Proof_global.there_are_pending_proofs () then
     Feedback.msg_info (str"Variable" ++ spc () ++ pr_id ident ++
     strbrk " is not visible from current goals")
   in
diff --git a/vernac/command.mli b/vernac/command.mli
index 9bbc2fdac..2a52d9bcb 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -15,7 +15,6 @@ open Vernacexpr
 open Constrexpr
 open Decl_kinds
 open Redexpr
-open Pfedit
 
 (** This file is about the interpretation of raw commands into typed
     ones and top-level declaration of the main Gallina objects *)
@@ -151,7 +150,7 @@ val declare_fixpoint :
   locality -> polymorphic ->
   recursive_preentry * lident list option * Evd.evar_universe_context * 
   (Context.Rel.t * Impargs.manual_implicits * int option) list ->
-  lemma_possible_guards -> decl_notation list -> unit
+  Proof_global.lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint : locality -> polymorphic -> 
   recursive_preentry * lident list option * Evd.evar_universe_context * 
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 77e356eb2..5bf419caf 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -209,7 +209,7 @@ let compute_proof_name locality = function
         user_err ?loc  (pr_id id ++ str " already exists.");
       id, pl
   | None ->
-      next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None
+      next_global_ident_away default_thm_id (Proof_global.get_all_proof_names ()), None
 
 let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,(_,imps))) =
   let t_i = norm t_i in
@@ -487,7 +487,7 @@ let save_proof ?proof = function
             let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
             Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes)
         | None ->
-            let pftree = Pfedit.get_pftreestate () in
+            let pftree = Proof_global.give_me_the_proof () in
             let id, k, typ = Pfedit.current_proof_statement () in
             let typ = EConstr.Unsafe.to_constr typ in
             let universes = Proof.initial_euctx pftree in
@@ -496,7 +496,7 @@ let save_proof ?proof = function
               Proof_global.return_proof ~allow_partial:true () in
             let sec_vars =
               if not !keep_admitted_vars then None
-              else match  Pfedit.get_used_variables(), pproofs with
+              else match Proof_global.get_used_variables(), pproofs with
               | Some _ as x, _ -> x
               | None, (pproof, _) :: _ -> 
                   let env = Global.env () in
@@ -504,7 +504,7 @@ let save_proof ?proof = function
                   let ids_def = Environ.global_vars_set env pproof in
                   Some (Environ.keep_hyps env (Idset.union ids_typ ids_def))
               | _ -> None in
-	    let names = Pfedit.get_universe_binders () in
+	    let names = Proof_global.get_universe_binders () in
             let evd = Evd.from_ctx universes in
             let binders, ctx = Evd.universe_context ?names evd in
             Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),
@@ -519,7 +519,7 @@ let save_proof ?proof = function
         | Some proof -> proof
       in
       (* if the proof is given explicitly, nothing has to be deleted *)
-      if Option.is_empty proof then Pfedit.delete_current_proof ();
+      if Option.is_empty proof then Proof_global.discard_current ();
       Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj)))
 
 (* Miscellaneous *)
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index d06b8fd14..a9c0d99f3 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -9,7 +9,6 @@
 open Names
 open Term
 open Decl_kinds
-open Pfedit
 
 type 'a declaration_hook
 val mk_hook :
@@ -21,16 +20,16 @@ val call_hook :
 (** A hook start_proof calls on the type of the definition being started *)
 val set_start_hook : (EConstr.types -> unit) -> unit
 
-val start_proof : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
-  ?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
+val start_proof : Id.t -> ?pl:Proof_global.universe_binders -> goal_kind -> Evd.evar_map ->
+  ?terminator:(Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
   ?sign:Environ.named_context_val -> EConstr.types ->
-  ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
+  ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> 
    unit declaration_hook -> unit
 
-val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
-  ?terminator:(lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
+val start_proof_univs : Id.t -> ?pl:Proof_global.universe_binders -> goal_kind -> Evd.evar_map ->
+  ?terminator:(Proof_global.lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
   ?sign:Environ.named_context_val -> EConstr.types ->
-  ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
+  ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> 
   (Evd.evar_universe_context option -> unit declaration_hook) -> unit
 
 val start_proof_com :
@@ -40,8 +39,8 @@ val start_proof_com :
 
 val start_proof_with_initialization : 
   goal_kind -> Evd.evar_map ->
-  (bool * lemma_possible_guards * unit Proofview.tactic list option) option ->
-  ((Id.t (* name of thm *) * universe_binders option) *
+  (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option ->
+  ((Id.t (* name of thm *) * Proof_global.universe_binders option) *
      (types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
   -> int list option -> unit declaration_hook -> unit
 
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 6dee95bc5..e03e9b803 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -947,7 +947,7 @@ let rec solve_obligation prg num tac =
   let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in
   let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator hook in
   let _ = Pfedit.by !default_tactic in
-  Option.iter (fun tac -> Pfedit.set_end_tac tac) tac
+  Option.iter (fun tac -> Proof_global.set_endline_tactic tac) tac
 
 and obligation (user_num, name, typ) tac =
   let num = pred user_num in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6830a5da1..c76ced56f 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -15,7 +15,6 @@ open Flags
 open Names
 open Nameops
 open Term
-open Pfedit
 open Tacmach
 open Constrintern
 open Prettyp
@@ -63,13 +62,13 @@ let show_proof () =
 
 let show_top_evars () =
   (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
-  let pfts = get_pftreestate () in
+  let pfts = Proof_global.give_me_the_proof () in
   let gls = Proof.V82.subgoals pfts in
   let sigma = gls.Evd.sigma in
   Feedback.msg_notice (pr_evars_int sigma 1 (Evarutil.non_instantiated sigma))
 
 let show_universes () =
-  let pfts = get_pftreestate () in
+  let pfts = Proof_global.give_me_the_proof () in
   let gls = Proof.V82.subgoals pfts in
   let sigma = gls.Evd.sigma in
   let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in
@@ -79,7 +78,7 @@ let show_universes () =
 (* Simulate the Intro(s) tactic *)
 let show_intro all =
   let open EConstr in
-  let pf = get_pftreestate() in
+  let pf = Proof_global.give_me_the_proof() in
   let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
   if not (List.is_empty gls) then begin
     let gl = {Evd.it=List.hd gls ; sigma = sigma; } in
@@ -498,7 +497,7 @@ let vernac_start_proof locality p kind l lettop =
       match id with
 	| Some (lid,_) -> Dumpglob.dump_definition lid false "prf"
 	| None -> ()) l;
-  if not(refining ()) then
+  if not(Proof_global.there_are_pending_proofs ()) then
     if lettop then
       user_err ~hdr:"Vernacentries.StartProof"
 	(str "Let declarations can only be used in proof editing mode.");
@@ -511,7 +510,7 @@ let vernac_end_proof ?proof = function
 let vernac_exact_proof c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the begining of a proof. *)
-  let status = by (Tactics.exact_proof c) in
+  let status = Pfedit.by (Tactics.exact_proof c) in
   save_proof (Vernacexpr.(Proved(Opaque None,None)));
   if not status then Feedback.feedback Feedback.AddedAxiom
 
@@ -657,7 +656,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
     user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
   match mexpr_ast_l with
     | [] ->
-       check_no_pending_proofs ();
+       Proof_global.check_no_pending_proof ();
        let binders_ast,argsexport =
         List.fold_right
          (fun (export,idl,ty) (args,argsexport) ->
@@ -703,7 +702,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
 
   match mty_ast_l with
     | [] ->
-       check_no_pending_proofs ();
+       Proof_global.check_no_pending_proof ();
        let binders_ast,argsexport =
 	 List.fold_right
          (fun (export,idl,ty) (args,argsexport) ->
@@ -751,7 +750,7 @@ let vernac_include l =
 (* Sections *)
 
 let vernac_begin_section (_, id as lid) =
-  check_no_pending_proofs ();
+  Proof_global.check_no_pending_proof ();
   Dumpglob.dump_definition lid true "sec";
   Lib.open_section id
 
@@ -765,7 +764,7 @@ let vernac_name_sec_hyp (_,id) set = Proof_using.name_set id set
 (* Dispatcher of the "End" command *)
 
 let vernac_end_segment (_,id as lid) =
-  check_no_pending_proofs ();
+  Proof_global.check_no_pending_proof ();
   match Lib.find_opening_node id with
   | Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid
   | Lib.OpenedModule (true,_,_,_) -> vernac_end_modtype lid
@@ -845,14 +844,14 @@ let focus_command_cond = Proof.no_cond command_focus
      there are no more goals to solve. It cannot be a tactic since
      all tactics fail if there are no further goals to prove. *)
 
-let vernac_solve_existential = instantiate_nth_evar_com
+let vernac_solve_existential = Pfedit.instantiate_nth_evar_com
 
 let vernac_set_end_tac tac =
   let env = Genintern.empty_glob_sign (Global.env ()) in
   let _, tac = Genintern.generic_intern env tac in
-  if not (refining ()) then
+  if not (Proof_global.there_are_pending_proofs ()) then
     user_err Pp.(str "Unknown command of the non proof-editing mode.");
-  set_end_tac tac
+  Proof_global.set_endline_tactic tac
     (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
 
 let vernac_set_used_variables e =
@@ -867,13 +866,13 @@ let vernac_set_used_variables e =
       user_err ~hdr:"vernac_set_used_variables"
         (str "Unknown variable: " ++ pr_id id))
     l;
-  let _, to_clear = set_used_variables l in
+  let _, to_clear = Proof_global.set_used_variables l in
   let to_clear = List.map snd to_clear in
   Proof_global.with_current_proof begin fun _ p ->
     if List.is_empty to_clear then (p, ())
     else
       let tac = Tactics.clear to_clear in
-      fst (solve SelectAll None tac p), ()
+      fst (Pfedit.solve SelectAll None tac p), ()
   end
 
 (*****************************)
@@ -917,12 +916,12 @@ let vernac_chdir = function
 (* State management *)
 
 let vernac_write_state file =
-  Pfedit.delete_all_proofs ();
+  Proof_global.discard_all ();
   let file = CUnix.make_suffix file ".coq" in
   States.extern_state file
 
 let vernac_restore_state file =
-  Pfedit.delete_all_proofs ();
+  Proof_global.discard_all ();
   let file = Loadpath.locate_file (CUnix.make_suffix file ".coq") in
   States.intern_state file
 
@@ -1516,7 +1515,7 @@ let vernac_print_option key =
   with Not_found -> error_undeclared_key key
 
 let get_current_context_of_args = function
-  | Some n -> get_goal_context n
+  | Some n -> Pfedit.get_goal_context n
   | None -> get_current_context ()
 
 let query_command_selector ?loc = function
@@ -1578,7 +1577,7 @@ let vernac_global_check c =
 
 
 let get_nth_goal n =
-  let pf = get_pftreestate() in
+  let pf = Proof_global.give_me_the_proof() in
   let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
   let gl = {Evd.it=List.nth gls (n-1) ; sigma = sigma; } in
   gl
@@ -1767,7 +1766,7 @@ let vernac_locate = let open Feedback in function
   | LocateFile f -> msg_notice (locate_file f)
 
 let vernac_register id r =
- if Pfedit.refining () then
+ if Proof_global.there_are_pending_proofs () then
     user_err Pp.(str "Cannot register a primitive while in proof editing mode.");
   let kn = Constrintern.global_reference (snd id) in
   if not (isConstRef kn) then
@@ -1838,12 +1837,12 @@ let vernac_show = let open Feedback in function
   | ShowExistentials -> show_top_evars ()
   | ShowUniverses -> show_universes ()
   | ShowProofNames ->
-      msg_notice (pr_sequence pr_id (Pfedit.get_all_proof_names()))
+      msg_notice (pr_sequence pr_id (Proof_global.get_all_proof_names()))
   | ShowIntros all -> show_intro all
   | ShowMatch id -> show_match id
 
 let vernac_check_guard () =
-  let pts = get_pftreestate () in
+  let pts = Proof_global.give_me_the_proof () in
   let pfterm = List.hd (Proof.partial_proof pts) in
   let message =
     try