diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-06-07 11:23:41 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-07 11:23:41 +0200 |
commit | 77e4a3712dff87e5941dd93ebfa8028039ab0715 (patch) | |
tree | ca9db76e334d40fb19938b014a20c3691866092a /stm/stm.ml | |
parent | 3e29266b1e2dfb970ca77fb5910b6a5860d4ad1a (diff) | |
parent | 48476a32fa9221b216074695cceeaa0b34fc659b (diff) |
Merge PR#717: [proof] Deprecate "proof mode" API
Diffstat (limited to 'stm/stm.ml')
-rw-r--r-- | stm/stm.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index e95bec099..a79bf5426 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 @@ -502,7 +502,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 @@ -511,10 +511,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 = @@ -2368,8 +2368,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 () = @@ -2551,7 +2551,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.") @@ -2632,7 +2632,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 *) |