aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-04-10 20:17:23 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-04-10 20:31:50 +0200
commitab66d07f321810e1142d0d2dc02511fa4ba0cffa (patch)
tree4da604c26f12f6aa9da68f91f31a67e8c33d07c5 /theories
parent23433eca87698d7e405861fd14f5fc2c375fb5bd (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 'theories')
0 files changed, 0 insertions, 0 deletions