diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-06 09:46:11 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-06 09:46:11 +0100 |
| commit | 7b14d01ccc41b47df9644391bf01e4b7949e571d (patch) | |
| tree | 78c28af49a3a77277632b64783a5325ed0186482 /plugins/ltac | |
| parent | c71ad19f52e003cfb21f80bb4071fdbeb3ce11a7 (diff) | |
| parent | e2789752960dabcda94e531f2c179446ad7dbb25 (diff) | |
Merge PR #6898: [compat] Remove "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 d0f31cd42..a51c09ca4 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -65,11 +65,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 @@ -79,14 +74,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 () @@ -202,16 +189,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 |