Merge PR #9935: [api] [proof] Alert users that `Vernacstate.Proof_global` is not to be used.

Ack-by: ejgallego
Ack-by: gares
Reviewed-by: maximedenes

8 files changed, 44 insertions, 34 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 74be300134..816316487c 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -65,6 +65,7 @@ let get_current_context () =
   with Vernacstate.Proof_global.NoCurrentProof ->
     let env = Global.env() in
     Evd.from_env env, env
+  [@@ocaml.warning "-3"]
 
 (* term printers *)
 let envpp pp = let sigma,env = get_current_context () in pp env sigma
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 543ff924bd..38839f3488 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -238,7 +238,8 @@ let goals () =
       Some (export_pre_goals Proof.(data newp) (process_goal_diffs diff_goal_map oldp))
     end else
       Some (export_pre_goals Proof.(data newp) process_goal)
-  with Vernacstate.Proof_global.NoCurrentProof -> None;;
+  with Vernacstate.Proof_global.NoCurrentProof -> None
+  [@@ocaml.warning "-3"];;
 
 let evars () =
   try
@@ -251,6 +252,7 @@ let evars () =
     let el = List.map map_evar exl in
     Some el
   with Vernacstate.Proof_global.NoCurrentProof -> None
+  [@@ocaml.warning "-3"]
 
 let hints () =
   try
@@ -264,7 +266,7 @@ let hints () =
       let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in
       Some (hint_hyps, concl_next_tac)
   with Vernacstate.Proof_global.NoCurrentProof -> None
-
+  [@@ocaml.warning "-3"]
 
 (** Other API calls *)
 
@@ -297,6 +299,7 @@ let status force =
     Interface.status_allproofs = allproofs;
     Interface.status_proofnum = Stm.current_proof_depth ~doc:(get_doc ());
   }
