diff options
| author | Gaëtan Gilbert | 2020-05-13 13:02:51 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-05-13 13:02:51 +0200 |
| commit | 23be910b49eac7a69a30b1e737a4738e24edcaa0 (patch) | |
| tree | 8bceafd4270a4943a48f7d6ebd26e0fa27a7e656 /vernac | |
| parent | 67f0e9fd40dc2f7b30a8aec4c7efb032e61a001e (diff) | |
| parent | 2b3bd349914a759b270cea48a7ec32c9320f1792 (diff) | |
Merge PR #11828: [obligations] Deprecated flag cleanup
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/declareObl.ml | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index ab11472dec..9ea54f5d8f 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -111,11 +111,6 @@ open ProgramDecl (* Saving an obligation *) -let get_shrink_obligations = - Goptions.declare_bool_option_and_ref ~depr:true (* remove in 8.8 *) - ~key:["Shrink"; "Obligations"] - ~value:true - (* XXX: Is this the right place for this? *) let it_mkLambda_or_LetIn_or_clean t ctx = let open Context.Rel.Declaration in @@ -190,7 +185,7 @@ let add_hint local prg cst = (* true = hide obligations *) let get_hide_obligations = Goptions.declare_bool_option_and_ref - ~depr:false + ~depr:true ~key:["Hide"; "Obligations"] ~value:false @@ -203,7 +198,7 @@ let declare_obligation prg obl body ty uctx = let opaque = (not force) && opaque in let poly = prg.prg_poly in let ctx, body, ty, args = - if get_shrink_obligations () && not poly then shrink_body body ty + if not poly then shrink_body body ty else ([], body, ty, [||]) in let ce = Declare.definition_entry ?types:ty ~opaque ~univs:uctx body in |