diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-10 20:17:23 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-10 20:31:50 +0200 |
| commit | ab66d07f321810e1142d0d2dc02511fa4ba0cffa (patch) | |
| tree | 4da604c26f12f6aa9da68f91f31a67e8c33d07c5 /tactics | |
| parent | 23433eca87698d7e405861fd14f5fc2c375fb5bd (diff) | |
Deprecate the "simple subst" tactic.
This tactic was introduced by aba4b19 in 2009 and never documented. Its main
purpose was backward compatibility, and as such it ought to be deprecated.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 98f627f21..5821717d9 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1761,8 +1761,17 @@ type subst_tactic_flags = { let default_subst_tactic_flags = { only_leibniz = false; rewrite_dependent_proof = true } +let warn_deprecated_simple_subst = + CWarnings.create ~name:"deprecated-simple-subst" ~category:"deprecated" + (fun () -> strbrk"\"simple subst\" is deprecated") + let subst_all ?(flags=default_subst_tactic_flags) () = + let () = + if flags.only_leibniz || not flags.rewrite_dependent_proof then + warn_deprecated_simple_subst () + in + if !regular_subst_tactic then (* First step: find hypotheses to treat in linear time *) |