+  [@@ocaml.warning "-3"]
 
 let export_coq_object t = {
   Interface.coq_object_prefix = t.Search.coq_object_prefix;
@@ -340,6 +343,7 @@ let search flags =
   List.map export_coq_object (Search.interface_search ?pstate (
     List.map (fun (c, b) -> (import_search_constraint c, b)) flags)
   )
+  [@@ocaml.warning "-3"]
 
 let export_option_value = function
   | Goptions.BoolValue b   -> Interface.BoolValue b
diff --git a/stm/stm.ml b/stm/stm.ml
index e1ab45163a..06bc6e3340 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -27,6 +27,8 @@ open Feedback
 open Vernacexpr
 open Vernacextend
 
+module PG_compat = Vernacstate.Proof_global [@@ocaml.warning "-3"]
+
 let is_vtkeep = function VtKeep _ -> true | _ -> false
 let get_vtkeep = function VtKeep x -> x | _ -> assert false
 
@@ -139,8 +141,8 @@ let may_pierce_opaque = function
   | _ -> false
 
 let update_global_env () =
-  if Vernacstate.Proof_global.there_are_pending_proofs () then
-    Vernacstate.Proof_global.update_global_env ()
+  if PG_compat.there_are_pending_proofs () then
+    PG_compat.update_global_env ()
 
 module Vcs_ = Vcs.Make(Stateid.Self)
 type future_proof = Proof_global.closed_proof_output Future.computation
@@ -948,7 +950,7 @@ end = struct (* {{{ *)
             let prev = (VCS.visit id).next in
             if is_cached_and_valid prev
             then { s with proof =
-                Vernacstate.Proof_global.copy_terminators
+                PG_compat.copy_terminators
                   ~src:((get_cached prev).proof) ~tgt:s.proof }
             else s
            with VCS.Expired -> s in
@@ -957,7 +959,7 @@ end = struct (* {{{ *)
          if is_cached_and_valid ontop then
            let s = get_cached ontop in
            let s = { s with proof =
-             Vernacstate.Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in
+             PG_compat.copy_terminators ~src:s.proof ~tgt:pstate } in
            let s = { s with system =
              States.replace_summary s.system
                begin
@@ -1009,8 +1011,8 @@ end = struct (* {{{ *)
       if feedback_processed then
         Hooks.(call state_computed ~doc id ~in_cache:false);
       VCS.reached id;
-      if Vernacstate.Proof_global.there_are_pending_proofs () then
-        VCS.goals id (Vernacstate.Proof_global.get_open_goals ())
+      if PG_compat.there_are_pending_proofs () then
+        VCS.goals id (PG_compat.get_open_goals ())
     with e ->
       let (e, info) = CErrors.push e in
       let good_id = !cur_id in
@@ -1130,9 +1132,9 @@ let show_script ?proof () =
   try
     let prf =
       try match proof with
-      | None -> Some (Vernacstate.Proof_global.get_current_proof_name ())
+      | None -> Some (PG_compat.get_current_proof_name ())
       | Some (p,_) -> Some (p.Proof_global.id)
-      with Vernacstate.Proof_global.NoCurrentProof -> None
+      with PG_compat.NoCurrentProof -> None
     in
     let cmds = get_script prf in
     let _,_,_,indented_cmds =
@@ -1295,7 +1297,7 @@ end = struct (* {{{ *)
             | Some vcs, _ -> vcs in
           let cb, _ =
             try Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs)
-            with Failure _ -> raise Vernacstate.Proof_global.NoCurrentProof in
+            with Failure _ -> raise PG_compat.NoCurrentProof in
           let n = fold_until (fun n (_,vcs,_,_,_) ->
             if List.mem cb (Vcs_.branches vcs) then `Cont (n+1) else `Stop n)
             0 id in
@@ -1333,7 +1335,7 @@ end = struct (* {{{ *)
             | None -> true
         done;
         !rv
-    with Not_found | Vernacstate.Proof_global.NoCurrentProof -> None
+    with Not_found | PG_compat.NoCurrentProof -> None
 
 end (* }}} *)
 
@@ -1594,7 +1596,7 @@ end = struct (* {{{ *)
       let wall_clock2 = Unix.gettimeofday () in
       Aux_file.record_in_aux_at ?loc "proof_build_time"
         (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
-      let p = Vernacstate.Proof_global.return_proof ~allow_partial:drop_pt () in
+      let p = PG_compat.return_proof ~allow_partial:drop_pt () in
       if drop_pt then feedback ~id Complete;
       p)
 
@@ -1621,7 +1623,7 @@ end = struct (* {{{ *)
              to set the state manually here *)
           State.unfreeze st;
           let pobject, _ =
-            Vernacstate.Proof_global.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in
+            PG_compat.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in
           let terminator = (* The one sent by master is an InvalidKey *)
             Lemmas.(standard_proof_terminator []) in
 
@@ -1758,15 +1760,15 @@ end = struct (* {{{ *)
     try
       Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false stop;
       if drop then
-        let _proof = Vernacstate.Proof_global.return_proof ~allow_partial:true () in
+        let _proof = PG_compat.return_proof ~allow_partial:true () in
         `OK_ADMITTED
       else begin
       (* The original terminator, a hook, has not been saved in the .vio*)
-      Vernacstate.Proof_global.set_terminator (Lemmas.standard_proof_terminator []);
+      PG_compat.set_terminator (Lemmas.standard_proof_terminator []);
 
       let opaque = Proof_global.Opaque in
       let proof =
-        Vernacstate.Proof_global.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in
+        PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in
       (* We jump at the beginning since the kernel handles side effects by also
        * looking at the ones that happen to be present in the current env *)
       Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false start;
@@ -2016,7 +2018,7 @@ end = struct (* {{{ *)
     try
       Reach.known_state ~doc:dummy_doc (* XXX should be vcs *) ~cache:false id;
       State.purify (fun () ->
-       let Proof.{sigma=sigma0} = Proof.data (Vernacstate.Proof_global.give_me_the_proof ()) in
+       let Proof.{sigma=sigma0} = Proof.data (PG_compat.give_me_the_proof ()) in
        let g = Evd.find sigma0 r_goal in
        let is_ground c = Evarutil.is_ground_term sigma0 c in
        if not (
@@ -2028,7 +2030,7 @@ end = struct (* {{{ *)
            "goals only"))
        else begin
         let (i, ast) = r_ast in
-        Vernacstate.Proof_global.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p);
+        PG_compat.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p);
         (* STATE SPEC:
          * - start : id
          * - return: id
@@ -2037,7 +2039,7 @@ end = struct (* {{{ *)
         *)
         let st = Vernacstate.freeze_interp_state ~marshallable:false in
         ignore(stm_vernac_interp r_state_fb st ast);
-        let Proof.{sigma} = Proof.data (Vernacstate.Proof_global.give_me_the_proof ()) in
+        let Proof.{sigma} = Proof.data (PG_compat.give_me_the_proof ()) in
         match Evd.(evar_body (find sigma r_goal)) with
         | Evd.Evar_empty -> RespNoProgress
         | Evd.Evar_defined t ->
@@ -2084,7 +2086,7 @@ end = struct (* {{{ *)
     stm_fail ~st fail (fun () ->
     (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () ->
     ignore(TaskQueue.with_n_workers nworkers (fun queue ->
-    Vernacstate.Proof_global.with_current_proof (fun _ p ->
+    PG_compat.with_current_proof (fun _ p ->
       let Proof.{goals} = Proof.data p in
       let open TacTask in
       let res = CList.map_i (fun i g ->
@@ -2117,7 +2119,7 @@ end = struct (* {{{ *)
           let open Notations in
           match Future.join f with
           | Some (pt, uc) ->
-            let sigma, env = Vernacstate.Proof_global.get_current_context () in
+            let sigma, env = PG_compat.get_current_context () in
             stm_pperr_endline (fun () -> hov 0 (
               str"g=" ++ int (Evar.repr gid) ++ spc () ++
               str"t=" ++ (Printer.pr_constr_env env sigma pt) ++ spc () ++
@@ -2399,8 +2401,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
               end in
            match (VCS.get_info base_state).state with
            | FullState { Vernacstate.proof } ->
-               Option.iter Vernacstate.Proof_global.unfreeze proof;
-               Vernacstate.Proof_global.with_current_proof (fun _ p ->
+               Option.iter PG_compat.unfreeze proof;
+               PG_compat.with_current_proof (fun _ p ->
                  feedback ~id:id Feedback.AddedAxiom;
                  fst (Pfedit.solve Goal_select.SelectAll None tac p), ());
                (* STATE SPEC:
@@ -2570,7 +2572,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                       | VtKeepDefined -> Proof_global.Transparent
                     in
                     let proof =
-                      Vernacstate.Proof_global.close_future_proof ~opaque ~feedback_id:id fp in
+                      PG_compat.close_future_proof ~opaque ~feedback_id:id fp in
                     if not delegate then ignore(Future.compute fp);
                     reach view.next;
                     let st = Vernacstate.freeze_interp_state ~marshallable:false in
@@ -2578,13 +2580,13 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                     feedback ~id:id Incomplete
                 | { VCS.kind = `Master }, _ -> assert false
                 end;
-                Vernacstate.Proof_global.discard_all ()
+                PG_compat.discard_all ()
               ), not redefine_qed, true
           | `Sync (name, `Immediate) -> (fun () ->
                 reach eop;
                 let st = Vernacstate.freeze_interp_state ~marshallable:false in
                 ignore(stm_vernac_interp id st x);
-                Vernacstate.Proof_global.discard_all ()
+                PG_compat.discard_all ()
               ), true, true
           | `Sync (name, reason) -> (fun () ->
                 log_processing_sync id name reason;
@@ -2603,7 +2605,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                       | VtKeepOpaque -> Opaque | VtKeepDefined -> Transparent
                       | VtKeepAxiom -> assert false
                     in
-                      Some(Vernacstate.Proof_global.close_proof ~opaque
+                      Some(PG_compat.close_proof ~opaque
                                 ~keep_body_ucst_separate:false
                                 (State.exn_on id ~valid:eop)) in
                 if keep <> VtKeep VtKeepAxiom then
@@ -2614,7 +2616,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                 let wall_clock3 = Unix.gettimeofday () in
                 Aux_file.record_in_aux_at ?loc:x.loc "proof_check_time"
                   (Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2));
-                Vernacstate.Proof_global.discard_all ()
+                PG_compat.discard_all ()
               ), true, true
           | `MaybeASync (start, nodes, name, delegate) -> (fun () ->
                 reach ~cache:true start;
@@ -2875,7 +2877,7 @@ let merge_proof_branch ~valid ?id qast keep brname =
       VCS.checkout VCS.Branch.master;
       `Unfocus qed_id
   | { VCS.kind = `Master } ->
-       Exninfo.iraise (State.exn_on ~valid Stateid.dummy (Vernacstate.Proof_global.NoCurrentProof, Exninfo.null))
+       Exninfo.iraise (State.exn_on ~valid Stateid.dummy (PG_compat.NoCurrentProof, Exninfo.null))
 
 (* When tty is true, this code also does some of the job of the user interface:
    jump back to a state that is valid *)
@@ -3067,7 +3069,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
             let st = Vernacstate.freeze_interp_state ~marshallable:false in
             ignore(stm_vernac_interp id st x);
             (* Vernac x may or may not start a proof *)
-            if not in_proof && Vernacstate.Proof_global.there_are_pending_proofs () then
+            if not in_proof && PG_compat.there_are_pending_proofs () then
             begin
               let bname = VCS.mk_branch_name x in
               let opacity_of_produced_term = function
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index 416ea88c1b..8934385091 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -85,7 +85,7 @@ let ensure_exists f =
 let compile opts copts ~echo ~f_in ~f_out =
   let open Vernac.State in
   let check_pending_proofs () =
-    let pfs = Vernacstate.Proof_global.get_all_proof_names () in
+    let pfs = Vernacstate.Proof_global.get_all_proof_names () [@ocaml.warning "-3"] in
     if not (CList.is_empty pfs) then
       fatal_error (str "There are pending proofs: "
                     ++ (pfs
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 4129562065..087cd67f3a 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -194,6 +194,7 @@ let make_prompt () =
     (Names.Id.to_string (Vernacstate.Proof_global.get_current_proof_name ())) ^ " < "
   with Vernacstate.Proof_global.NoCurrentProof ->
     "Coq < "
+  [@@ocaml.warning "-3"]
 
 (* the coq prompt added to the default one when in emacs mode
    The prompt contains the current state label [n] (for global
@@ -363,6 +364,7 @@ let top_goal_print ~doc c oldp newp =
     let loc = Loc.get_loc info in
     let msg = CErrors.iprint (e, info) in
     TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer
+  [@@ocaml.warning "-3"]
 
 let exit_on_error =
   let open Goptions in
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 038ff54bf6..6c6379ec5e 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -70,7 +70,7 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) =
 
       (* Force the command  *)
       let ndoc = if check then Stm.observe ~doc nsid else doc in
-      let new_proof = Vernacstate.Proof_global.give_me_the_proof_opt () in
+      let new_proof = Vernacstate.Proof_global.give_me_the_proof_opt () [@ocaml.warning "-3"] in
       { state with doc = ndoc; sid = nsid; proof = new_proof; }
     with reraise ->
       (* XXX: In non-interactive mode edit_at seems to do very weird
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 3a305c3b61..e44d68b87d 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2627,7 +2627,7 @@ let interp ?(verbosely=true) ?proof ~st cmd =
   try vernac_timeout (fun st ->
       let v_mod = if verbosely then Flags.verbosely else Flags.silently in
       let pstate = v_mod (interp_control ?proof ~st) cmd in
-      Vernacstate.Proof_global.set pstate;
+      Vernacstate.Proof_global.set pstate [@ocaml.warning "-3"];
       Vernacstate.freeze_interp_state ~marshallable:false
     ) st
   with exn ->
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index b79f97796f..dff81ad9bb 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -82,3 +82,4 @@ module Proof_global : sig
   val copy_terminators : src:t option -> tgt:t option -> t option
 
 end
+[@@ocaml.deprecated "This module is internal and should not be used, instead, thread the proof state"]