diff options
| author | Pierre-Marie Pédrot | 2016-05-17 11:02:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-17 11:06:14 +0200 |
| commit | 43343c1f79d9f373104ae5174baf41e2257e2b8d (patch) | |
| tree | 7ac3a1ec228702fd8bf81c828e3d3e1c8f0ebc3c /kernel/nativelambda.ml | |
| parent | cddddce068bc0482f62ffab8e412732a307b90bb (diff) | |
Removing the old refine tactic from the Tactics module.
It is indeed confusing, as it has little to do with the proper refine defined
in the New submodule. Legacy code relying on it should call the Logic or
Tacmach modules instead.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions