aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--proofs/proof_global.mli77
-rw-r--r--stm/stm.ml16
-rw-r--r--stm/vernac_classifier.ml2
-rw-r--r--vernac/vernacentries.ml6
4 files changed, 55 insertions, 46 deletions
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 52bbd9ac5..22cc8cf59 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -10,26 +10,6 @@
toplevel. In particular it defines the global proof
environment. *)
-(** Type of proof modes :
- - A name
- - A function [set] to set it *from standard mode*
- - A function [reset] to reset the *standard mode* from it
-
-*)
-type proof_mode_name = string
-type proof_mode = {
- name : proof_mode_name ;
- set : unit -> unit ;
- reset : unit -> unit
-}
-
-(** Registers a new proof mode which can then be adressed by name
- in [set_default_proof_mode].
- One mode is already registered - the standard mode - named "No",
- It corresponds to Coq default setting are they are set when coqtop starts. *)
-val register_proof_mode : proof_mode -> unit
-val get_default_proof_mode_name : unit -> proof_mode_name
-
val there_are_pending_proofs : unit -> bool
val check_no_pending_proof : unit -> unit
@@ -40,10 +20,6 @@ val discard : Names.Id.t Loc.located -> unit
val discard_current : unit -> unit
val discard_all : unit -> unit
-(** [set_proof_mode] sets the proof mode to be used after it's called. It is
- typically called by the Proof Mode command. *)
-val set_proof_mode : proof_mode_name -> unit
-
exception NoCurrentProof
val give_me_the_proof : unit -> Proof.proof
(** @raise NoCurrentProof when outside proof mode. *)
@@ -147,16 +123,6 @@ val get_universe_binders : unit -> universe_binders option
(**********************************************************)
(* *)
-(* Proof modes *)
-(* *)
-(**********************************************************)
-
-
-val activate_proof_mode : proof_mode_name -> unit
-val disactivate_current_proof_mode : unit -> unit
-
-(**********************************************************)
-(* *)
(* Bullets *)
(* *)
(**********************************************************)
@@ -211,3 +177,46 @@ val freeze : marshallable:[`Yes | `No | `Shallow] -> state
val unfreeze : state -> unit
val proof_of_state : state -> Proof.proof
val copy_terminators : src:state -> tgt:state -> state
+
+
+(**********************************************************)
+(* Proof Mode API *)
+(* The current Proof Mode API is deprecated and a new one *)
+(* will be (hopefully) defined in 8.8 *)
+(**********************************************************)
+
+(** Type of proof modes :
+ - A name
+ - A function [set] to set it *from standard mode*
+ - A function [reset] to reset the *standard mode* from it
+
+*)
+type proof_mode_name = string
+type proof_mode = {
+ name : proof_mode_name ;
+ set : unit -> unit ;
+ reset : unit -> unit
+}
+
+(** Registers a new proof mode which can then be adressed by name
+ in [set_default_proof_mode].
+ One mode is already registered - the standard mode - named "No",
+ It corresponds to Coq default setting are they are set when coqtop starts. *)
+val register_proof_mode : proof_mode -> unit
+(* Can't make this deprecated due to limitations of camlp5 *)
+(* [@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] *)
+
+val get_default_proof_mode_name : unit -> proof_mode_name
+[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
+
+(** [set_proof_mode] sets the proof mode to be used after it's called. It is
+ typically called by the Proof Mode command. *)
+val set_proof_mode : proof_mode_name -> unit
+[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
+
+val activate_proof_mode : proof_mode_name -> unit
+[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
+
+val disactivate_current_proof_mode : unit -> unit
+[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
+
diff --git a/stm/stm.ml b/stm/stm.ml
index b98cb312e..2ea36cf78 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -80,7 +80,7 @@ type aast = {
}
let pr_ast { expr; indentation } = Pp.(int indentation ++ str " " ++ Ppvernac.pr_vernac expr)
-let default_proof_mode () = Proof_global.get_default_proof_mode_name ()
+let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"]
(* Commands piercing opaque *)
let may_pierce_opaque = function
@@ -500,7 +500,7 @@ end = struct (* {{{ *)
if List.mem edit_branch (Vcs_.branches !vcs) then begin
checkout edit_branch;
match get_branch edit_branch with
- | { kind = `Edit (mode, _,_,_,_) } -> Proof_global.activate_proof_mode mode
+ | { kind = `Edit (mode, _,_,_,_) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
| _ -> assert false
end else
let pl = proof_nesting () in
@@ -509,10 +509,10 @@ end = struct (* {{{ *)
| h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in
checkout branch;
stm_prerr_endline (fun () -> "mode:" ^ mode);
- Proof_global.activate_proof_mode mode
+ Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
with Failure _ ->
checkout Branch.master;
- Proof_global.disactivate_current_proof_mode ()
+ Proof_global.disactivate_current_proof_mode () [@ocaml.warning "-3"]
(* copies the transaction on every open branch *)
let propagate_sideff ~action =
@@ -2367,8 +2367,8 @@ let finish () =
hides true bugs cf bug #5363. Also, what happens with observe? *)
(* Some commands may by side effect change the proof mode *)
match VCS.get_branch head with
- | { VCS.kind = `Edit (mode,_,_,_,_) } -> Proof_global.activate_proof_mode mode
- | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode
+ | { VCS.kind = `Edit (mode,_,_,_,_) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
+ | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
| _ -> ()
let wait () =
@@ -2550,7 +2550,7 @@ let process_transaction ?(newtip=Stateid.fresh ())
VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1));
VCS.merge id ~ours:(Fork (x, bname, guarantee, names)) head
end;
- Proof_global.activate_proof_mode mode;
+ Proof_global.activate_proof_mode mode [@ocaml.warning "-3"];
Backtrack.record (); if w == VtNow then finish (); `Ok
| VtProofMode _, VtLater ->
anomaly(str"VtProofMode must be executed VtNow")
@@ -2631,7 +2631,7 @@ let process_transaction ?(newtip=Stateid.fresh ())
VCS.commit id (Fork (x,bname,opacity_of_produced_term x.expr,[]));
let proof_mode = default_proof_mode () in
VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1));
- Proof_global.activate_proof_mode proof_mode;
+ Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"];
end else begin
VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
(* We hope it can be replayed, but we can't really know *)
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index c4f392f20..9c24bf379 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -10,7 +10,7 @@ open Vernacexpr
open CErrors
open Pp
-let default_proof_mode () = Proof_global.get_default_proof_mode_name ()
+let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"]
let string_of_in_script b = if b then " (inside script)" else ""
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6c1d64cfe..ca2cac7f9 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1871,8 +1871,8 @@ exception End_of_input
*)
let vernac_load interp fname =
let interp x =
- let proof_mode = Proof_global.get_default_proof_mode_name () in
- Proof_global.activate_proof_mode proof_mode;
+ let proof_mode = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] in
+ Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"];
interp x in
let parse_sentence = Flags.with_option Flags.we_are_parsing
(fun po ->
@@ -2055,7 +2055,7 @@ let interp ?proof ?loc locality poly c =
| VernacProof (Some tac, Some l) ->
Aux_file.record_in_aux_at ?loc "VernacProof" "tac:yes using:yes";
vernac_set_end_tac tac; vernac_set_used_variables l
- | VernacProofMode mn -> Proof_global.set_proof_mode mn
+ | VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"]
(* Extensions *)
| VernacExtend (opn,args) -> Vernacinterp.call ?locality (opn,args)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 07:04:20 +0000