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 /plugins/firstorder | |
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 'plugins/firstorder')
0 files changed, 0 insertions, 0 deletions