diff options
| author | Emilio Jesus Gallego Arias | 2020-03-14 22:41:07 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-10 01:18:52 -0400 |
| commit | 2b3bd349914a759b270cea48a7ec32c9320f1792 (patch) | |
| tree | 2557ec70c694f790d01937f666a8770711672532 /vernac | |
| parent | 795df4b7a194b53b592ed327d2318ef5abc7d131 (diff) | |
[obligations] Deprecated flag cleanup
We deprecate `Hide Obligations` and remove `Shrink Obligations`
[deprecated since 8.7]
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 bba3687256..e9fc70cd97 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 |