diff options
| -rw-r--r-- | proofs/proof_global.ml | 10 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 10 | ||||
| -rw-r--r-- | stm/stm.ml | 9 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 14 |
4 files changed, 27 insertions, 16 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 647dbe1115..36277bf58d 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -23,8 +23,9 @@ open Names (* Type of proof modes : - 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 : string ; + name : proof_mode_name ; set : unit -> unit ; reset : unit -> unit } @@ -45,6 +46,9 @@ let _ = register_proof_mode standard (* Default proof mode, to be set at the beginning of proofs. *) let default_proof_mode = ref (find_proof_mode "No") +let get_default_proof_mode_name () = + (CEphemeron.default !default_proof_mode standard).name + let _ = Goptions.declare_string_option {Goptions. optsync = true ; @@ -219,8 +223,8 @@ let set_proof_mode mn = let activate_proof_mode mode = CEphemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ()) -let disactivate_proof_mode mode = - CEphemeron.iter_opt (find_proof_mode mode) (fun x -> x.reset ()) +let disactivate_current_proof_mode () = + CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()) (** [start_proof sigma id str goals terminator] starts a proof of name [id] with goals [goals] (a list of pairs of environment and diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index ebe7f6d6f3..59daa29681 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -16,8 +16,9 @@ - A function [reset] to reset the *standard mode* from it *) +type proof_mode_name = string type proof_mode = { - name : string ; + name : proof_mode_name ; set : unit -> unit ; reset : unit -> unit } @@ -27,6 +28,7 @@ type 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,7 +42,7 @@ 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 : string -> unit +val set_proof_mode : proof_mode_name -> unit exception NoCurrentProof val give_me_the_proof : unit -> Proof.proof @@ -153,8 +155,8 @@ val get_universe_binders : unit -> universe_binders option (**********************************************************) -val activate_proof_mode : string -> unit -val disactivate_proof_mode : string -> unit +val activate_proof_mode : proof_mode_name -> unit +val disactivate_current_proof_mode : unit -> unit (**********************************************************) (* *) diff --git a/stm/stm.ml b/stm/stm.ml index f16b115e4b..8f11875b62 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -83,6 +83,8 @@ let async_proofs_workers_extra_env = ref [||] type ast = { verbose : bool; loc : Loc.t; mutable expr : vernac_expr } let pr_ast { expr } = pr_vernac expr +let default_proof_mode () = Proof_global.get_default_proof_mode_name () + (* Commands piercing opaque *) let may_pierce_opaque = function | { expr = VernacPrint (PrintName _) } -> true @@ -482,7 +484,7 @@ end = struct (* {{{ *) Proof_global.activate_proof_mode mode with Failure _ -> checkout Branch.master; - Proof_global.disactivate_proof_mode "Classic" + Proof_global.disactivate_current_proof_mode () (* copies the transaction on every open branch *) let propagate_sideff ~replay:t = @@ -2286,8 +2288,9 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity | _ -> Doesn'tGuaranteeOpacity in VCS.commit id (Fork (x,bname,opacity_of_produced_term,[])); - VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1)); - Proof_global.activate_proof_mode "Classic"; + let proof_mode = default_proof_mode () in + VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1)); + Proof_global.activate_proof_mode proof_mode; end else begin VCS.commit id (Cmd { ctac=false;ceff=in_proof;cast=x;cids=[];cqueue=`MainQueue }); diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index ecaf0fb7c5..b1df3c9ca6 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -10,6 +10,8 @@ open Vernacexpr open Errors open Pp +let default_proof_mode () = Proof_global.get_default_proof_mode_name () + let string_of_in_script b = if b then " (inside script)" else "" let string_of_vernac_type = function @@ -115,27 +117,27 @@ let rec classify_vernac e = (* StartProof *) | VernacDefinition ( (Some Decl_kinds.Discharge,Decl_kinds.Definition),((_,i),_),ProveBody _) -> - VtStartProof("Classic",Doesn'tGuaranteeOpacity,[i]), VtLater + VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater | VernacDefinition (_,((_,i),_),ProveBody _) -> - VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater + VtStartProof(default_proof_mode (),GuaranteesOpacity,[i]), VtLater | VernacStartTheoremProof (_,l,_) -> let ids = CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in - VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater - | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater + VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater + | VernacGoal _ -> VtStartProof (default_proof_mode (),GuaranteesOpacity,[]), VtLater | VernacFixpoint (_,l) -> let ids, open_proof = List.fold_left (fun (l,b) ((((_,id),_),_,_,_,p),_) -> id::l, b || p = None) ([],false) l in if open_proof - then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater + then VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater else VtSideff ids, VtLater | VernacCoFixpoint (_,l) -> let ids, open_proof = List.fold_left (fun (l,b) ((((_,id),_),_,_,p),_) -> id::l, b || p = None) ([],false) l in if open_proof - then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater + then VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater else VtSideff ids, VtLater (* Sideff: apply to all open branches. usually run on master only *) | VernacAssumption (_,_,l) -> |