diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-03 01:50:30 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-06 10:53:27 +0100 |
| commit | 6e0c7f83c6ad024df7105f9b799fda9dbe7a14d0 (patch) | |
| tree | 92bccad12e3f512b31568ba6d422420f956398d8 /tactics/equality.ml | |
| parent | db8fcbb7763ac784f7c72b72509d5dc7c2c5323c (diff) | |
[compat] Remove "Discriminate Introduction"
Following up on #6791, we the option "Discriminate Introduction".
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 20 |
1 files changed, 3 insertions, 17 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 236db1dcc..98f627f21 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -56,18 +56,7 @@ type inj_flags = { injection_pattern_l2r_order : bool; } -let discriminate_introduction = ref true - -let discr_do_intro () = !discriminate_introduction - open Goptions -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "automatic introduction of hypotheses by discriminate"; - optkey = ["Discriminate";"Introduction"]; - optread = (fun () -> !discriminate_introduction); - optwrite = (:=) discriminate_introduction } let use_injection_pattern_l2r_order = function | None -> true @@ -1080,13 +1069,10 @@ let discrClause with_evars = onClause (discrSimpleClause with_evars) let discrEverywhere with_evars = tclTHEN (Proofview.tclUNIT ()) (* Delay the interpretation of side-effect *) - (if discr_do_intro () then - (tclTHEN - (tclREPEAT introf) - (tryAllHyps + (tclTHEN + (tclREPEAT introf) + (tryAllHyps (fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings))))) - else (* <= 8.2 compat *) - tryAllHypsAndConcl (discrSimpleClause with_evars)) let discr_tac with_evars = function | None -> discrEverywhere with_evars |