diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/obligations.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 4b1565d3ce..10d3317f8d 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -350,7 +350,7 @@ let get_shrink_obligations () = !shrink_obligations let _ = declare_bool_option - { optdepr = true; + { optdepr = true; (* remove in 8.8 *) optname = "Shrinking of Program obligations"; optkey = ["Shrink";"Obligations"]; optread = get_shrink_obligations; diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 8a647c6c18..9650ea19d7 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1811,9 +1811,9 @@ let vernac_end_subproof () = Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus subproof_kind p ()) -let vernac_bullet (bullet:Proof_global.Bullet.t) = +let vernac_bullet (bullet : Proof_bullet.t) = Proof_global.simple_with_current_proof (fun _ p -> - Proof_global.Bullet.put p bullet) + Proof_bullet.put p bullet) let vernac_show = let open Feedback in function | ShowScript -> assert false (* Only the stm knows the script *) |