diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-03 01:58:48 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-03 07:15:44 +0100 |
commit | e2789752960dabcda94e531f2c179446ad7dbb25 (patch) | |
tree | fa6f68a6ceebf17c177fc3b33b1bad0f60d4405f /plugins/ltac | |
parent | df9d3a36e71d6d224286811fdc529ad5a955deb7 (diff) |
[compat] Remove "Intuition Iff Unfolding"
Following up on #6791, we remove the option "Intuition Iff Unfolding"
Diffstat (limited to 'plugins/ltac')
-rw-r--r-- | plugins/ltac/tauto.ml | 22 |
1 files changed, 3 insertions, 19 deletions
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 5ce30c3d7..b9b84f3f4 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -63,11 +63,6 @@ let assoc_flags ist : tauto_flags = (* Whether inner not are unfolded *) let negation_unfolding = ref true -(* Whether inner iff are unfolded *) -let iff_unfolding = ref false - -let unfold_iff () = !iff_unfolding - open Goptions let _ = declare_bool_option @@ -77,14 +72,6 @@ let _ = optread = (fun () -> !negation_unfolding); optwrite = (:=) negation_unfolding } -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "unfolding of iff in intuition"; - optkey = ["Intuition";"Iff";"Unfolding"]; - optread = (fun () -> !iff_unfolding); - optwrite = (:=) iff_unfolding } - (** Base tactics *) let idtac = Proofview.tclUNIT () @@ -200,16 +187,13 @@ let make_unfold name = let const = Constant.make2 (ModPath.MPfile dir) (Label.make name) in (Locus.AllOccurrences, ArgArg (EvalConstRef const, None)) -let u_iff = make_unfold "iff" let u_not = make_unfold "not" let reduction_not_iff _ ist = let make_reduce c = TacAtom (Loc.tag @@ TacReduce (Genredexpr.Unfold c, Locusops.allHypsAndConcl)) in - let tac = match !negation_unfolding, unfold_iff () with - | true, true -> make_reduce [u_not; u_iff] - | true, false -> make_reduce [u_not] - | false, true -> make_reduce [u_iff] - | false, false -> TacId [] + let tac = match !negation_unfolding with + | true -> make_reduce [u_not] + | false -> TacId [] in eval_tactic_ist ist tac |